--- a/NEWS Mon Jul 03 12:19:49 2017 +0200
+++ b/NEWS Mon Jul 03 14:25:07 2017 +0200
@@ -62,6 +62,10 @@
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.
+* Commands 'alias' and 'type_alias' introduce aliases for constants and
+type constructors, respectively. This allows adhoc changes to name-space
+accesses within global or local theory contexts, e.g. within a 'bundle'.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Spec.thy Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Jul 03 14:25:07 2017 +0200
@@ -1311,6 +1311,8 @@
text \<open>
\begin{matharray}{rcl}
+ @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\
@@ -1318,8 +1320,10 @@
\end{matharray}
@{rail \<open>
- ( @{command hide_class} | @{command hide_type} |
- @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
+ (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}
+ ;
+ (@{command hide_class} | @{command hide_type} |
+ @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )
\<close>}
Isabelle organizes any kind of name declarations (of types, constants,
@@ -1327,6 +1331,12 @@
the user does not have to control the behaviour of name spaces by hand, yet
the following commands provide some way to do so.
+ \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type
+ constructors, respectively. This allows adhoc changes to name-space
+ accesses.
+
+ \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.
+
\<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name
space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jul 03 12:19:49 2017 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jul 03 14:25:07 2017 +0200
@@ -17,7 +17,7 @@
"primcorec" :: thy_decl
begin
-setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close>
+alias proj = Equiv_Relations.proj
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
--- a/src/Pure/General/name_space.ML Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/General/name_space.ML Mon Jul 03 14:25:07 2017 +0200
@@ -258,8 +258,8 @@
fun completion context space (xname, pos) =
Completion.make (xname, pos) (fn completed =>
let
- fun result_ord ((precise1, (xname1, (_, name1))), (precise2, (xname2, (_, name2)))) =
- (case bool_ord (precise2, precise1) of
+ fun result_ord ((pri1, (xname1, (_, name1))), (pri2, (xname2, (_, name2)))) =
+ (case int_ord (pri2, pri1) of
EQUAL =>
(case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
EQUAL =>
@@ -271,16 +271,21 @@
val Name_Space {kind, internals, ...} = space;
val ext = extern_shortest (Context.proof_of context) space;
val full = Name.clean xname = "";
+
+ fun complete xname' name =
+ if (completed xname' orelse exists completed (Long_Name.explode xname')) andalso
+ not (is_concealed space name)
+ then
+ let
+ val xname'' = ext name;
+ val pri = (if xname' = xname'' then 1 else 0) + (if completed xname' then 1 else 0);
+ in
+ if xname' <> xname'' andalso full then I
+ else cons (pri, (xname', (kind, name)))
+ end
+ else I;
in
- Change_Table.fold
- (fn (xname', (name :: _, _)) =>
- if completed xname' andalso not (is_concealed space name) then
- let val xname'' = ext name in
- if xname' <> xname'' andalso full then I
- else cons (xname' = xname'', (xname', (kind, name)))
- end
- else I
- | _ => I) internals []
+ Change_Table.fold (fn (xname', (name :: _, _)) => complete xname' name | _ => I) internals []
|> sort_distinct result_ord
|> map #2
end);
--- a/src/Pure/Isar/local_theory.ML Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML Mon Jul 03 14:25:07 2017 +0200
@@ -63,7 +63,6 @@
val set_defsort: sort -> 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 class_alias: binding -> class -> local_theory -> local_theory
val type_alias: binding -> string -> local_theory -> local_theory
val const_alias: binding -> string -> local_theory -> local_theory
val init: Name_Space.naming -> operations -> Proof.context -> local_theory
@@ -294,7 +293,7 @@
let val binding' = Morphism.binding phi binding in
Context.mapping
(Global_Theory.alias_fact binding' name)
- (Proof_Context.fact_alias binding' name)
+ (Proof_Context.alias_fact binding' name)
end));
@@ -335,7 +334,6 @@
let val b' = Morphism.binding phi b
in Context.mapping (global_alias b' name) (local_alias b' name) end);
-val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
--- a/src/Pure/Isar/proof_context.ML Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Jul 03 14:25:07 2017 +0200
@@ -132,6 +132,7 @@
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
+ val alias_fact: binding -> string -> Proof.context -> Proof.context
val read_var: binding * string option * mixfix -> Proof.context ->
(binding * typ option * mixfix) * Proof.context
val cert_var: binding * typ option * mixfix -> Proof.context ->
@@ -158,10 +159,8 @@
Context.generic -> Context.generic
val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
- val class_alias: binding -> class -> Proof.context -> Proof.context
val type_alias: binding -> string -> Proof.context -> Proof.context
val const_alias: binding -> string -> Proof.context -> Proof.context
- val fact_alias: binding -> string -> Proof.context -> Proof.context
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
@@ -1089,6 +1088,8 @@
end;
+fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
+
(** basic logical entities **)
@@ -1184,10 +1185,8 @@
(* aliases *)
-fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
-fun fact_alias b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
(* local constants *)
--- a/src/Pure/Isar/specification.ML Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Isar/specification.ML Mon Jul 03 14:25:07 2017 +0200
@@ -45,6 +45,10 @@
(binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
(binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
+ val alias: binding * string -> local_theory -> local_theory
+ val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
+ val type_alias: binding * string -> local_theory -> local_theory
+ val type_alias_cmd: binding * (xstring * Position.T) -> 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
@@ -305,6 +309,27 @@
val abbreviation_cmd = gen_abbrev read_spec_open;
+(* alias *)
+
+fun gen_alias decl check (b, arg) lthy =
+ let
+ val (c, reports) = check {proper = true, strict = false} lthy arg;
+ val _ = Position.reports reports;
+ in decl b c lthy end;
+
+val alias =
+ gen_alias Local_Theory.const_alias (K (K (fn c => (c, []))));
+val alias_cmd =
+ gen_alias Local_Theory.const_alias
+ (fn flags => fn ctxt => fn (c, pos) =>
+ apfst (#1 o dest_Const) (Proof_Context.check_const flags ctxt (c, [pos])));
+
+val type_alias =
+ gen_alias Local_Theory.type_alias (K (K (fn c => (c, []))));
+val type_alias_cmd =
+ gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
+
+
(* notation *)
local
--- a/src/Pure/Pure.thy Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Pure.thy Mon Jul 03 14:25:07 2017 +0200
@@ -18,7 +18,7 @@
and "typedecl" "type_synonym" "nonterminal" "judgment"
"consts" "syntax" "no_syntax" "translations" "no_translations"
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
- "no_notation" "axiomatization" "lemmas" "declare"
+ "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
@@ -374,6 +374,16 @@
Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
>> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
+val _ =
+ Outer_Syntax.local_theory @{command_keyword alias} "name-space alias for constant"
+ (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
+ >> Specification.alias_cmd);
+
+val _ =
+ Outer_Syntax.local_theory @{command_keyword type_alias} "name-space alias for type constructor"
+ (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
+ >> Specification.type_alias_cmd);
+
in end\<close>
--- a/src/Pure/sign.ML Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/sign.ML Mon Jul 03 14:25:07 2017 +0200
@@ -53,7 +53,6 @@
val intern_class: theory -> xstring -> string
val intern_type: theory -> xstring -> string
val intern_const: theory -> xstring -> string
- val class_alias: binding -> class -> theory -> theory
val type_alias: binding -> string -> theory -> theory
val const_alias: binding -> string -> theory -> theory
val arity_number: theory -> string -> int
@@ -246,7 +245,6 @@
val intern_type = Name_Space.intern o type_space;
val intern_const = Name_Space.intern o const_space;
-fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
--- a/src/Pure/type.ML Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/type.ML Mon Jul 03 14:25:07 2017 +0200
@@ -29,7 +29,6 @@
val change_ignore: tsig -> tsig
val empty_tsig: tsig
val class_space: tsig -> Name_Space.T
- val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
val defaultS: tsig -> sort
val logical_types: tsig -> string list
val eq_sort: tsig -> sort * sort -> bool
@@ -202,9 +201,6 @@
val class_space = #1 o #classes o rep_tsig;
-fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
- ((Name_Space.alias naming binding name space, classes), default, types));
-
fun defaultS (TSig {default, ...}) = default;
fun logical_types (TSig {log_types, ...}) = log_types;