src/HOLCF/cont_consts.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5700 491944c2fb12
child 11651 201b3f76c7b7
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/cont_consts.ML
     2     ID:         $Id$
     3     Author:     Tobias Mayr and David von Oheimb
     4 
     5 Theory extender for consts section.
     6 *)
     7 
     8 structure ContConsts =
     9 struct
    10 
    11 local
    12 
    13 open HOLCFLogic;
    14 
    15 exception Impossible of string;
    16 fun Imposs msg = raise Impossible ("ContConst:"^msg);
    17 fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    18 fun upd_first  f (x,y,z) = (f x,   y,   z);
    19 fun upd_second f (x,y,z) = (  x, f y,   z);
    20 fun upd_third  f (x,y,z) = (  x,   y, f z);
    21 
    22 fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
    23   let fun filt []      = ([],[])
    24         | filt (x::xs) = let val (ys,zs) = filt xs in
    25 			 if pred x then (x::ys,zs) else (ys,x::zs) end
    26   in filt end;
    27 
    28 fun change_arrow 0 T               = T
    29 |   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
    30 |   change_arrow _ _               = Imposs "change_arrow";
    31 
    32 fun trans_rules name2 name1 n mx = let
    33   fun argnames _ 0 = []
    34   |   argnames c n = chr c::argnames (c+1) (n-1);
    35   val vnames = argnames (ord "A") n;
    36   val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
    37   in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames),
    38 			  foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") 
    39 						[t,Variable arg]))
    40 			  (Constant name1,vnames))]
    41      @(case mx of InfixlName _ => [extra_parse_rule] 
    42                 | InfixrName _ => [extra_parse_rule] | _ => []) end; 
    43 
    44 
    45 (* transforming infix/mixfix declarations of constants with type ...->...
    46    a declaration of such a constant is transformed to a normal declaration with 
    47    an internal name, the same type, and nofix. Additionally, a purely syntactic
    48    declaration with the original name, type ...=>..., and the original mixfix
    49    is generated and connected to the other declaration via some translation.
    50 *)
    51 fun fix_mixfix (syn                     , T, mx as Infixl           p ) = 
    52 	       (Syntax.const_name syn mx, T,       InfixlName (syn, p))
    53   | fix_mixfix (syn                     , T, mx as Infixr           p ) = 
    54 	       (Syntax.const_name syn mx, T,       InfixrName (syn, p))
    55   | fix_mixfix decl = decl;
    56 fun transform decl = let 
    57 	val (c, T, mx) = fix_mixfix decl; 
    58 	val c2 = "@"^c;
    59 	val n  = Syntax.mixfix_args mx
    60     in	   ((c ,               T,NoSyn),
    61 	    (c2,change_arrow n T,mx   ),
    62 	    trans_rules c2 c n mx) end;
    63 
    64 fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
    65 |   cfun_arity _               = 0;
    66 
    67 fun is_contconst (_,_,NoSyn   ) = false
    68 |   is_contconst (_,_,Binder _) = false
    69 |   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    70 			 handle ERROR => error ("in mixfix annotation for " ^
    71 			 		       quote (Syntax.const_name c mx));
    72 
    73 in (* local *)
    74 
    75 fun ext_consts prep_typ raw_decls thy =
    76 let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
    77     val (contconst_decls, normal_decls) = filter2 is_contconst decls;
    78     val transformed_decls = map transform contconst_decls;
    79 in thy |> Theory.add_consts_i                    normal_decls
    80        |> Theory.add_consts_i        (map first  transformed_decls)
    81        |> Theory.add_syntax_i        (map second transformed_decls)
    82        |> Theory.add_trrules_i (flat (map third  transformed_decls))
    83     handle ERROR =>
    84       error ("The error(s) above occurred in (cont)consts section")
    85 end;
    86 
    87 fun cert_typ sg typ =
    88   ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
    89 
    90 val add_consts   = ext_consts read_ctyp;
    91 val add_consts_i = ext_consts cert_typ;
    92 
    93 end; (* local *)
    94 
    95 end; (* struct *)
    96 
    97 val _ = ThySyn.add_syntax []
    98     [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
    99