src/HOLCF/Tools/cont_consts.ML
author huffman
Tue, 02 Mar 2010 17:21:10 -0800
changeset 35525 fa231b86cb1e
parent 35262 9ea4445d2ccf
child 36960 01594f816e3a
permissions -rw-r--r--
proper names for types cfun, sprod, ssum
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOLCF/Tools/cont_consts.ML
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     2
    Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
HOLCF version of consts: handle continuous function types in mixfix
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
syntax.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     8
signature CONT_CONSTS =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     9
sig
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    10
  val add_consts: (binding * typ * mixfix) list -> theory -> theory
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    11
  val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    12
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    13
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    14
structure Cont_Consts: CONT_CONSTS =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    15
struct
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
(* misc utils *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    19
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    20
fun change_arrow 0 T = T
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    21
  | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T])
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    22
  | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []);
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
33245
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    24
fun trans_rules name2 name1 n mx =
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    25
  let
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    26
    val vnames = Name.invents Name.context "a" n;
33245
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    27
    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    28
  in
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    29
    [Syntax.ParsePrintRule
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    30
      (Syntax.mk_appl (Constant name2) (map Variable vnames),
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    31
        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a])
33245
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    32
          vnames (Constant name1))] @
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    33
    (case mx of
35130
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
    34
      Infix _ => [extra_parse_rule]
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
    35
    | Infixl _ => [extra_parse_rule]
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
    36
    | Infixr _ => [extra_parse_rule]
33245
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    37
    | _ => [])
65232054ffd0 eliminated some old folds;
wenzelm
parents: 31023
diff changeset
    38
  end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    39
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
(* transforming infix/mixfix declarations of constants with type ...->...
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    42
   a declaration of such a constant is transformed to a normal declaration with
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
   an internal name, the same type, and nofix. Additionally, a purely syntactic
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
   declaration with the original name, type ...=>..., and the original mixfix
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
   is generated and connected to the other declaration via some translation.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
*)
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    47
fun transform thy (c, T, mx) =
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    48
  let
35262
9ea4445d2ccf slightly more abstract syntax mark/unmark operations;
wenzelm
parents: 35257
diff changeset
    49
    fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    50
    val c1 = Binding.name_of c;
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    51
    val c2 = c1 ^ "_cont_syntax";
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    52
    val n = Syntax.mixfix_args mx;
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    53
  in
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    54
    ((c, T, NoSyn),
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    55
      (Binding.name c2, change_arrow n T, mx),
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    56
      trans_rules (syntax c2) (syntax c1) n mx)
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    57
  end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35262
diff changeset
    59
fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    60
  | cfun_arity _ = 0;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    62
fun is_contconst (_, _, NoSyn) = false
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    63
  | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    64
  | is_contconst (c, T, mx) =
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    65
      let
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    66
        val n = Syntax.mixfix_args mx handle ERROR msg =>
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    67
          cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c));
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    68
      in cfun_arity T >= n end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    70
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    71
(* add_consts *)
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    72
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    73
local
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
fun gen_add_consts prep_typ raw_decls thy =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
  let
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    77
    val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    78
    val (contconst_decls, normal_decls) = List.partition is_contconst decls;
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    79
    val transformed_decls = map (transform thy) contconst_decls;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    80
  in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    81
    thy
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    82
    |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    83
    |> Sign.add_trrules_i (maps #3 transformed_decls)
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
  end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    85
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    86
in
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    87
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    88
val add_consts = gen_add_consts Sign.certify_typ;
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    89
val add_consts_cmd = gen_add_consts Syntax.read_typ_global;
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    90
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
    91
end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    92
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    93
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    94
(* outer syntax *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    95
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    96
local structure P = OuterParse and K = OuterKeyword in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    97
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24707
diff changeset
    98
val _ =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    99
  OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
35257
3e5980f612d9 adapted to authentic syntax;
wenzelm
parents: 35130
diff changeset
   100
    (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   101
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   102
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   103
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   104
end;