HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
authorwenzelm
Tue Nov 04 17:12:13 1997 +0100 (1997-11-04)
changeset 41292fd816aa6206
parent 4128 42584a53a3e7
child 4130 9fac2370a2f4
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
src/HOLCF/HOLCFLogic.ML
src/HOLCF/IsaMakefile
src/HOLCF/ROOT.ML
src/HOLCF/cont_consts.ML
src/HOLCF/contconsts.ML
src/HOLCF/holcf_logic.ML
     1.1 --- a/src/HOLCF/HOLCFLogic.ML	Tue Nov 04 16:57:52 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,66 +0,0 @@
     1.4 -(*  Title:      HOLCF/HOLCFLogic.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     David von Oheimb
     1.7 -
     1.8 -Abstract syntax operations for HOLCF.
     1.9 -*)
    1.10 -
    1.11 -infixr 6 ->>;
    1.12 -
    1.13 -signature HOLCFLOGIC =
    1.14 -sig
    1.15 -  val mk_btyp: string -> typ * typ -> typ
    1.16 -  val mk_prodT:          typ * typ -> typ
    1.17 -  val mk_not:  term -> term
    1.18 -
    1.19 -  val HOLCF_sg: Sign.sg
    1.20 -  val pcpoC: class
    1.21 -  val pcpoS: sort
    1.22 -  val mk_TFree: string -> typ
    1.23 -  val cfun_arrow: string
    1.24 -  val ->>      : typ * typ -> typ
    1.25 -  val mk_ssumT : typ * typ -> typ
    1.26 -  val mk_sprodT: typ * typ -> typ
    1.27 -  val mk_uT: typ -> typ
    1.28 -  val trT: typ
    1.29 -  val oneT: typ
    1.30 -
    1.31 -end;
    1.32 -
    1.33 -
    1.34 -structure HOLCFLogic: HOLCFLOGIC =
    1.35 -struct
    1.36 -
    1.37 -local
    1.38 -
    1.39 -  open HOLogic;
    1.40 -
    1.41 -in
    1.42 -
    1.43 -fun mk_btyp t (S,T) = Type (t,[S,T]);
    1.44 -val mk_prodT = mk_btyp "*";
    1.45 -
    1.46 -fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
    1.47 -
    1.48 -(* basics *)
    1.49 -
    1.50 -val HOLCF_sg    = sign_of HOLCF.thy;
    1.51 -val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
    1.52 -val pcpoS       = [pcpoC];
    1.53 -fun mk_TFree s  = TFree ("'"^s, pcpoS);
    1.54 -
    1.55 -(*cfun, ssum, sprod, u, tr, one *)
    1.56 -
    1.57 -local val intern = Sign.intern_tycon HOLCF_sg;
    1.58 -in
    1.59 -val cfun_arrow = intern "->";
    1.60 -val op   ->>  = mk_btyp cfun_arrow;
    1.61 -val mk_ssumT  = mk_btyp (intern "++");
    1.62 -val mk_sprodT = mk_btyp (intern "**");
    1.63 -fun mk_uT T   = Type (intern "u"  ,[T]);
    1.64 -val trT       = Type (intern "tr" ,[ ]);
    1.65 -val oneT      = Type (intern "one",[ ]);
    1.66 -end;
    1.67 -
    1.68 -end; (* local *)
    1.69 -end; (* struct *)
     2.1 --- a/src/HOLCF/IsaMakefile	Tue Nov 04 16:57:52 1997 +0100
     2.2 +++ b/src/HOLCF/IsaMakefile	Tue Nov 04 17:12:13 1997 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4  ONLYTHYS = 
     2.5  
     2.6  FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \
     2.7 -	HOLCFLogic.ML contconsts.ML \
     2.8 +	holcf_logic.ML cont_consts.ML \
     2.9          domain/library.ML  domain/syntax.ML   domain/axioms.ML \
    2.10          domain/theorems.ML domain/extender.ML domain/interface.ML
    2.11  
     3.1 --- a/src/HOLCF/ROOT.ML	Tue Nov 04 16:57:52 1997 +0100
     3.2 +++ b/src/HOLCF/ROOT.ML	Tue Nov 04 17:12:13 1997 +0100
     3.3 @@ -14,8 +14,8 @@
     3.4  
     3.5  use_thy "HOLCF";
     3.6  
     3.7 -use "HOLCFLogic.ML";
     3.8 -use "contconsts.ML";
     3.9 +use "holcf_logic.ML";
    3.10 +use "cont_consts.ML";
    3.11  
    3.12  (* domain package *)
    3.13  use "domain/library.ML";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/cont_consts.ML	Tue Nov 04 17:12:13 1997 +0100
     4.3 @@ -0,0 +1,99 @@
     4.4 +(*  Title:      HOLCF/cont_consts.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Mayr and David von Oheimb
     4.7 +
     4.8 +Theory extender for consts section.
     4.9 +*)
    4.10 +
    4.11 +structure ContConsts =
    4.12 +struct
    4.13 +
    4.14 +local
    4.15 +
    4.16 +open HOLCFLogic;
    4.17 +
    4.18 +exception Impossible of string;
    4.19 +fun Imposs msg = raise Impossible ("ContConst:"^msg);
    4.20 +fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    4.21 +fun upd_first  f (x,y,z) = (f x,   y,   z);
    4.22 +fun upd_second f (x,y,z) = (  x, f y,   z);
    4.23 +fun upd_third  f (x,y,z) = (  x,   y, f z);
    4.24 +
    4.25 +fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
    4.26 +  let fun filt []      = ([],[])
    4.27 +        | filt (x::xs) = let val (ys,zs) = filt xs in
    4.28 +			 if pred x then (x::ys,zs) else (ys,x::zs) end
    4.29 +  in filt end;
    4.30 +
    4.31 +fun change_arrow 0 T               = T
    4.32 +|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
    4.33 +|   change_arrow _ _               = Imposs "change_arrow";
    4.34 +
    4.35 +fun trans_rules name2 name1 n mx = let
    4.36 +  fun argnames _ 0 = []
    4.37 +  |   argnames c n = chr c::argnames (c+1) (n-1);
    4.38 +  val vnames = argnames (ord "A") n;
    4.39 +  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
    4.40 +  in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
    4.41 +			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
    4.42 +						[t,Variable arg]))
    4.43 +			  (Constant name1,vnames))]
    4.44 +     @(case mx of InfixlName _ => [extra_parse_rule] 
    4.45 +                | InfixrName _ => [extra_parse_rule] | _ => []) end; 
    4.46 +
    4.47 +
    4.48 +(* transforming infix/mixfix declarations of constants with type ...->...
    4.49 +   a declaration of such a constant is transformed to a normal declaration with 
    4.50 +   an internal name, the same type, and nofix. Additionally, a purely syntactic
    4.51 +   declaration with the original name, type ...=>..., and the original mixfix
    4.52 +   is generated and connected to the other declaration via some translation.
    4.53 +*)
    4.54 +fun fix_mixfix (syn                     , T, mx as Infixl           p ) = 
    4.55 +	       (Syntax.const_name syn mx, T,       InfixlName (syn, p))
    4.56 +  | fix_mixfix (syn                     , T, mx as Infixr           p ) = 
    4.57 +	       (Syntax.const_name syn mx, T,       InfixrName (syn, p))
    4.58 +  | fix_mixfix decl = decl;
    4.59 +fun transform decl = let 
    4.60 +	val (c, T, mx) = fix_mixfix decl; 
    4.61 +	val c2 = "@"^c;
    4.62 +	val n  = Syntax.mixfix_args mx
    4.63 +    in	   ((c ,               T,NoSyn),
    4.64 +	    (c2,change_arrow n T,mx   ),
    4.65 +	    trans_rules c2 c n mx) end;
    4.66 +
    4.67 +fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
    4.68 +|   cfun_arity _               = 0;
    4.69 +
    4.70 +fun is_contconst (_,_,NoSyn   ) = false
    4.71 +|   is_contconst (_,_,Binder _) = false
    4.72 +|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    4.73 +			 handle ERROR => error ("in mixfix annotation for " ^
    4.74 +			 		       quote (Syntax.const_name c mx));
    4.75 +
    4.76 +in (* local *)
    4.77 +
    4.78 +fun ext_consts prep_typ raw_decls thy =
    4.79 +let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
    4.80 +    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
    4.81 +    val transformed_decls = map transform contconst_decls;
    4.82 +in thy |> Theory.add_consts_i                    normal_decls
    4.83 +       |> Theory.add_consts_i        (map first  transformed_decls)
    4.84 +       |> Theory.add_syntax_i        (map second transformed_decls)
    4.85 +       |> Theory.add_trrules_i (flat (map third  transformed_decls))
    4.86 +    handle ERROR =>
    4.87 +      error ("The error(s) above occurred in (cont)consts section")
    4.88 +end;
    4.89 +
    4.90 +fun cert_typ sg typ =
    4.91 +  ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
    4.92 +
    4.93 +val add_consts   = ext_consts read_ctyp;
    4.94 +val add_consts_i = ext_consts cert_typ;
    4.95 +
    4.96 +end; (* local *)
    4.97 +
    4.98 +end; (* struct *)
    4.99 +
   4.100 +val _ = ThySyn.add_syntax []
   4.101 +    [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
   4.102 +
     5.1 --- a/src/HOLCF/contconsts.ML	Tue Nov 04 16:57:52 1997 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,99 +0,0 @@
     5.4 -(*  Title:      HOLCF/contconsts.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Mayr and David von Oheimb
     5.7 -
     5.8 -theory extender for consts section
     5.9 -*)
    5.10 -
    5.11 -structure ContConsts =
    5.12 -struct
    5.13 -
    5.14 -local
    5.15 -
    5.16 -open HOLCFLogic;
    5.17 -
    5.18 -exception Impossible of string;
    5.19 -fun Imposs msg = raise Impossible ("ContConst:"^msg);
    5.20 -fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    5.21 -fun upd_first  f (x,y,z) = (f x,   y,   z);
    5.22 -fun upd_second f (x,y,z) = (  x, f y,   z);
    5.23 -fun upd_third  f (x,y,z) = (  x,   y, f z);
    5.24 -
    5.25 -fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
    5.26 -  let fun filt []      = ([],[])
    5.27 -        | filt (x::xs) = let val (ys,zs) = filt xs in
    5.28 -			 if pred x then (x::ys,zs) else (ys,x::zs) end
    5.29 -  in filt end;
    5.30 -
    5.31 -fun change_arrow 0 T               = T
    5.32 -|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
    5.33 -|   change_arrow _ _               = Imposs "change_arrow";
    5.34 -
    5.35 -fun trans_rules name2 name1 n mx = let
    5.36 -  fun argnames _ 0 = []
    5.37 -  |   argnames c n = chr c::argnames (c+1) (n-1);
    5.38 -  val vnames = argnames (ord "A") n;
    5.39 -  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
    5.40 -  in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
    5.41 -			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
    5.42 -						[t,Variable arg]))
    5.43 -			  (Constant name1,vnames))]
    5.44 -     @(case mx of InfixlName _ => [extra_parse_rule] 
    5.45 -                | InfixrName _ => [extra_parse_rule] | _ => []) end; 
    5.46 -
    5.47 -
    5.48 -(* transforming infix/mixfix declarations of constants with type ...->...
    5.49 -   a declaration of such a constant is transformed to a normal declaration with 
    5.50 -   an internal name, the same type, and nofix. Additionally, a purely syntactic
    5.51 -   declaration with the original name, type ...=>..., and the original mixfix
    5.52 -   is generated and connected to the other declaration via some translation.
    5.53 -*)
    5.54 -fun fix_mixfix (syn                     , T, mx as Infixl           p ) = 
    5.55 -	       (Syntax.const_name syn mx, T,       InfixlName (syn, p))
    5.56 -  | fix_mixfix (syn                     , T, mx as Infixr           p ) = 
    5.57 -	       (Syntax.const_name syn mx, T,       InfixrName (syn, p))
    5.58 -  | fix_mixfix decl = decl;
    5.59 -fun transform decl = let 
    5.60 -	val (c, T, mx) = fix_mixfix decl; 
    5.61 -	val c2 = "@"^c;
    5.62 -	val n  = Syntax.mixfix_args mx
    5.63 -    in	   ((c ,               T,NoSyn),
    5.64 -	    (c2,change_arrow n T,mx   ),
    5.65 -	    trans_rules c2 c n mx) end;
    5.66 -
    5.67 -fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
    5.68 -|   cfun_arity _               = 0;
    5.69 -
    5.70 -fun is_contconst (_,_,NoSyn   ) = false
    5.71 -|   is_contconst (_,_,Binder _) = false
    5.72 -|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    5.73 -			 handle ERROR => error ("in mixfix annotation for " ^
    5.74 -			 		       quote (Syntax.const_name c mx));
    5.75 -
    5.76 -in (* local *)
    5.77 -
    5.78 -fun ext_consts prep_typ raw_decls thy =
    5.79 -let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
    5.80 -    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
    5.81 -    val transformed_decls = map transform contconst_decls;
    5.82 -in thy |> Theory.add_consts_i                    normal_decls
    5.83 -       |> Theory.add_consts_i        (map first  transformed_decls)
    5.84 -       |> Theory.add_syntax_i        (map second transformed_decls)
    5.85 -       |> Theory.add_trrules_i (flat (map third  transformed_decls))
    5.86 -    handle ERROR =>
    5.87 -      error ("The error(s) above occurred in (cont)consts section")
    5.88 -end;
    5.89 -
    5.90 -fun cert_typ sg typ =
    5.91 -  ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
    5.92 -
    5.93 -val add_consts   = ext_consts read_ctyp;
    5.94 -val add_consts_i = ext_consts cert_typ;
    5.95 -
    5.96 -end; (* local *)
    5.97 -
    5.98 -end; (* struct *)
    5.99 -
   5.100 -val _ = ThySyn.add_syntax []
   5.101 -    [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
   5.102 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/holcf_logic.ML	Tue Nov 04 17:12:13 1997 +0100
     6.3 @@ -0,0 +1,66 @@
     6.4 +(*  Title:      HOLCF/holcf_logic.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     David von Oheimb
     6.7 +
     6.8 +Abstract syntax operations for HOLCF.
     6.9 +*)
    6.10 +
    6.11 +infixr 6 ->>;
    6.12 +
    6.13 +signature HOLCF_LOGIC =
    6.14 +sig
    6.15 +  val mk_btyp: string -> typ * typ -> typ
    6.16 +  val mk_prodT:          typ * typ -> typ
    6.17 +  val mk_not:  term -> term
    6.18 +
    6.19 +  val HOLCF_sg: Sign.sg
    6.20 +  val pcpoC: class
    6.21 +  val pcpoS: sort
    6.22 +  val mk_TFree: string -> typ
    6.23 +  val cfun_arrow: string
    6.24 +  val ->>      : typ * typ -> typ
    6.25 +  val mk_ssumT : typ * typ -> typ
    6.26 +  val mk_sprodT: typ * typ -> typ
    6.27 +  val mk_uT: typ -> typ
    6.28 +  val trT: typ
    6.29 +  val oneT: typ
    6.30 +
    6.31 +end;
    6.32 +
    6.33 +
    6.34 +structure HOLCFLogic: HOLCF_LOGIC =
    6.35 +struct
    6.36 +
    6.37 +local
    6.38 +
    6.39 +  open HOLogic;
    6.40 +
    6.41 +in
    6.42 +
    6.43 +fun mk_btyp t (S,T) = Type (t,[S,T]);
    6.44 +val mk_prodT = mk_btyp "*";
    6.45 +
    6.46 +fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
    6.47 +
    6.48 +(* basics *)
    6.49 +
    6.50 +val HOLCF_sg    = sign_of HOLCF.thy;
    6.51 +val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
    6.52 +val pcpoS       = [pcpoC];
    6.53 +fun mk_TFree s  = TFree ("'"^s, pcpoS);
    6.54 +
    6.55 +(*cfun, ssum, sprod, u, tr, one *)
    6.56 +
    6.57 +local val intern = Sign.intern_tycon HOLCF_sg;
    6.58 +in
    6.59 +val cfun_arrow = intern "->";
    6.60 +val op   ->>  = mk_btyp cfun_arrow;
    6.61 +val mk_ssumT  = mk_btyp (intern "++");
    6.62 +val mk_sprodT = mk_btyp (intern "**");
    6.63 +fun mk_uT T   = Type (intern "u"  ,[T]);
    6.64 +val trT       = Type (intern "tr" ,[ ]);
    6.65 +val oneT      = Type (intern "one",[ ]);
    6.66 +end;
    6.67 +
    6.68 +end; (* local *)
    6.69 +end; (* struct *)