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