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