--- a/NEWS Tue Mar 09 23:29:04 2010 +0100
+++ b/NEWS Tue Mar 09 23:32:13 2010 +0100
@@ -76,6 +76,10 @@
within a local theory context, with explicit checking of the
constructors involved (in contrast to the raw 'syntax' versions).
+* Command 'typedecl' now works within a local theory context --
+without introducing dependencies on parameters or assumptions, which
+is not possible in Isabelle/Pure.
+
*** HOL ***
--- a/doc-src/IsarRef/Thy/Spec.thy Tue Mar 09 23:29:04 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Tue Mar 09 23:32:13 2010 +0100
@@ -954,7 +954,7 @@
text {*
\begin{matharray}{rcll}
@{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Tue Mar 09 23:29:04 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Mar 09 23:32:13 2010 +0100
@@ -991,7 +991,7 @@
\begin{isamarkuptext}%
\begin{matharray}{rcll}
\indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\end{matharray}
--- a/src/Pure/Isar/isar_syn.ML Tue Mar 09 23:29:04 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Mar 09 23:32:13 2010 +0100
@@ -103,16 +103,15 @@
(* types *)
val _ =
- OuterSyntax.command "typedecl" "type declaration" K.thy_decl
- (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
- Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
+ OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
+ (P.type_args -- P.binding -- P.opt_mixfix
+ >> (fn ((args, a), mx) => Typedecl.typedecl (a, args, mx) #> snd));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
(P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
- >> (Toplevel.theory o Sign.add_tyabbrs o
- map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+ >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
val _ =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
--- a/src/Pure/Isar/typedecl.ML Tue Mar 09 23:29:04 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML Tue Mar 09 23:32:13 2010 +0100
@@ -6,26 +6,50 @@
signature TYPEDECL =
sig
- val typedecl: binding * string list * mixfix -> theory -> typ * theory
+ val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
+ val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
end;
structure Typedecl: TYPEDECL =
struct
-fun typedecl (b, vs, mx) thy =
+fun typedecl (b, vs, mx) lthy =
let
- val base_sort = Object_Logic.get_base_sort thy;
- val _ = has_duplicates (op =) vs andalso
- error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
- val name = Sign.full_name thy b;
+ fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
+ val _ = has_duplicates (op =) vs andalso err "Duplicate parameters";
+
+ val name = Local_Theory.full_name lthy b;
val n = length vs;
- val T = Type (name, map (fn v => TFree (v, [])) vs);
+ val args = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) vs;
+ val T = Type (name, args);
+
+ val bad_args =
+ #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
+ |> filter_out Term.is_TVar;
+ val _ = not (null bad_args) andalso
+ err ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ lthy) bad_args));
+
+ val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
in
- thy
- |> Sign.add_types [(b, n, mx)]
- |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
+ lthy
+ |> Local_Theory.theory
+ (Sign.add_types [(b, n, NoSyn)] #>
+ (case base_sort of
+ NONE => I
+ | SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
+ |> Local_Theory.checkpoint
+ |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
+ |> Local_Theory.type_syntax false
+ (fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
+ |> ProofContext.type_alias b name
+ |> Variable.declare_typ T
|> pair T
end;
+fun typedecl_global decl =
+ Theory_Target.init NONE
+ #> typedecl decl
+ #> Local_Theory.exit_result_global Morphism.typ;
+
end;