--- 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 *)
--- 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
--- 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";
--- /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];
+
--- 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];
-
--- /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 *)