adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Implemented print mode (only apply print translation if default types match).

This commit is contained in:
Achim D. Brucker 2018-06-21 23:08:39 +01:00
parent 66307c1c2b
commit 54d9b20cc4
1 changed files with 22 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
Hiding_Type_Variables.thy
View File

@ -54,7 +54,7 @@ signature HIDE_TVAR = sig
type hide_varT = {
name: string,
tvars: typ list,
typ_syn_tab : (string * typ list) Symtab.table,
typ_syn_tab : (string * typ list*string) Symtab.table,
print_mode: print_mode,
parse_mode: parse_mode
}
@ -75,7 +75,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
type hide_varT = {
name: string,
tvars: typ list,
typ_syn_tab : (string * typ list) Symtab.table,
typ_syn_tab : (string * typ list*string) Symtab.table,
print_mode: print_mode,
parse_mode: parse_mode
}
@ -177,8 +177,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
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, _ )) = error("TVar not supported in key_of_type: "^
(Term.string_of_vname xi))
| key_of_type (TVar (xi, _ )) = mk_p (Term.string_of_vname xi)
val key_of_type' = key_of_type o normalize_typvar_type'
@ -216,7 +215,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
then Lexicon.unmark_type s
else ""
| key_of_term (Free(s,_)) = s
| key_of_term (Var(_,_)) = error("Var() not supported in key_of_term")
| 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)
@ -229,7 +228,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
val mtyp = Syntax.parse_typ ctx tname (* no type checking *)
val (fq_name,_) = case mtyp of
val (fq_name, _) = case mtyp of
Type(s,ts) => (s,ts)
| _ => error("Complex type not (yet) supported.")
@ -239,19 +238,23 @@ structure Hide_Tvar : HIDE_TVAR = struct
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 = case Symtab.lookup (#typ_syn_tab e) key of
NONE => local_name_of tname
| SOME (s,_) => local_name_of s
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 => hide_type tname (* TODO *)
| noprint => raise Match
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
@ -290,6 +293,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
| _ => 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
@ -300,7 +304,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
val entry = {
name = name,
tvars = tvars,
typ_syn_tab = Symtab.empty:((string * typ list) Symtab.table),
typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
print_mode = print_m,
parse_mode = parse_m
}
@ -310,7 +314,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
{
name = "",
tvars = [],
typ_syn_tab = Symtab.empty:((string * typ list) Symtab.table),
typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
print_mode = noprint,
parse_mode = noparse
}
@ -322,7 +326,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
val base_entry = {
name = #name base_entry,
tvars = #tvars base_entry,
typ_syn_tab = Symtab.update (base_key, (name, base_tvars))
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
@ -417,6 +421,9 @@ assert[string_of_thm_equal,
subsection\<open>Parse Translation\<close>
update_default_tvars_mode "_ foobar" (print_all,parse)
declare [[show_types]]
thm f_def
declare [[show_types]]
definition A :: "'alpha \<Rightarrow> (_) foobar"
where "A = foo"