src/HOLCF/Tools/cont_consts.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24707 dfeb98f84e93
child 24867 e5b55d7be9bb
permissions -rw-r--r--
filtering out some package theorems
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
    ID:         $Id$
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
HOLCF version of consts: handle continuous function types in mixfix
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
syntax.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     8
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     9
signature CONT_CONSTS =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    10
sig
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    11
  val add_consts: (bstring * string * mixfix) list -> theory -> theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    12
  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    13
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    14
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    15
structure ContConsts: CONT_CONSTS =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
struct
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    19
(* misc utils *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    20
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    21
open HOLCFLogic;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
fun first  (x,_,_) = x;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    24
fun second (_,x,_) = x;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    25
fun third  (_,_,x) = x;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    26
fun upd_first  f (x,y,z) = (f x,   y,   z);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    27
fun upd_second f (x,y,z) = (  x, f y,   z);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    28
fun upd_third  f (x,y,z) = (  x,   y, f z);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    29
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    30
fun change_arrow 0 T               = T
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    31
|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    32
|   change_arrow _ _               = sys_error "cont_consts: change_arrow";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    33
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    34
fun trans_rules name2 name1 n mx = let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    35
  fun argnames _ 0 = []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    36
  |   argnames c n = chr c::argnames (c+1) (n-1);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    37
  val vnames = argnames (ord "A") n;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    38
  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    39
  in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
                          Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun")
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
                                                [t,Variable arg]))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    42
                          (Constant name1,vnames))]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
     @(case mx of InfixName _ => [extra_parse_rule]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
                | InfixlName _ => [extra_parse_rule]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
                | InfixrName _ => [extra_parse_rule] | _ => []) end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    47
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    48
(* transforming infix/mixfix declarations of constants with type ...->...
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    49
   a declaration of such a constant is transformed to a normal declaration with
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    50
   an internal name, the same type, and nofix. Additionally, a purely syntactic
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    51
   declaration with the original name, type ...=>..., and the original mixfix
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    52
   is generated and connected to the other declaration via some translation.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    53
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    54
fun fix_mixfix (syn                     , T, mx as Infix           p ) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    55
               (Syntax.const_name syn mx, T,       InfixName (syn, p))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    56
  | fix_mixfix (syn                     , T, mx as Infixl           p ) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    57
               (Syntax.const_name syn mx, T,       InfixlName (syn, p))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
  | fix_mixfix (syn                     , T, mx as Infixr           p ) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    59
               (Syntax.const_name syn mx, T,       InfixrName (syn, p))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
  | fix_mixfix decl = decl;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
fun transform decl = let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    62
        val (c, T, mx) = fix_mixfix decl;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    63
        val c2 = "_cont_" ^ c;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    64
        val n  = Syntax.mixfix_args mx
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    65
    in     ((c ,               T,NoSyn),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    66
            (c2,change_arrow n T,mx   ),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    67
            trans_rules c2 c n mx) end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    68
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    70
|   cfun_arity _               = 0;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    71
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    72
fun is_contconst (_,_,NoSyn   ) = false
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    73
|   is_contconst (_,_,Binder _) = false
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
                         handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
                                               quote (Syntax.const_name c mx));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    77
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    78
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    79
(* add_consts(_i) *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    80
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    81
fun gen_add_consts prep_typ raw_decls thy =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    82
  let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    83
    val decls = map (upd_second (prep_typ thy)) raw_decls;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
    val (contconst_decls, normal_decls) = List.partition is_contconst decls;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    85
    val transformed_decls = map transform contconst_decls;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    86
  in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    87
    thy
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
    |> Sign.add_consts_i normal_decls
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    89
    |> Sign.add_consts_i (map first transformed_decls)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    90
    |> Sign.add_syntax_i (map second transformed_decls)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    91
    |> Sign.add_trrules_i (List.concat (map third transformed_decls))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    92
  end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    93
24707
dfeb98f84e93 Syntax.parse/check/read;
wenzelm
parents: 23152
diff changeset
    94
val add_consts = gen_add_consts Syntax.read_typ_global;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    95
val add_consts_i = gen_add_consts Sign.certify_typ;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    96
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    97
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    98
(* outer syntax *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    99
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   100
local structure P = OuterParse and K = OuterKeyword in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   101
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   102
val constsP =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   103
  OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   104
    (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   105
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   106
val _ = OuterSyntax.add_parsers [constsP];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   107
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   108
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   109
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   110
end;