isabelle-hacks/Hiding_Type_Variables.thy

553 lines
24 KiB
Plaintext

(***********************************************************************************
* Copyright (c) 2018-2019 Achim D. Brucker
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
* Repository: https://git.logicalhacking.com/adbrucker/isabelle-hacks/
* Dependencies: None (assert.thy is used for testing the theory but it is
* not required for providing the functionality of this hack)
***********************************************************************************)
(***********************************************************************************
# Changelog
This comment documents all notable changes to this file in a format inspired by
[Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres
to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
## [Unreleased]
## [1.0.0] - 2017-06-25
- Initial release
***********************************************************************************)
chapter\<open>Using Print and Parse Translations for Hiding Type Variables\<close>
theory
"Hiding_Type_Variables"
imports
"Assert" (* Can be replaced by Main, after removing all assertions. *)
keywords
"register_default_tvars"
"update_default_tvars_mode"::thy_decl
begin
text\<open>
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 \<open>all\<close>} type variables by \<open>(_)\<close>, e.g., a five-ary
constructor \<open>('a, 'b, 'c, 'd, 'e) hide_tvar_foo\<close> can be shorted to
\<open>(_) hide_tvar_foo\<close>. The use of this shorthand in output (printing) and input
(parsing) is, on a per-type basis, user-configurable using the top-level
commands \<open>register_default_tvars\<close> (for registering the names of the
default type variables and the print/parse mode) and
\<open>update_default_tvars_mode\<close> (for changing the print/parse mode
dynamically).
The input also supports short-hands for declaring default sorts (e.g.,
\<open>(_::linorder)\<close> specifies that all default variables need to be
instances of the sort (type class) @{class \<open>linorder\<close>} and short-hands
of overriding a suffice (or prefix) of the default type variables. For
example, \<open>('state) hide_tvar_foo _.\<close> is a short-hand for
\<open>('a, 'b, 'c, 'd, 'state) hide_tvar_foo\<close>.
\<close>
section\<open>Implementation\<close>
subsection\<open>Theory Managed Data Structure\<close>
ML\<open>
signature HIDE_TVAR = sig
datatype print_mode = print_all | print | noprint
datatype tvar_subst = right | left
datatype parse_mode = parse | noparse
type hide_varT = {
name: string,
tvars: typ list,
typ_syn_tab : (string * typ list*string) Symtab.table,
print_mode: print_mode,
parse_mode: parse_mode
}
val parse_print_mode : string -> print_mode
val parse_parse_mode : string -> parse_mode
val register : string -> print_mode option -> parse_mode option ->
theory -> theory
val update_mode : string -> print_mode option -> parse_mode option ->
theory -> theory
val lookup : theory -> string -> hide_varT option
val hide_tvar_tr' : string -> Proof.context -> term list -> term
val hide_tvar_ast_tr : Proof.context -> Ast.ast list -> Ast.ast
val hide_tvar_subst_ast_tr : tvar_subst -> Proof.context -> Ast.ast list
-> Ast.ast
val hide_tvar_subst_return_ast_tr : tvar_subst -> Proof.context
-> Ast.ast list -> Ast.ast
end
structure Hide_Tvar : HIDE_TVAR = struct
datatype print_mode = print_all | print | noprint
datatype tvar_subst = right | left
datatype parse_mode = parse | noparse
type hide_varT = {
name: string,
tvars: typ list,
typ_syn_tab : (string * typ list*string) Symtab.table,
print_mode: print_mode,
parse_mode: parse_mode
}
type hide_tvar_tab = (hide_varT) Symtab.table
fun hide_tvar_eq (a, a') = (#name a) = (#name a')
fun merge_tvar_tab (tab,tab') = Symtab.merge hide_tvar_eq (tab,tab')
structure Data = Generic_Data
(
type T = hide_tvar_tab
val empty = Symtab.empty:hide_tvar_tab
val extend = I
fun merge(t1,t2) = merge_tvar_tab (t1, t2)
);
fun parse_print_mode "print_all" = print_all
| parse_print_mode "print" = print
| parse_print_mode "noprint" = noprint
| parse_print_mode s = error("Print mode not supported: "^s)
fun parse_parse_mode "parse" = parse
| parse_parse_mode "noparse" = noparse
| parse_parse_mode s = error("Parse mode not supported: "^s)
fun update_mode typ_str print_mode parse_mode thy =
let
val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
val typ = Syntax.parse_typ ctx typ_str (* no type checking *)
val name = case typ of
Type(name,_) => name
| _ => error("Complex type not (yet) supported.")
fun update tab =
let
val old_entry = (case Symtab.lookup tab name of
SOME t => t
| NONE => error ("Type shorthand not registered: "^name))
val print_m = case print_mode of
SOME m => m
| NONE => #print_mode old_entry
val parse_m = case parse_mode of
SOME m => m
| NONE => #parse_mode old_entry
val entry = {
name = name,
tvars = #tvars old_entry,
typ_syn_tab = #typ_syn_tab old_entry,
print_mode = print_m,
parse_mode = parse_m
}
in
Symtab.update (name,entry) tab
end
in
Context.theory_of ( (Data.map update) (Context.Theory thy))
end
fun lookup thy name =
let
val tab = (Data.get o Context.Theory) thy
in
Symtab.lookup tab name
end
fun obtain_normalized_vname lookup_table vname =
case List.find (fn e => fst e = vname) lookup_table of
SOME (_,idx) => (lookup_table, Int.toString idx)
| NONE => let
fun max_idx [] = 0
| max_idx ((_,idx)::lt) = Int.max(idx,max_idx lt)
val idx = (max_idx lookup_table ) + 1
in
((vname,idx)::lookup_table, Int.toString idx) end
fun normalize_typvar_type lt (Type (a, Ts)) =
let
fun switch (a,b) = (b,a)
val (Ts', lt') = fold_map (fn t => fn lt => switch (normalize_typvar_type lt t)) Ts lt
in
(lt', Type (a, Ts'))
end
| normalize_typvar_type lt (TFree (vname, S)) =
let
val (lt, vname) = obtain_normalized_vname lt (vname)
in
(lt, TFree( vname, S))
end
| normalize_typvar_type lt (TVar (xi, S)) =
let
val (lt, vname) = obtain_normalized_vname lt (Term.string_of_vname xi)
in
(lt, TFree( vname, S))
end
fun normalize_typvar_type' t = snd ( normalize_typvar_type [] t)
fun mk_p s = s (* "("^s^")" *)
fun key_of_type (Type(a, TS)) = mk_p (a^String.concat(map key_of_type TS))
| key_of_type (TFree (vname, _)) = mk_p vname
| key_of_type (TVar (xi, _ )) = mk_p (Term.string_of_vname xi)
val key_of_type' = key_of_type o normalize_typvar_type'
fun normalize_typvar_term lt (Const (a, t)) = (lt, Const(a, t))
| normalize_typvar_term lt (Free (a, t)) = let
val (lt, vname) = obtain_normalized_vname lt a
in
(lt, Free(vname,t))
end
| normalize_typvar_term lt (Var (xi, t)) =
let
val (lt, vname) = obtain_normalized_vname lt (Term.string_of_vname xi)
in
(lt, Free(vname,t))
end
| normalize_typvar_term lt (Bound (i)) = (lt, Bound(i))
| normalize_typvar_term lt (Abs(s,ty,tr)) =
let
val (lt,tr) = normalize_typvar_term lt tr
in
(lt, Abs(s,ty,tr))
end
| normalize_typvar_term lt (t1$t2) =
let
val (lt,t1) = normalize_typvar_term lt t1
val (lt,t2) = normalize_typvar_term lt t2
in
(lt, t1$t2)
end
fun normalize_typvar_term' t = snd(normalize_typvar_term [] t)
fun key_of_term (Const(s,_)) = if String.isPrefix "\<^type>" s
then Lexicon.unmark_type s
else ""
| key_of_term (Free(s,_)) = s
| key_of_term (Var(xi,_)) = Term.string_of_vname xi
| key_of_term (Bound(_)) = error("Bound() not supported in key_of_term")
| key_of_term (Abs(_,_,_)) = error("Abs() not supported in key_of_term")
| key_of_term (t1$t2) = (key_of_term t1)^(key_of_term t2)
val key_of_term' = key_of_term o normalize_typvar_term'
fun hide_tvar_tr' tname ctx terms =
let
val mtyp = Syntax.parse_typ ctx tname (* no type checking *)
val (fq_name, _) = case mtyp of
Type(s,ts) => (s,ts)
| _ => error("Complex type not (yet) supported.")
val local_name_of = hd o rev o String.fields (fn c => c = #".")
fun hide_type tname = Syntax.const("(_) "^tname)
val reg_type_as_term = Term.list_comb(Const(Lexicon.mark_type tname,dummyT),terms)
val key = key_of_term' reg_type_as_term
val actual_tvars_key = key_of_term reg_type_as_term
in
case lookup (Proof_Context.theory_of ctx) fq_name of
NONE => raise Match
| SOME e => let
val (tname,default_tvars_key) =
case Symtab.lookup (#typ_syn_tab e) key of
NONE => (local_name_of tname, "")
| SOME (s,_,tv) => (local_name_of s,tv)
in
case (#print_mode e) of
print_all => hide_type tname
| print => if default_tvars_key=actual_tvars_key
then hide_type tname
else raise Match
| noprint => raise Match
end
end
fun hide_tvar_ast_tr ctx ast=
let
val thy = Proof_Context.theory_of ctx
fun parse_ast ((Ast.Constant const)::[]) = (const,NONE)
| parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[])
= (const,SOME sort)
| parse_ast _ = error("AST type not supported.")
val (decorated_name, decorated_sort) = parse_ast ast
val name = Lexicon.unmark_type decorated_name
val default_info = case lookup thy name of
NONE => error("No default type vars registered: "^name)
| SOME e => e
val _ = if #parse_mode default_info = noparse
then error("Default type vars disabled (option noparse): "^name)
else ()
fun name_of_tvar tvar = case tvar of (TFree(n,_)) => n
| _ => error("Unsupported type structure.")
val type_vars_ast =
let fun mk_tvar n =
case decorated_sort of
NONE => Ast.Variable(name_of_tvar n)
| SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
Ast.Variable(name_of_tvar n),
Ast.Constant(sort)])
in
map mk_tvar (#tvars default_info)
end
in
Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)
end
fun register typ_str print_mode parse_mode thy =
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,tvars) => (name,tvars)
| _ => error("Unsupported type structure.")
val base_typ = Syntax.read_typ ctx typ_str
val (base_name,base_tvars) = case base_typ of Type(name,tvars) => (name,tvars)
| _ => error("Unsupported type structure.")
val base_key = key_of_type' base_typ
val base_tvar_key = key_of_type base_typ
val print_m = case print_mode of
SOME m => m
| NONE => print_all
val parse_m = case parse_mode of
SOME m => m
| NONE => parse
val entry = {
name = name,
tvars = tvars,
typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
print_mode = print_m,
parse_mode = parse_m
}
val base_entry = if name = base_name
then
{
name = "",
tvars = [],
typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
print_mode = noprint,
parse_mode = noparse
}
else case lookup thy base_name of
SOME e => e
| NONE => error ("No entry found for "^base_name^
" (via "^name^")")
val base_entry = {
name = #name base_entry,
tvars = #tvars base_entry,
typ_syn_tab = Symtab.update (base_key, (name, base_tvars, base_tvar_key))
(#typ_syn_tab (base_entry)),
print_mode = #print_mode base_entry,
parse_mode = #parse_mode base_entry
}
fun reg tab = let
val tab = Symtab.update_new(name, entry) tab
val tab = if name = base_name
then tab
else Symtab.update(base_name, base_entry) tab
in
tab
end
val thy = Sign.print_translation
[(Lexicon.mark_type name, hide_tvar_tr' name)] thy
in
Context.theory_of ( (Data.map reg) (Context.Theory thy))
handle Symtab.DUP _ => error("Type shorthand already registered: "^name)
end
fun hide_tvar_subst_ast_tr hole ctx (ast::[]) =
let
val thy = Proof_Context.theory_of ctx
val (decorated_name, args) = case ast
of (Ast.Appl ((Ast.Constant s)::args)) => (s, args)
| _ => error "Error in obtaining type constructor."
val name = Lexicon.unmark_type decorated_name
val default_info = case lookup thy name of
NONE => error("No default type vars registered: "^name)
| SOME e => e
val _ = if #parse_mode default_info = noparse
then error("Default type vars disabled (option noparse): "^name)
else ()
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)
val type_vars_ast = case hole of
right => (List.rev(List.drop(List.rev type_vars_ast, List.length args)))@args
| left => args@List.drop(type_vars_ast, List.length args)
in
Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)
end
| hide_tvar_subst_ast_tr _ _ _ = error("hide_tvar_subst_ast_tr: empty AST.")
fun hide_tvar_subst_return_ast_tr hole ctx (retval::constructor::[]) =
hide_tvar_subst_ast_tr hole ctx [Ast.Appl (constructor::retval::[])]
| hide_tvar_subst_return_ast_tr _ _ _ =
error("hide_tvar_subst_return_ast_tr: error in parsing AST")
end
\<close>
subsection\<open>Register Parse Translations\<close>
syntax "_tvars_wildcard" :: "type \<Rightarrow> type" ("'('_') _")
syntax "_tvars_wildcard_retval" :: "type \<Rightarrow> type \<Rightarrow> type" ("'('_, _') _")
syntax "_tvars_wildcard_sort" :: "sort \<Rightarrow> type \<Rightarrow> type" ("'('_::_') _")
syntax "_tvars_wildcard_right" :: "type \<Rightarrow> type" ("_ '_..")
syntax "_tvars_wildcard_left" :: "type \<Rightarrow> type" ("_ ..'_")
parse_ast_translation\<open>
[
(@{syntax_const "_tvars_wildcard_sort"}, Hide_Tvar.hide_tvar_ast_tr),
(@{syntax_const "_tvars_wildcard"}, Hide_Tvar.hide_tvar_ast_tr),
(@{syntax_const "_tvars_wildcard_retval"}, Hide_Tvar.hide_tvar_subst_return_ast_tr Hide_Tvar.right),
(@{syntax_const "_tvars_wildcard_right"}, Hide_Tvar.hide_tvar_subst_ast_tr Hide_Tvar.right),
(@{syntax_const "_tvars_wildcard_left"}, Hide_Tvar.hide_tvar_subst_ast_tr Hide_Tvar.left)
]
\<close>
subsection\<open>Register Top-Level Isar Commands\<close>
ML\<open>
val modeP = (Parse.$$$ "("
|-- (Parse.name --| Parse.$$$ ","
-- Parse.name --|
Parse.$$$ ")"))
val typ_modeP = Parse.typ -- (Scan.optional modeP ("print_all","parse"))
val _ = Outer_Syntax.command @{command_keyword "register_default_tvars"}
"Register default variables (and hiding mechanims) for a type."
(typ_modeP >> (fn (typ,(print_m,parse_m)) =>
(Toplevel.theory
(Hide_Tvar.register typ
(SOME (Hide_Tvar.parse_print_mode print_m))
(SOME (Hide_Tvar.parse_parse_mode parse_m))))));
val _ = Outer_Syntax.command @{command_keyword "update_default_tvars_mode"}
"Update print and/or parse mode or the default type variables for a certain type."
(typ_modeP >> (fn (typ,(print_m,parse_m)) =>
(Toplevel.theory
(Hide_Tvar.update_mode typ
(SOME (Hide_Tvar.parse_print_mode print_m))
(SOME (Hide_Tvar.parse_parse_mode parse_m))))));
\<close>
section\<open>Examples\<close>
subsection\<open>Print Translation\<close>
datatype ('a, 'b) hide_tvar_foobar = hide_tvar_foo 'a | hide_tvar_bar 'b
type_synonym ('a, 'b, 'c, 'd) hide_tvar_baz = "('a+'b, 'a \<times> 'b) hide_tvar_foobar"
definition hide_tvar_f::"('a, 'b) hide_tvar_foobar \<Rightarrow> ('a, 'b) hide_tvar_foobar \<Rightarrow> ('a, 'b) hide_tvar_foobar"
where "hide_tvar_f a b = a"
definition hide_tvar_g::"('a, 'b, 'c, 'd) hide_tvar_baz \<Rightarrow> ('a, 'b, 'c, 'd) hide_tvar_baz \<Rightarrow> ('a, 'b, 'c, 'd) hide_tvar_baz"
where "hide_tvar_g a b = a"
assert[string_of_thm_equal,
thm_def="hide_tvar_f_def",
str="hide_tvar_f (a::('a, 'b) hide_tvar_foobar) (b::('a, 'b) hide_tvar_foobar) = a"]
assert[string_of_thm_equal,
thm_def="hide_tvar_g_def",
str="hide_tvar_g (a::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) (b::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) = a"]
register_default_tvars "('alpha, 'beta) hide_tvar_foobar" (print_all,parse)
register_default_tvars "('alpha, 'beta, 'gamma, 'delta) hide_tvar_baz" (print_all,parse)
update_default_tvars_mode "_ hide_tvar_foobar" (noprint,noparse)
assert[string_of_thm_equal,
thm_def="hide_tvar_f_def",
str="hide_tvar_f (a::('a, 'b) hide_tvar_foobar) (b::('a, 'b) hide_tvar_foobar) = a"]
assert[string_of_thm_equal,
thm_def="hide_tvar_g_def",
str="hide_tvar_g (a::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) (b::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) = a"]
update_default_tvars_mode "_ hide_tvar_foobar" (print_all,noparse)
assert[string_of_thm_equal,
thm_def="hide_tvar_f_def", str="hide_tvar_f (a::(_) hide_tvar_foobar) (b::(_) hide_tvar_foobar) = a"]
assert[string_of_thm_equal,
thm_def="hide_tvar_g_def", str="hide_tvar_g (a::(_) hide_tvar_baz) (b::(_) hide_tvar_baz) = a"]
subsection\<open>Parse Translation\<close>
update_default_tvars_mode "_ hide_tvar_foobar" (print_all,parse)
declare [[show_types]]
definition hide_tvar_A :: "'x \<Rightarrow> (('x::linorder) hide_tvar_foobar) .._"
where "hide_tvar_A x = hide_tvar_foo x"
assert[string_of_thm_equal,
thm_def="hide_tvar_A_def", str="hide_tvar_A (x::'x) = hide_tvar_foo x"]
definition hide_tvar_A' :: "'x \<Rightarrow> (('x,'b) hide_tvar_foobar) .._"
where "hide_tvar_A' x = hide_tvar_foo x"
assert[string_of_thm_equal,
thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = hide_tvar_foo x"]
definition hide_tvar_B' :: "(_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar"
where "hide_tvar_B' x y = x"
assert[string_of_thm_equal,
thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = hide_tvar_foo x"]
definition hide_tvar_B :: "(_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar"
where "hide_tvar_B x y = x"
assert[string_of_thm_equal,
thm_def="hide_tvar_B_def", str="hide_tvar_B (x::(_) hide_tvar_foobar) (y::(_) hide_tvar_foobar) = x"]
definition hide_tvar_C :: "(_) hide_tvar_baz \<Rightarrow> (_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_baz"
where "hide_tvar_C x y = x"
assert[string_of_thm_equal,
thm_def="hide_tvar_C_def", str="hide_tvar_C (x::(_) hide_tvar_baz) (y::(_) hide_tvar_foobar) = x"]
definition hide_tvar_E :: "(_::linorder) hide_tvar_baz \<Rightarrow> (_::linorder) hide_tvar_foobar \<Rightarrow> (_::linorder) hide_tvar_baz"
where "hide_tvar_E x y = x"
assert[string_of_thm_equal,
thm_def="hide_tvar_C_def", str="hide_tvar_C (x::(_) hide_tvar_baz) (y::(_) hide_tvar_foobar) = x"]
definition hide_tvar_X :: "(_, 'retval::linorder) hide_tvar_baz
\<Rightarrow> (_,'retval) hide_tvar_foobar
\<Rightarrow> (_,'retval) hide_tvar_baz"
where "hide_tvar_X x y = x"
end