# HG changeset patch
# User wenzelm
# Date 878659933 -3600
# Node ID 2fd816aa6206bdaa7e9d4d660df8c66bd9db858a
# Parent  42584a53a3e7837ee0d4ad7bb012bd56f0152aa3
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;

diff -r 42584a53a3e7 -r 2fd816aa6206 src/HOLCF/HOLCFLogic.ML
--- a/src/HOLCF/HOLCFLogic.ML	Tue Nov 04 16:57:52 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(*  Title:      HOLCF/HOLCFLogic.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-
-Abstract syntax operations for HOLCF.
-*)
-
-infixr 6 ->>;
-
-signature HOLCFLOGIC =
-sig
-  val mk_btyp: string -> typ * typ -> typ
-  val mk_prodT:          typ * typ -> typ
-  val mk_not:  term -> term
-
-  val HOLCF_sg: Sign.sg
-  val pcpoC: class
-  val pcpoS: sort
-  val mk_TFree: string -> typ
-  val cfun_arrow: string
-  val ->>      : typ * typ -> typ
-  val mk_ssumT : typ * typ -> typ
-  val mk_sprodT: typ * typ -> typ
-  val mk_uT: typ -> typ
-  val trT: typ
-  val oneT: typ
-
-end;
-
-
-structure HOLCFLogic: HOLCFLOGIC =
-struct
-
-local
-
-  open HOLogic;
-
-in
-
-fun mk_btyp t (S,T) = Type (t,[S,T]);
-val mk_prodT = mk_btyp "*";
-
-fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
-
-(* basics *)
-
-val HOLCF_sg    = sign_of HOLCF.thy;
-val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
-val pcpoS       = [pcpoC];
-fun mk_TFree s  = TFree ("'"^s, pcpoS);
-
-(*cfun, ssum, sprod, u, tr, one *)
-
-local val intern = Sign.intern_tycon HOLCF_sg;
-in
-val cfun_arrow = intern "->";
-val op   ->>  = mk_btyp cfun_arrow;
-val mk_ssumT  = mk_btyp (intern "++");
-val mk_sprodT = mk_btyp (intern "**");
-fun mk_uT T   = Type (intern "u"  ,[T]);
-val trT       = Type (intern "tr" ,[ ]);
-val oneT      = Type (intern "one",[ ]);
-end;
-
-end; (* local *)
-end; (* struct *)
diff -r 42584a53a3e7 -r 2fd816aa6206 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue Nov 04 16:57:52 1997 +0100
+++ b/src/HOLCF/IsaMakefile	Tue Nov 04 17:12:13 1997 +0100
@@ -22,7 +22,7 @@
 ONLYTHYS = 
 
 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \
-	HOLCFLogic.ML contconsts.ML \
+	holcf_logic.ML cont_consts.ML \
         domain/library.ML  domain/syntax.ML   domain/axioms.ML \
         domain/theorems.ML domain/extender.ML domain/interface.ML
 
diff -r 42584a53a3e7 -r 2fd816aa6206 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Tue Nov 04 16:57:52 1997 +0100
+++ b/src/HOLCF/ROOT.ML	Tue Nov 04 17:12:13 1997 +0100
@@ -14,8 +14,8 @@
 
 use_thy "HOLCF";
 
-use "HOLCFLogic.ML";
-use "contconsts.ML";
+use "holcf_logic.ML";
+use "cont_consts.ML";
 
 (* domain package *)
 use "domain/library.ML";
