src/HOLCF/cont_consts.ML
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12876 a70df1e5bf10
child 14682 a5072752114c
permissions -rw-r--r--
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOLCF/cont_consts.ML
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
     3
    Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
12030
wenzelm
parents: 11651
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     5
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
     6
HOLCF version of consts/constdefs: handle continuous function types in
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
     7
mixfix syntax.
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     8
*)
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     9
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    10
signature CONT_CONSTS =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    11
sig
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    12
  val add_consts: (bstring * string * mixfix) list -> theory -> theory
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    13
  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    14
  val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    15
  val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    16
end;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    17
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    18
structure ContConsts: CONT_CONSTS =
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    19
struct
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    20
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    21
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    22
(* misc utils *)
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    23
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    24
open HOLCFLogic;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    25
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    26
fun first  (x,_,_) = x;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    27
fun second (_,x,_) = x;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    28
fun third  (_,_,x) = x;
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    29
fun upd_first  f (x,y,z) = (f x,   y,   z);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    30
fun upd_second f (x,y,z) = (  x, f y,   z);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    31
fun upd_third  f (x,y,z) = (  x,   y, f z);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    32
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    33
fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    34
  let fun filt []      = ([],[])
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    35
        | filt (x::xs) = let val (ys,zs) = filt xs in
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    36
                         if pred x then (x::ys,zs) else (ys,x::zs) end
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    37
  in filt end;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    38
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    39
fun change_arrow 0 T               = T
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    40
|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    41
|   change_arrow _ _               = sys_error "cont_consts: change_arrow";
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    42
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    43
fun trans_rules name2 name1 n mx = let
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    44
  fun argnames _ 0 = []
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    45
  |   argnames c n = chr c::argnames (c+1) (n-1);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    46
  val vnames = argnames (ord "A") n;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    47
  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
5700
491944c2fb12 fixed Syntax module;
wenzelm
parents: 5291
diff changeset
    48
  in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames),
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    49
                          foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun")
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    50
                                                [t,Variable arg]))
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    51
                          (Constant name1,vnames))]
11651
201b3f76c7b7 support non-oriented infix;
wenzelm
parents: 5700
diff changeset
    52
     @(case mx of InfixName _ => [extra_parse_rule]
201b3f76c7b7 support non-oriented infix;
wenzelm
parents: 5700
diff changeset
    53
                | InfixlName _ => [extra_parse_rule]
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    54
                | InfixrName _ => [extra_parse_rule] | _ => []) end;
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    55
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    56
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    57
(* transforming infix/mixfix declarations of constants with type ...->...
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    58
   a declaration of such a constant is transformed to a normal declaration with
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    59
   an internal name, the same type, and nofix. Additionally, a purely syntactic
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    60
   declaration with the original name, type ...=>..., and the original mixfix
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    61
   is generated and connected to the other declaration via some translation.
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    62
*)
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    63
fun fix_mixfix (syn                     , T, mx as Infix           p ) =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    64
               (Syntax.const_name syn mx, T,       InfixName (syn, p))
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    65
  | fix_mixfix (syn                     , T, mx as Infixl           p ) =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    66
               (Syntax.const_name syn mx, T,       InfixlName (syn, p))
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    67
  | fix_mixfix (syn                     , T, mx as Infixr           p ) =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    68
               (Syntax.const_name syn mx, T,       InfixrName (syn, p))
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    69
  | fix_mixfix decl = decl;
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    70
fun transform decl = let
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    71
        val (c, T, mx) = fix_mixfix decl;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    72
        val c2 = "_cont_" ^ c;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    73
        val n  = Syntax.mixfix_args mx
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    74
    in     ((c ,               T,NoSyn),
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    75
            (c2,change_arrow n T,mx   ),
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    76
            trans_rules c2 c n mx) end;
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    77
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    78
fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    79
|   cfun_arity _               = 0;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    80
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    81
fun is_contconst (_,_,NoSyn   ) = false
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    82
|   is_contconst (_,_,Binder _) = false
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    83
|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    84
                         handle ERROR => error ("in mixfix annotation for " ^
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    85
                                               quote (Syntax.const_name c mx));
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    86
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    87
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    88
(* add_consts(_i) *)
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    89
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    90
fun gen_add_consts prep_typ raw_decls thy =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    91
  let
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    92
    val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls;
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    93
    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    94
    val transformed_decls = map transform contconst_decls;
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    95
  in
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    96
    thy
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    97
    |> Theory.add_consts_i normal_decls
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    98
    |> Theory.add_consts_i (map first transformed_decls)
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
    99
    |> Theory.add_syntax_i (map second transformed_decls)
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   100
    |> Theory.add_trrules_i (flat (map third transformed_decls))
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   101
  end;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   102
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   103
val add_consts = gen_add_consts Thm.read_ctyp;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   104
val add_consts_i = gen_add_consts Thm.ctyp_of;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   105
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   106
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   107
(* add_constdefs(_i) *)
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   108
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   109
fun gen_add_constdefs consts defs args thy =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   110
  thy
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   111
  |> consts (map fst args)
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   112
  |> defs (false, map (fn ((c, _, mx), s) =>
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12625
diff changeset
   113
    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   114
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   115
fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   116
fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args;
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   117
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   118
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   119
(* outer syntax *)
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   120
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   121
local structure P = OuterParse and K = OuterSyntax.Keyword in
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   122
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   123
val constsP =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   124
  OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12625
diff changeset
   125
    (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   126
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   127
val constdefsP =
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   128
  OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12625
diff changeset
   129
    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs));
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   130
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   131
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   132
val _ = OuterSyntax.add_parsers [constsP, constdefsP];
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   133
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
   134
end;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
   135
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
   136
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   137
(* old-style theory syntax *)
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
   138
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
   139
val _ = ThySyn.add_syntax []
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   140
  [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
   141
12625
425ca8613a1d Isar version;
wenzelm
parents: 12030
diff changeset
   142
end;