src/HOL/HOLCF/Tools/cont_consts.ML
author wenzelm
Sun Apr 03 21:59:33 2011 +0200 (2011-04-03)
changeset 42204 b3277168c1e7
parent 42151 4da4fc77664b
child 42224 578a51fae383
permissions -rw-r--r--
added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;
     1 (*  Title:      HOL/HOLCF/Tools/cont_consts.ML
     2     Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
     3 
     4 HOLCF version of consts: handle continuous function types in mixfix
     5 syntax.
     6 *)
     7 
     8 signature CONT_CONSTS =
     9 sig
    10   val add_consts: (binding * typ * mixfix) list -> theory -> theory
    11   val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
    12 end
    13 
    14 structure Cont_Consts: CONT_CONSTS =
    15 struct
    16 
    17 
    18 (* misc utils *)
    19 
    20 fun 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 
    24 fun trans_rules name2 name1 n mx =
    25   let
    26     val vnames = Name.invents Name.context "a" n
    27     val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
    28   in
    29     [Syntax.Parse_Print_Rule
    30       (Syntax.mk_appl (Constant name2) (map Variable vnames),
    31         fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
    32           vnames (Constant name1))] @
    33     (case mx of
    34       Infix _ => [extra_parse_rule]
    35     | Infixl _ => [extra_parse_rule]
    36     | Infixr _ => [extra_parse_rule]
    37     | _ => [])
    38   end
    39 
    40 
    41 (* transforming infix/mixfix declarations of constants with type ...->...
    42    a declaration of such a constant is transformed to a normal declaration with
    43    an internal name, the same type, and nofix. Additionally, a purely syntactic
    44    declaration with the original name, type ...=>..., and the original mixfix
    45    is generated and connected to the other declaration via some translation.
    46 *)
    47 fun transform thy (c, T, mx) =
    48   let
    49     fun syntax b = Syntax.mark_const (Sign.full_bname thy b)
    50     val c1 = Binding.name_of c
    51     val c2 = c1 ^ "_cont_syntax"
    52     val n = Syntax.mixfix_args mx
    53   in
    54     ((c, T, NoSyn),
    55       (Binding.name c2, change_arrow n T, mx),
    56       trans_rules (syntax c2) (syntax c1) n mx)
    57   end
    58 
    59 fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
    60   | cfun_arity _ = 0
    61 
    62 fun is_contconst (_, _, NoSyn) = false
    63   | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
    64   | is_contconst (c, T, mx) =
    65       let
    66         val n = Syntax.mixfix_args mx handle ERROR msg =>
    67           cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c))
    68       in cfun_arity T >= n end
    69 
    70 
    71 (* add_consts *)
    72 
    73 local
    74 
    75 fun gen_add_consts prep_typ raw_decls thy =
    76   let
    77     val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls
    78     val (contconst_decls, normal_decls) = List.partition is_contconst decls
    79     val transformed_decls = map (transform thy) contconst_decls
    80   in
    81     thy
    82     |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
    83     |> Sign.add_trrules (maps #3 transformed_decls)
    84   end
    85 
    86 in
    87 
    88 val add_consts = gen_add_consts Sign.certify_typ
    89 val add_consts_cmd = gen_add_consts Syntax.read_typ_global
    90 
    91 end
    92 
    93 end