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