1(* Title: HOL/HOLCF/Tools/cont_consts.ML 2 Author: Tobias Mayr, David von Oheimb, and Markus Wenzel 3 4HOLCF version of consts: handle continuous function types in mixfix 5syntax. 6*) 7 8signature CONT_CONSTS = 9sig 10 val add_consts: (binding * typ * mixfix) list -> theory -> theory 11 val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory 12end 13 14structure Cont_Consts: CONT_CONSTS = 15struct 16 17 18(* misc utils *) 19 20fun change_arrow 0 T = T 21 | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T]) 22 | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) 23 24fun trans_rules name2 name1 n mx = 25 let 26 val vnames = Name.invent Name.context "a" n 27 val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1) 28 in 29 [Syntax.Parse_Print_Rule 30 (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames), 31 fold (fn a => fn t => 32 Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a]) 33 vnames (Ast.Constant name1))] @ 34 (case mx of 35 Infix _ => [extra_parse_rule] 36 | Infixl _ => [extra_parse_rule] 37 | Infixr _ => [extra_parse_rule] 38 | _ => []) 39 end 40 41 42(* transforming infix/mixfix declarations of constants with type ...->... 43 a declaration of such a constant is transformed to a normal declaration with 44 an internal name, the same type, and nofix. Additionally, a purely syntactic 45 declaration with the original name, type ...=>..., and the original mixfix 46 is generated and connected to the other declaration via some translation. 47*) 48fun transform thy (c, T, mx) = 49 let 50 fun syntax b = Lexicon.mark_const (Sign.full_bname thy b) 51 val c1 = Binding.name_of c 52 val c2 = c1 ^ "_cont_syntax" 53 val n = Mixfix.mixfix_args mx 54 in 55 ((c, T, NoSyn), 56 (Binding.name c2, change_arrow n T, mx), 57 trans_rules (syntax c2) (syntax c1) n mx) 58 end 59 60fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0 61 | cfun_arity _ = 0 62 63fun is_contconst (_, _, NoSyn) = false 64 | is_contconst (_, _, Binder _) = false (* FIXME ? *) 65 | is_contconst (c, T, mx) = 66 let 67 val n = Mixfix.mixfix_args mx handle ERROR msg => 68 cat_error msg ("in mixfix annotation for " ^ Binding.print c) 69 in cfun_arity T >= n end 70 71 72(* add_consts *) 73 74local 75 76fun gen_add_consts prep_typ raw_decls thy = 77 let 78 val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls 79 val (contconst_decls, normal_decls) = List.partition is_contconst decls 80 val transformed_decls = map (transform thy) contconst_decls 81 in 82 thy 83 |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) 84 |> Sign.add_trrules (maps #3 transformed_decls) 85 end 86 87in 88 89val add_consts = gen_add_consts Sign.certify_typ 90val add_consts_cmd = gen_add_consts Syntax.read_typ_global 91 92end 93 94end 95