From 66101d2527c263e3f16d035276ff729c16d2f378 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 20 Jun 2018 10:57:09 +0100 Subject: [PATCH] Changed styntax for type wildcard from __ to (_). --- Hiding_Type_Variables.thy | 38 ++++++++++++++++++-------------------- README.md | 2 +- 2 files changed, 19 insertions(+), 21 deletions(-) diff --git a/Hiding_Type_Variables.thy b/Hiding_Type_Variables.thy index b6cb948..341f636 100644 --- a/Hiding_Type_Variables.thy +++ b/Hiding_Type_Variables.thy @@ -41,8 +41,8 @@ text\This theory implements a mechanism for declaring default type variables for data types. This comes handy for complex data types with many type variables. The theory sets up both configurable print and parse translations that allows for replacing @{emph \all\} type variables - by @{text \__\}, e.g., @{text \('a, 'b, 'c, 'd, 'e) foo\} becomes - @{text \__ foo\}. The use of this shorthand in output (printing) and input + by @{text \(_)\}, e.g., @{text \('a, 'b, 'c, 'd, 'e) foo\} becomes + @{text \(_) foo\}. The use of this shorthand in output (printing) and input (parsing) is, on a per-type basis, user-configurable.\ @@ -53,7 +53,7 @@ signature HIDE_TVAR = sig datatype parse_mode = active | noparse type hide_varT = { name: string, - tvars: string list, + tvars: typ list, print_mode: print_mode, parse_mode: parse_mode } @@ -73,7 +73,7 @@ structure Hide_Tvar : HIDE_TVAR = struct datatype parse_mode = active | noparse type hide_varT = { name: string, - tvars: string list, + tvars: typ list, print_mode: print_mode, parse_mode: parse_mode } @@ -144,7 +144,7 @@ structure Hide_Tvar : HIDE_TVAR = struct | _ => error("Complex type not (yet) supported.") val local_name_of = hd o rev o String.fields (fn c => c = #".") val local_tname = local_name_of tname - val hide_type = Syntax.const("__ "^(local_tname)) + val hide_type = Syntax.const("(_) "^(local_tname)) val reg_type = Term.list_comb(Const(local_tname,typ),terms) in case lookup (Proof_Context.theory_of ctx) fq_name of @@ -168,7 +168,11 @@ structure Hide_Tvar : HIDE_TVAR = struct val _ = if #parse_mode default_info = noparse then error("Default type vars disabled (option noparse): "^name) else () - val type_vars_ast = map (fn n => Ast.Variable(n)) (#tvars default_info) + fun name_of_tvar tvar = case tvar of (TFree(n,_)) => n + | _ => error("Unsupported type structure.") + + + val type_vars_ast = map (fn n => Ast.Variable(name_of_tvar n)) (#tvars default_info) in Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast) end @@ -178,14 +182,8 @@ structure Hide_Tvar : HIDE_TVAR = struct let val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy) val typ = Syntax.parse_typ ctx typ_str - val (name,tvars) = case typ of - Type(name,ts) => let - val tvars = map (fn (TFree(n,_)) => n - | _ => error("Unsupported type structure.")) ts - in - (name,tvars) - end - | _ => error("Complex type not (yet) supported.") + val (name,tvars) = case typ of Type(name,tvars) => (name,tvars) + | _ => error("Unsupported type structure.") val print_m = case print_mode of SOME m => m | NONE => always @@ -211,7 +209,7 @@ end \ section\Register Parse Translation\ -syntax "_tvars_wildcard" :: "type \ type" ("'_'_ _") +syntax "_tvars_wildcard" :: "type \ type" ("'('_') _") parse_ast_translation\ [(@{syntax_const "_tvars_wildcard"}, Hide_Tvar.hide_tvar_ast_tr)] \ @@ -272,21 +270,21 @@ assert[string_of_thm_equal, update_default_tvars_mode "_ foobar" (always,noparse) assert[string_of_thm_equal, - thm_def="f_def", str="f (a::__ foobar) (b::__ foobar) = a"] + thm_def="f_def", str="f (a::(_) foobar) (b::(_) foobar) = a"] assert[string_of_thm_equal, - thm_def="g_def", str="g (a::__ foobar) (b::__ foobar) = a"] + thm_def="g_def", str="g (a::(_) foobar) (b::(_) foobar) = a"] subsection\Parse Translation\ update_default_tvars_mode "_ foobar" (noprint,active) declare [[show_types]] -definition A :: "'alpha \ __ foobar" +definition A :: "'alpha \ (_) foobar" where "A = foo" -definition B :: "__ foobar \ __ foobar \ __ foobar" +definition B :: "(_) foobar \ (_) foobar \ (_) foobar" where "B x y = x" -definition C :: "__ baz \ __ foobar \ __ baz" +definition C :: "(_) baz \ (_) foobar \ (_) baz" where "C x y = x" diff --git a/README.md b/README.md index 6e70df2..aedfd2b 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ older versions might be available on a dedicated branch. * [Hiding_Type_Variables.thy](Hiding_Type_Variables.thy) provides print a setup for defining default type variables of type constructors. The default type variables can be hidden in output, - e.g., `('a, 'b, 'c) foo` is shown as `__ foo`. This shorthand + e.g., `('a, 'b, 'c) foo` is shown as `(_) foo`. This shorthand notation can also be used in input (using a parse translation), which (sometimes) helps to focus on the important parts of complex type declarations.