BrowserSecurity
/
Core_DOM-dev
Archived
forked from afp-mirror/Core_DOM
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Added support for multiple sorts in shortened type variables.

This commit is contained in:
Michael Herzberg 2019-07-25 16:27:10 +01:00
parent e04b656f02
commit ac0fa734e4
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Core_DOM/preliminaries/Hiding_Type_Variables.thy
View File

@ -276,9 +276,8 @@ structure Hide_Tvar : HIDE_TVAR = struct
val thy = Proof_Context.theory_of ctx val thy = Proof_Context.theory_of ctx
fun parse_ast ((Ast.Constant const)::[]) = (const,NONE) fun parse_ast ((Ast.Constant const)::[]) = (const,NONE)
| parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[]) | parse_ast (sort::(Ast.Constant const)::[]) = (const,SOME sort)
= (const,SOME sort) | parse_ast _ = error("AST type not supported.")
| parse_ast _ = error("AST type not supported.")
val (decorated_name, decorated_sort) = parse_ast ast val (decorated_name, decorated_sort) = parse_ast ast
@ -295,9 +294,9 @@ structure Hide_Tvar : HIDE_TVAR = struct
let fun mk_tvar n = let fun mk_tvar n =
case decorated_sort of case decorated_sort of
NONE => Ast.Variable(name_of_tvar n) NONE => Ast.Variable(name_of_tvar n)
| SOME sort => Ast.Appl([Ast.Constant("_ofsort"), | SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
Ast.Variable(name_of_tvar n), Ast.Variable(name_of_tvar n),
Ast.Constant(sort)]) sort])
in in
map mk_tvar (#tvars default_info) map mk_tvar (#tvars default_info)
end end