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