(* Title: HOL/HOLCF/Tools/cont_consts.ML Author: Tobias Mayr Author: David von Oheimb Author: Makarius
HOLCF version of 'consts' command: handle continuous function types in mixfix syntax.
*)
signature CONT_CONSTS = sig val add_consts: (binding * typ * mixfix) list -> theory -> theory val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory end
structure Cont_Consts: CONT_CONSTS = struct
fun count_cfun \<^Type>\<open>cfun _ B\<close> = count_cfun B + 1
| count_cfun _ = 0
fun change_cfun 0 T = T
| change_cfun n \<^Type>\<open>cfun A B\<close> = \<^Type>\<open>fun A \<open>change_cfun (n - 1) B\<close>\<close>
| change_cfun _ T = raiseTYPE ("cont_consts: change_cfun", [T], [])
fun gen_add_consts prep_typ raw_decls thy = let val thy_ctxt = Proof_Context.init_global thy
fun is_cont_const (_, _, NoSyn) = false
| is_cont_const (_, _, Binder _) = false
| is_cont_const (b, T, mx) = let val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
cat_error msg ("in mixfix annotation for " ^ Binding.print b) in count_cfun T >= n end
fun transform (b, T, mx) = let val c = Sign.full_name thy b val c1 = Lexicon.mark_syntax c val c2 = Lexicon.mark_const c val xs = Name.invent_global "xa" (Mixfix.mixfix_args thy_ctxt mx) val trans_rules =
Syntax.Parse_Print_Rule
(Ast.mk_appl (Ast.Constant c1) (map Ast.Variable xs),
fold (fn x => fn t =>
Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable x])
xs (Ast.Constant c2)) ::
(if Mixfix.is_infix mx then [Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)] else []) in ((b, T, NoSyn), (c1, change_cfun (length xs) T, mx), trans_rules) end
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