diff -r 42584a53a3e7 -r 2fd816aa6206 src/HOLCF/cont_consts.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/cont_consts.ML	Tue Nov 04 17:12:13 1997 +0100
@@ -0,0 +1,99 @@
+(*  Title:      HOLCF/cont_consts.ML
+    ID:         $Id$
+    Author:     Tobias Mayr and David von Oheimb
+
+Theory extender for consts section.
+*)
+
+structure ContConsts =
+struct
+
+local
+
+open HOLCFLogic;
+
+exception Impossible of string;
+fun Imposs msg = raise Impossible ("ContConst:"^msg);
+fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
+fun upd_first  f (x,y,z) = (f x,   y,   z);
+fun upd_second f (x,y,z) = (  x, f y,   z);
+fun upd_third  f (x,y,z) = (  x,   y, f z);
+
+fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
+  let fun filt []      = ([],[])
+        | filt (x::xs) = let val (ys,zs) = filt xs in
+			 if pred x then (x::ys,zs) else (ys,x::zs) end
+  in filt end;
+
+fun change_arrow 0 T               = T
+|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
+|   change_arrow _ _               = Imposs "change_arrow";
+
+fun trans_rules name2 name1 n mx = let
+  fun argnames _ 0 = []
+  |   argnames c n = chr c::argnames (c+1) (n-1);
+  val vnames = argnames (ord "A") n;
+  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
+  in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
+			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
+						[t,Variable arg]))
+			  (Constant name1,vnames))]
+     @(case mx of InfixlName _ => [extra_parse_rule] 
+                | InfixrName _ => [extra_parse_rule] | _ => []) end; 
+
+
+(* transforming infix/mixfix declarations of constants with type ...->...
+   a declaration of such a constant is transformed to a normal declaration with 
+   an internal name, the same type, and nofix. Additionally, a purely syntactic
+   declaration with the original name, type ...=>..., and the original mixfix
+   is generated and connected to the other declaration via some translation.
+*)
+fun fix_mixfix (syn                     , T, mx as Infixl           p ) = 
+	       (Syntax.const_name syn mx, T,       InfixlName (syn, p))
+  | fix_mixfix (syn                     , T, mx as Infixr           p ) = 
+	       (Syntax.const_name syn mx, T,       InfixrName (syn, p))
+  | fix_mixfix decl = decl;
+fun transform decl = let 
+	val (c, T, mx) = fix_mixfix decl; 
+	val c2 = "@"^c;
+	val n  = Syntax.mixfix_args mx
+    in	   ((c ,               T,NoSyn),
+	    (c2,change_arrow n T,mx   ),
+	    trans_rules c2 c n mx) end;
+
+fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
+|   cfun_arity _               = 0;
+
+fun is_contconst (_,_,NoSyn   ) = false
+|   is_contconst (_,_,Binder _) = false
+|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
+			 handle ERROR => error ("in mixfix annotation for " ^
+			 		       quote (Syntax.const_name c mx));
+
+in (* local *)
+
+fun ext_consts prep_typ raw_decls thy =
+let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
+    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
+    val transformed_decls = map transform contconst_decls;
+in thy |> Theory.add_consts_i                    normal_decls
+       |> Theory.add_consts_i        (map first  transformed_decls)
+       |> Theory.add_syntax_i        (map second transformed_decls)
+       |> Theory.add_trrules_i (flat (map third  transformed_decls))
+    handle ERROR =>
+      error ("The error(s) above occurred in (cont)consts section")
+end;
+
+fun cert_typ sg typ =
+  ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
+
+val add_consts   = ext_consts read_ctyp;
+val add_consts_i = ext_consts cert_typ;
+
+end; (* local *)
+
+end; (* struct *)
+
+val _ = ThySyn.add_syntax []
+    [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
+
diff -r 42584a53a3e7 -r 2fd816aa6206 src/HOLCF/contconsts.ML
--- a/src/HOLCF/contconsts.ML	Tue Nov 04 16:57:52 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(*  Title:      HOLCF/contconsts.ML
-    ID:         $Id$
-    Author:     Tobias Mayr and David von Oheimb
-
-theory extender for consts section
-*)
-
-structure ContConsts =
-struct
-
-local
-
-open HOLCFLogic;
-
-exception Impossible of string;
-fun Imposs msg = raise Impossible ("ContConst:"^msg);
-fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
-fun upd_first  f (x,y,z) = (f x,   y,   z);
-fun upd_second f (x,y,z) = (  x, f y,   z);
-fun upd_third  f (x,y,z) = (  x,   y, f z);
-
-fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
-  let fun filt []      = ([],[])
-        | filt (x::xs) = let val (ys,zs) = filt xs in
-			 if pred x then (x::ys,zs) else (ys,x::zs) end
-  in filt end;
-
-fun change_arrow 0 T               = T
-|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
-|   change_arrow _ _               = Imposs "change_arrow";
-
-fun trans_rules name2 name1 n mx = let
-  fun argnames _ 0 = []
-  |   argnames c n = chr c::argnames (c+1) (n-1);
-  val vnames = argnames (ord "A") n;
-  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
-  in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
-			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
-						[t,Variable arg]))
-			  (Constant name1,vnames))]
-     @(case mx of InfixlName _ => [extra_parse_rule] 
-                | InfixrName _ => [extra_parse_rule] | _ => []) end; 
-
-
-(* transforming infix/mixfix declarations of constants with type ...->...
-   a declaration of such a constant is transformed to a normal declaration with 
-   an internal name, the same type, and nofix. Additionally, a purely syntactic
-   declaration with the original name, type ...=>..., and the original mixfix
-   is generated and connected to the other declaration via some translation.
-*)
-fun fix_mixfix (syn                     , T, mx as Infixl           p ) = 
-	       (Syntax.const_name syn mx, T,       InfixlName (syn, p))
-  | fix_mixfix (syn                     , T, mx as Infixr           p ) = 
-	       (Syntax.const_name syn mx, T,       InfixrName (syn, p))
-  | fix_mixfix decl = decl;
-fun transform decl = let 
-	val (c, T, mx) = fix_mixfix decl; 
-	val c2 = "@"^c;
-	val n  = Syntax.mixfix_args mx
-    in	   ((c ,               T,NoSyn),
-	    (c2,change_arrow n T,mx   ),
-	    trans_rules c2 c n mx) end;
-
-fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
-|   cfun_arity _               = 0;
-
-fun is_contconst (_,_,NoSyn   ) = false
-|   is_contconst (_,_,Binder _) = false
-|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
-			 handle ERROR => error ("in mixfix annotation for " ^
-			 		       quote (Syntax.const_name c mx));
-
-in (* local *)
-
-fun ext_consts prep_typ raw_decls thy =
-let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
-    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
-    val transformed_decls = map transform contconst_decls;
-in thy |> Theory.add_consts_i                    normal_decls
-       |> Theory.add_consts_i        (map first  transformed_decls)
-       |> Theory.add_syntax_i        (map second transformed_decls)
-       |> Theory.add_trrules_i (flat (map third  transformed_decls))
-    handle ERROR =>
-      error ("The error(s) above occurred in (cont)consts section")
-end;
-
-fun cert_typ sg typ =
-  ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
-
-val add_consts   = ext_consts read_ctyp;
-val add_consts_i = ext_consts cert_typ;
-
-end; (* local *)
-
-end; (* struct *)
-
-val _ = ThySyn.add_syntax []
-    [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
-
diff -r 42584a53a3e7 -r 2fd816aa6206 src/HOLCF/holcf_logic.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/holcf_logic.ML	Tue Nov 04 17:12:13 1997 +0100
@@ -0,0 +1,66 @@
+(*  Title:      HOLCF/holcf_logic.ML
+    ID:         $Id$
+    Author:     David von Oheimb
+
+Abstract syntax operations for HOLCF.
+*)
+
+infixr 6 ->>;
+
+signature HOLCF_LOGIC =
+sig
+  val mk_btyp: string -> typ * typ -> typ
+  val mk_prodT:          typ * typ -> typ
+  val mk_not:  term -> term
+
+  val HOLCF_sg: Sign.sg
+  val pcpoC: class
+  val pcpoS: sort
+  val mk_TFree: string -> typ
+  val cfun_arrow: string
+  val ->>      : typ * typ -> typ
+  val mk_ssumT : typ * typ -> typ
+  val mk_sprodT: typ * typ -> typ
+  val mk_uT: typ -> typ
+  val trT: typ
+  val oneT: typ
+
+end;
+
+
+structure HOLCFLogic: HOLCF_LOGIC =
+struct
+
+local
+
+  open HOLogic;
+
+in
+
+fun mk_btyp t (S,T) = Type (t,[S,T]);
+val mk_prodT = mk_btyp "*";
+
+fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
+
+(* basics *)
+
+val HOLCF_sg    = sign_of HOLCF.thy;
+val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
+val pcpoS       = [pcpoC];
+fun mk_TFree s  = TFree ("'"^s, pcpoS);
+
+(*cfun, ssum, sprod, u, tr, one *)
+
+local val intern = Sign.intern_tycon HOLCF_sg;
+in
+val cfun_arrow = intern "->";
+val op   ->>  = mk_btyp cfun_arrow;
+val mk_ssumT  = mk_btyp (intern "++");
+val mk_sprodT = mk_btyp (intern "**");
+fun mk_uT T   = Type (intern "u"  ,[T]);
+val trT       = Type (intern "tr" ,[ ]);
+val oneT      = Type (intern "one",[ ]);
+end;
+
+end; (* local *)
+end; (* struct *)