* removed "axioms" and "generated by" section
authoroheimb
Tue Nov 04 14:40:29 1997 +0100 (1997-11-04)
changeset 4122f63c283cefaf
parent 4121 390e10ddadf2
child 4123 9600dd68d35b
* removed "axioms" and "generated by" section
* replaced "ops" section by extended "consts" section, which is capable of
handling the continuous function space "->" directly
* domain package: now uses normal mixfix annotations (instead of cinfix...)
src/HOLCF/HOLCFLogic.ML
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IsaMakefile
src/HOLCF/ROOT.ML
src/HOLCF/ax_ops/holcflogic.ML
src/HOLCF/ax_ops/thy_axioms.ML
src/HOLCF/ax_ops/thy_ops.ML
src/HOLCF/ax_ops/thy_syntax.ML
src/HOLCF/contconsts.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/ex/Stream.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/HOLCFLogic.ML	Tue Nov 04 14:40:29 1997 +0100
     1.3 @@ -0,0 +1,66 @@
     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/IOA/meta_theory/Seq.thy	Tue Nov 04 14:37:51 1997 +0100
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Nov 04 14:40:29 1997 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  Seq = HOLCF + 
     2.6  
     2.7 -domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (cinfixr 65) 
     2.8 +domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (infixr 65) 
     2.9  
    2.10  
    2.11  consts    
     3.1 --- a/src/HOLCF/IsaMakefile	Tue Nov 04 14:37:51 1997 +0100
     3.2 +++ b/src/HOLCF/IsaMakefile	Tue Nov 04 14:40:29 1997 +0100
     3.3 @@ -22,8 +22,7 @@
     3.4  ONLYTHYS = 
     3.5  
     3.6  FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \
     3.7 -        ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
     3.8 -        ax_ops/thy_ops.ML    ax_ops/thy_syntax.ML \
     3.9 +	HOLCFLogic.ML contconsts.ML \
    3.10          domain/library.ML  domain/syntax.ML   domain/axioms.ML \
    3.11          domain/theorems.ML domain/extender.ML domain/interface.ML
    3.12  
     4.1 --- a/src/HOLCF/ROOT.ML	Tue Nov 04 14:37:51 1997 +0100
     4.2 +++ b/src/HOLCF/ROOT.ML	Tue Nov 04 14:40:29 1997 +0100
     4.3 @@ -14,14 +14,10 @@
     4.4  
     4.5  use_thy "HOLCF";
     4.6  
     4.7 -(* sections axioms, ops *)
     4.8 -use "ax_ops/holcflogic.ML";
     4.9 -use "ax_ops/thy_axioms.ML";
    4.10 -use "ax_ops/thy_ops.ML";
    4.11 -use "ax_ops/thy_syntax.ML";
    4.12 +use "HOLCFLogic";
    4.13 +use "contconsts";
    4.14  
    4.15 -(* sections domain, generated *)
    4.16 -
    4.17 +(* domain package *)
    4.18  use "domain/library.ML";
    4.19  use "domain/syntax.ML";
    4.20  use "domain/axioms.ML";
     5.1 --- a/src/HOLCF/ax_ops/holcflogic.ML	Tue Nov 04 14:37:51 1997 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,69 +0,0 @@
     5.4 -(*
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Mayr
     5.7 -
     5.8 -Additional term and type constructors, extension of Pure/term.ML, logic.ML
     5.9 -and HOL/hologic.ML
    5.10 -
    5.11 -TODO:
    5.12 -
    5.13 -*)
    5.14 -
    5.15 -signature HOLCFLOGIC =
    5.16 -sig
    5.17 - val True  : term;
    5.18 - val False : term;
    5.19 - val Imp   : term;
    5.20 - val And   : term;
    5.21 - val Not   : term;
    5.22 - val mkNot : term -> term;                (* negates, no Trueprop *)
    5.23 - val mkNotEqUU : term -> term;            (* Trueprop(x ~= UU) *)
    5.24 - val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *)
    5.25 - val ==>     : typ * typ -> typ;          (* Infix operation typ constructor *)
    5.26 - val cfun_arrow : string                  (* internalized "->" *)
    5.27 - val mkOpApp : term -> term -> term;      (* Ops application (f ` x) *)
    5.28 - val mkCPair : term -> term -> term;      (* cpair constructor *)
    5.29 -end;
    5.30 -
    5.31 -structure HOLCFlogic : HOLCFLOGIC =
    5.32 -struct
    5.33 -open Logic 
    5.34 -open HOLogic
    5.35 -
    5.36 -val True = Const("True",boolT);
    5.37 -val False = Const("False",boolT);
    5.38 -val Imp = Const("op -->",boolT --> boolT --> boolT);
    5.39 -val And = Const("op &",boolT --> boolT --> boolT);
    5.40 -val Not = Const("Not",boolT --> boolT);   
    5.41 -
    5.42 -fun mkNot A = Not $ A; (* negates, no Trueprop *)
    5.43 -
    5.44 -(* Trueprop(x ~= UU) *)
    5.45 -fun mkNotEqUU v = mk_Trueprop(mkNot(mk_eq(v,Const("UU",fastype_of v))));
    5.46 -
    5.47 -(* mkNotEqUU_in v t = "v~=UU ==> t" *)
    5.48 -fun mkNotEqUU_in vterm term = 
    5.49 -   mk_implies(mkNotEqUU vterm,term)
    5.50 -
    5.51 -val HOLCF_sg = sign_of HOLCF.thy;
    5.52 -fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
    5.53 -fun rep_Type  (Type  x) = x| rep_Type _ = error "Internal error: rep_Type";
    5.54 -
    5.55 -infixr 6 ==>; (* the analogon to --> for operations *)
    5.56 -val op ==> = mk_typ "->";
    5.57 -val cfun_arrow = fst (rep_Type (dummyT ==> dummyT));
    5.58 -
    5.59 -(* Ops application (f ` x) *)
    5.60 -fun mkOpApp (f as Const(_,ft as Type(_(*"->"*),[xt,rt]))) x =
    5.61 -     Const("fapp",ft --> xt --> rt) $ f $ x
    5.62 -  | mkOpApp f x = (error("Internal error: mkOpApp: wrong args"));
    5.63 -
    5.64 -(* cpair constructor *)
    5.65 -fun mkCPair x y = let val tx = fastype_of x
    5.66 -                       val ty = fastype_of y
    5.67 -                   in  
    5.68 -      Const("fapp",(ty==>Type("*",[tx,ty]))-->ty-->Type("*",[tx,ty])) $
    5.69 -      (mkOpApp (Const("cpair",tx ==> ty ==> Type("*",[tx,ty]))) x) $ y
    5.70 -                   end;
    5.71 -
    5.72 -end;
     6.1 --- a/src/HOLCF/ax_ops/thy_axioms.ML	Tue Nov 04 14:37:51 1997 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,209 +0,0 @@
     6.4 -(*
     6.5 -    ID:         $Id$
     6.6 -    Author:     Tobias Mayr
     6.7 -
     6.8 -Additional theory file section for HOLCF: axioms 
     6.9 -*)
    6.10 -
    6.11 -(*** new section of HOLCF : axioms 
    6.12 -     since rules are already internally called axioms,
    6.13 -     the new section is internally called ext_axioms res. eaxms *)
    6.14 -
    6.15 -signature THY_AXIOMS =
    6.16 -sig
    6.17 - (* theory extenders : *)
    6.18 - val add_ext_axioms   : (string * string) list -> (string * string) list
    6.19 -                        -> (string * string) list -> theory -> theory;
    6.20 - val add_ext_axioms_i : (string * (typ option)) list -> 
    6.21 -                        (string * (typ option)) list ->
    6.22 -                        (string * term) list -> theory -> theory;
    6.23 - val axioms_keywords    : string list;
    6.24 - val axioms_sections    : (string * (ThyParse.token list -> 
    6.25 -                        (string * string) * ThyParse.token list)) list;
    6.26 -end;
    6.27 -
    6.28 -structure ThyAxioms : THY_AXIOMS =
    6.29 -struct
    6.30 -
    6.31 -open HOLCFlogic;
    6.32 -
    6.33 -(** library ******************************************************)
    6.34 -
    6.35 -fun apsnd_of_three f = fn (a,b,c) => (a,f b,c);
    6.36 -
    6.37 -fun is_elem e list = exists (fn y => e=y) list
    6.38 -
    6.39 -fun without l1 l2 = (* l1 without the elements of l2 *)
    6.40 -  filter (fn x => (not (is_elem x l2))) l1;
    6.41 -
    6.42 -fun conc [e:string] = e
    6.43 -  | conc (head::tail) = head^", "^(conc tail)
    6.44 -  | conc [] = "";
    6.45 -
    6.46 -fun appear varlist = (* all (x,_) for which (x,_) is in varlist *)
    6.47 -  filter (fn x => (exists (fn y => (fst x)=(fst y)) varlist)) 
    6.48 -
    6.49 -
    6.50 -(* all non unique elements of a list *)
    6.51 -fun doubles (hd::tl) = if   (is_elem hd tl)
    6.52 -                       then (hd::(doubles tl))
    6.53 -                       else (doubles tl)
    6.54 -  | doubles _ = [];
    6.55 -
    6.56 -
    6.57 -(* The main functions are the section parser ext_axiom_decls and the 
    6.58 -   theory extender add_ext_axioms. *)
    6.59 -
    6.60 -(** theory extender : add_ext_axioms *)
    6.61 -
    6.62 -(* forms a function from constrained varnames to their constraints 
    6.63 -   these constraints are then used local to each axiom, as an argument
    6.64 -   of read_def_cterm. Called by add_ext_axioms. *)
    6.65 -fun get_constraints_of_str sign ((vname,vtyp)::tail) = 
    6.66 -   if (vtyp <> "")
    6.67 -   then ((fn (x,_)=> if x=vname 
    6.68 -                      then Some (#T (rep_ctyp (read_ctyp sign vtyp)))
    6.69 -                      else raise Match)
    6.70 -        orelf (get_constraints_of_str sign tail))
    6.71 -   else (get_constraints_of_str sign tail)
    6.72 -  | get_constraints_of_str sign [] = K None;
    6.73 -
    6.74 -(* does the same job for allready parsed optional constraints. 
    6.75 -   Called by add_ext_axioms_i. *)
    6.76 -fun get_constraints_of_typ sign ((vname,vtyp)::tail) = 
    6.77 -   if (is_some vtyp)
    6.78 -   then ((fn (x,_)=> if x=vname 
    6.79 -                      then vtyp
    6.80 -                      else raise Match)
    6.81 -        orelf (get_constraints_of_typ sign tail))
    6.82 -   else (get_constraints_of_typ sign tail)
    6.83 -  | get_constraints_of_typ sign [] = K None;
    6.84 -
    6.85 -
    6.86 -(* applies mkNotEqUU_in on the axiom and every Free that appears in the list
    6.87 -   and in the axiom. Called by check_and_extend. *)
    6.88 -fun add_prem axiom [] = axiom
    6.89 -  | add_prem axiom (vname::tl) =
    6.90 - let val vterm = find_first (fn x => ((#1 o dest_Free) x = vname))
    6.91 -                            (term_frees axiom)
    6.92 - in 
    6.93 -   add_prem  
    6.94 -     (if (is_some vterm) 
    6.95 -      then mkNotEqUU_in (the vterm) axiom
    6.96 -      else axiom)
    6.97 -     tl
    6.98 - end
    6.99 -
   6.100 -(* checks for uniqueness and completeness of var/defvar declarations, 
   6.101 -   and enriches the axiom term with premises. Called by add_ext_axioms(_i).*)
   6.102 -fun check_and_extend sign defvarl varl axiom =
   6.103 -  let
   6.104 -   val names_of_frees =  map (fst o dest_Free) 
   6.105 -                             (term_frees axiom);
   6.106 -   val all_decl_varnames = (defvarl @ varl);
   6.107 -   val undeclared = without names_of_frees all_decl_varnames;
   6.108 -   val doubles = doubles all_decl_varnames
   6.109 -  in
   6.110 -   if (doubles <> [])
   6.111 -   then 
   6.112 -    (error("Multiple declarations of one identifier in section axioms :\n"
   6.113 -           ^(conc doubles)))
   6.114 -   else ();
   6.115 -   if (undeclared <> [])
   6.116 -   then 
   6.117 -    (error("Undeclared identifiers in section axioms : \n"
   6.118 -           ^(conc undeclared)))
   6.119 -   else (); 
   6.120 -   add_prem axiom (rev defvarl)
   6.121 -  end; 
   6.122 -
   6.123 -(* the next five only differ from the original add_axioms' subfunctions
   6.124 -   in the constraints argument for read_def_cterm *) 
   6.125 -local
   6.126 - fun err_in_axm name =
   6.127 -   error ("The error(s) above occurred in axiom " ^ quote name); 
   6.128 -
   6.129 - fun no_vars tm =
   6.130 -   if null (term_vars tm) andalso null (term_tvars tm) then tm
   6.131 -   else error "Illegal schematic variable(s) in term"; 
   6.132 -
   6.133 - fun read_ext_cterm sign constraints = 
   6.134 -   #1 o read_def_cterm (sign, constraints, K None) [] true;
   6.135 -
   6.136 - (* only for add_ext_axioms (working on strings) *)
   6.137 - fun read_ext_axm sg constraints (name,str) =
   6.138 -   (name, no_vars (term_of (read_ext_cterm sg constraints (str, propT))))
   6.139 -    handle ERROR => err_in_axm name;
   6.140 -
   6.141 - (* only for add_ext_axioms_i (working on terms) *)
   6.142 - fun read_ext_axm_terms sg constraints (name,term) =
   6.143 -   (name, no_vars (#2(Sign.infer_types sg constraints  (K None) [] true 
   6.144 -                                       ([term], propT))))
   6.145 -    handle ERROR => err_in_axm name;
   6.146 -
   6.147 -in
   6.148 -
   6.149 -(******* THE THEORY EXTENDERS THEMSELVES *****)
   6.150 - fun add_ext_axioms varlist defvarlist axioms theory =
   6.151 -  let val {sign, ...} = rep_theory theory;
   6.152 -      val constraints = get_constraints_of_str sign (defvarlist@varlist)
   6.153 -  in
   6.154 -    PureThy.add_store_axioms_i (map (apsnd 
   6.155 -     (check_and_extend sign (map fst defvarlist) (map fst varlist)) o
   6.156 -               (read_ext_axm sign constraints)) axioms) theory
   6.157 -  end 
   6.158 -
   6.159 - fun add_ext_axioms_i varlist defvarlist axiom_terms theory =
   6.160 -  let val {sign, ...} = rep_theory theory;
   6.161 -      val constraints = get_constraints_of_typ sign (defvarlist@varlist)
   6.162 -  in
   6.163 -    PureThy.add_store_axioms_i (map (apsnd (check_and_extend sign 
   6.164 -                               (map fst defvarlist) (map fst varlist)) o
   6.165 -                   (read_ext_axm_terms sign constraints)) axiom_terms) theory
   6.166 -  end
   6.167 -end;
   6.168 -
   6.169 -
   6.170 -(******** SECTION PARSER : ext_axiom_decls **********)
   6.171 -local 
   6.172 - open ThyParse 
   6.173 -
   6.174 - (* as in the pure section 'rules' : 
   6.175 -    making the "val thmname = get_axiom thy thmname" list *)
   6.176 - val mk_list_of_pairs = mk_big_list o map (mk_pair o apfst quote);
   6.177 - fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";";
   6.178 - val mk_vals = cat_lines o map mk_val;
   6.179 -
   6.180 - (* making the call for the theory extender *) 
   6.181 - fun mk_eaxms_decls ((vars,defvars),axms) = 
   6.182 -     ( "|> ThyAxioms.add_ext_axioms \n  " ^ 
   6.183 -       (mk_list_of_pairs vars) ^ "\n  " ^
   6.184 -       (mk_list_of_pairs defvars) ^ "\n  " ^
   6.185 -       (mk_list_of_pairs axms),
   6.186 -       mk_vals (map fst axms));
   6.187 -
   6.188 - (* parsing the concrete syntax *)    
   6.189 -
   6.190 - val axiom_decls = (repeat1 (ident -- !! string));
   6.191 -
   6.192 - val varlist = "vars" $$-- 
   6.193 -                 repeat1 (ident -- optional ("::" $$-- string) "\"\"");
   6.194 -
   6.195 - val defvarlist = "defvars" $$-- 
   6.196 -                    repeat1 (ident -- optional ("::" $$-- string) "\"\""); 
   6.197 -
   6.198 -in
   6.199 -
   6.200 - val ext_axiom_decls = (optional varlist []) -- (optional defvarlist [])
   6.201 -                         -- ("in" $$-- axiom_decls) >> mk_eaxms_decls;
   6.202 -end; (* local *)
   6.203 -
   6.204 -
   6.205 -(**** new keywords and sections ************************************)
   6.206 -
   6.207 -val axioms_keywords = ["vars", "defvars","in"];
   6.208 -     (* "::" is already a pure keyword *)
   6.209 -
   6.210 -val axioms_sections = [("axioms" , ext_axiom_decls)]
   6.211 -                       
   6.212 -end; (* the structure *)
     7.1 --- a/src/HOLCF/ax_ops/thy_ops.ML	Tue Nov 04 14:37:51 1997 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,449 +0,0 @@
     7.4 -(*  TTITLEF/thy_ops.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Tobias Mayr
     7.7 -
     7.8 -Additional theory file section for HOLCF: ops 
     7.9 -
    7.10 -TODO:
    7.11 -  maybe AST-representation with "op name" instead of _I_...
    7.12 -*)
    7.13 -
    7.14 -signature THY_OPS =
    7.15 -sig
    7.16 - (* continuous mixfixes (extension of datatype Mixfix.mixfix) *)
    7.17 - datatype cmixfix =
    7.18 -    Mixfix of Mixfix.mixfix |
    7.19 -    CInfixl of int | 
    7.20 -    CInfixr of int |
    7.21 -    CMixfix of string * int list *int;
    7.22 -
    7.23 - exception CINFIX of cmixfix;
    7.24 - val cmixfix_to_mixfix : cmixfix ->  Mixfix.mixfix;
    7.25 -
    7.26 - (* theory extenders : *)
    7.27 - val add_ops          : {curried: bool, total: bool, strict: bool} ->
    7.28 -                        (string * string * cmixfix) list -> theory -> theory;
    7.29 - val add_ops_i        : {curried: bool, total: bool, strict: bool} ->
    7.30 -                        (string * typ * cmixfix) list -> theory -> theory;
    7.31 - val ops_keywords  : string list;
    7.32 - val ops_sections  : (string * (ThyParse.token list -> 
    7.33 -                        (string * string) * ThyParse.token list)) list;
    7.34 - val opt_cmixfix: ThyParse.token list -> (string * ThyParse.token list);
    7.35 - val const_name    : string -> cmixfix -> string;
    7.36 -end;
    7.37 -
    7.38 -structure ThyOps : THY_OPS =
    7.39 -struct
    7.40 -
    7.41 -open HOLCFlogic;
    7.42 -
    7.43 -(** library ******************************************************)
    7.44 -
    7.45 -(* abbreviations *)
    7.46 -val internal = fst; (* cinfix-ops will have diffrent internal/external names *)
    7.47 -val external = snd;
    7.48 -
    7.49 -fun apsnd_of_three f = fn (a,b,c) => (a,f b,c);
    7.50 -
    7.51 -
    7.52 -(******** ops ********************)
    7.53 -
    7.54 -(* the extended copy of mixfix *)
    7.55 -datatype cmixfix =
    7.56 -    Mixfix of Mixfix.mixfix |
    7.57 -    CInfixl of int |
    7.58 -    CInfixr of int |
    7.59 -    CMixfix of string * int list *int;
    7.60 -
    7.61 -exception CINFIX of cmixfix;
    7.62 -
    7.63 -fun cmixfix_to_mixfix (Mixfix x) = x
    7.64 -  | cmixfix_to_mixfix x = raise CINFIX x;
    7.65 -
    7.66 -
    7.67 -(** theory extender : add_ops *)
    7.68 -
    7.69 -(* generating the declarations of the new constants. *************
    7.70 -   cinfix names x are internally non infix (renamed by mk_internal_name) 
    7.71 -   and externally non continous infix function names (changed by op_to_fun).
    7.72 -   Thus the cinfix declaration is splitted in an 'oldstyle' decl,
    7.73 -   which is NoSyn (non infix) and is added by add_consts_i,
    7.74 -   and an syn(tactic) decl, which is an infix function (not operation)
    7.75 -   added by add_syntax_i, so that it can appear in input strings, but 
    7.76 -   not in terms.
    7.77 -   The interface between internal and external names is realized by 
    7.78 -   transrules A x B <=> _x ' A ' B (generated by xrules_of) 
    7.79 -   The boolean argument 'curried' distinguishes between curried and
    7.80 -   tupeled syntax of operation application *)
    7.81 -   
    7.82 -local
    7.83 - fun strip ("'" :: c :: cs) = c :: strip cs
    7.84 -   | strip ["'"] = []
    7.85 -   | strip (c :: cs) = c :: strip cs
    7.86 -   | strip [] = [];
    7.87 -
    7.88 - val strip_esc = implode o strip o explode;
    7.89 -
    7.90 - fun infix_name c = "op " ^ strip_esc c;
    7.91 -in
    7.92 -  val mk_internal_name = infix_name;
    7.93 -(*
    7.94 -(* changing e.g. 'ab' to '_I_97_98'. 
    7.95 -   Called by oldstyle, xrules_of, strictness_axms and totality_axms. *)
    7.96 -  fun mk_internal_name name =
    7.97 -  let fun alphanum (s::ss) = "_"^(string_of_int (ord s))^(alphanum ss)
    7.98 -        | alphanum [] = "";
    7.99 -  in 
   7.100 -      "_I"^(alphanum o explode) name
   7.101 -  end;
   7.102 -*)
   7.103 - (* extension of Pure/Syntax/mixfix.ML: SynExt.const_name *)
   7.104 - fun const_name c (CInfixl _) = mk_internal_name c
   7.105 -   | const_name c (CInfixr _) = mk_internal_name c
   7.106 -   | const_name c (CMixfix _) = c
   7.107 -   | const_name c (Mixfix  x) = Syntax.const_name c x;
   7.108 -end;
   7.109 -
   7.110 -(* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *) 
   7.111 -(*####*)
   7.112 -fun op_to_fun true  sign (ty as Type(name ,[larg,t]))= if name = cfun_arrow
   7.113 -                  then Type("fun",[larg,op_to_fun true sign t]) else ty
   7.114 -  | op_to_fun false sign (ty as Type(name,[args,res])) = let
   7.115 -                fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
   7.116 -                |   otf t                        = Type("fun",[t,res]);
   7.117 -                in if name = cfun_arrow then otf args else ty end
   7.118 -  | op_to_fun _     sign t = t;
   7.119 -(*####*)
   7.120 -
   7.121 -(* oldstyle is called by add_ext_axioms(_i) *)
   7.122 -    (* the first part is just copying the homomorphic part of the structures *)
   7.123 -fun oldstyle ((name,typ,Mixfix(x))::tl) = 
   7.124 -         (name,typ,x)::(oldstyle tl)
   7.125 -  | oldstyle ((name,typ,CInfixl(i))::tl) = 
   7.126 -         (mk_internal_name name,typ,Mixfix.NoSyn)::
   7.127 -         (oldstyle tl)
   7.128 -  | oldstyle ((name,typ,CInfixr(i))::tl) =
   7.129 -         (mk_internal_name name,typ,Mixfix.NoSyn)::
   7.130 -         (oldstyle tl) 
   7.131 -  | oldstyle ((name,typ,CMixfix(x))::tl) =
   7.132 -         (name,typ,Mixfix.NoSyn)::
   7.133 -         (oldstyle tl) 
   7.134 -  | oldstyle [] = [];
   7.135 -
   7.136 -(* generating the external purely syntactical infix functions. 
   7.137 -   Called by add_ext_axioms(_i) *)
   7.138 -fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) =
   7.139 -     (name,op_to_fun curried sign typ,Mixfix.Infixl(i))::
   7.140 -      (syn_decls curried sign tl)
   7.141 -  | syn_decls curried sign ((name,typ,CInfixr(i))::tl) =
   7.142 -     (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
   7.143 -      (syn_decls curried sign tl)
   7.144 -  | syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
   7.145 -     (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
   7.146 -
   7.147 -      (syn_decls curried sign tl)
   7.148 -  | syn_decls curried sign (_::tl) = syn_decls curried sign tl
   7.149 -  | syn_decls _ _ [] = [];
   7.150 -
   7.151 -fun translate name vars rhs = 
   7.152 -    Syntax.ParsePrintRule ((Ast.mk_appl (Constant (mk_internal_name name)) 
   7.153 -		 (map Variable vars)), 
   7.154 -		rhs); 
   7.155 -
   7.156 -(* generating the translation rules. Called by add_ext_axioms(_i) *)
   7.157 -local open Ast in 
   7.158 -fun xrules_of true ((name,typ,CInfixl(i))::tail) = 
   7.159 -    translate name ["A","B"]
   7.160 -     (mk_appl (Constant "@fapp") 
   7.161 -      [(mk_appl (Constant "@fapp") 
   7.162 -	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
   7.163 -    ::xrules_of true tail
   7.164 -  | xrules_of true ((name,typ,CInfixr(i))::tail) = 
   7.165 -    translate name ["A","B"]
   7.166 -     (mk_appl (Constant "@fapp") 
   7.167 -      [(mk_appl (Constant "@fapp") 
   7.168 -	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
   7.169 -    ::xrules_of true tail
   7.170 -(*####*)
   7.171 -  | xrules_of true ((name,typ,CMixfix(_))::tail) = 
   7.172 -        let fun argnames n (Type(name ,[_,t]))= if name = cfun_arrow then
   7.173 -					chr n :: argnames (n+1) t else []
   7.174 -            |   argnames _ _ = [];
   7.175 -            val names = argnames (ord"A") typ;
   7.176 -        in if names = [] then [] else 
   7.177 -	    [Syntax.ParsePrintRule (mk_appl (Constant name) (map Variable names),
   7.178 -			 foldl (fn (t,arg) => 
   7.179 -				(mk_appl (Constant "@fapp") [t,Variable arg]))
   7.180 -			 (Constant name,names))] 
   7.181 -        end
   7.182 -    @xrules_of true tail
   7.183 -(*####*)
   7.184 -  | xrules_of false ((name,typ,CInfixl(i))::tail) = 
   7.185 -    translate name ["A","B"]
   7.186 -    (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
   7.187 -     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
   7.188 -    ::xrules_of false tail
   7.189 -  | xrules_of false ((name,typ,CInfixr(i))::tail) = 
   7.190 -    translate name ["A","B"]
   7.191 -    (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
   7.192 -     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
   7.193 -    ::xrules_of false tail
   7.194 -(*####*)
   7.195 -  | xrules_of false ((name,typ,CMixfix(_))::tail) = 
   7.196 -        let fun foldr' f l =
   7.197 -	      let fun itr []  = raise LIST "foldr'"
   7.198 -		    | itr [a] = a
   7.199 -		    | itr (a::l) = f(a, itr l)
   7.200 -	      in  itr l end;
   7.201 -	    fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
   7.202 -	    |   argnames n _ = [chr n];
   7.203 -	    val vars = map Variable (case typ of (Type(name ,[t,_])) =>
   7.204 -			if name = cfun_arrow then argnames (ord"A") t else []
   7.205 -						 | _ => []);
   7.206 -        in if vars = [] then [] else 
   7.207 -	    [Syntax.ParsePrintRule 
   7.208 -	     (mk_appl (Constant name) vars,
   7.209 -	      mk_appl (Constant "@fapp")
   7.210 -	      [Constant name, 
   7.211 -	       case vars of [v] => v
   7.212 -	                 | args => mk_appl (Constant "@ctuple")
   7.213 -			             [hd args,
   7.214 -				      foldr' (fn (t,arg) => 
   7.215 -					      mk_appl (Constant "_args")
   7.216 -					      [t,arg]) (tl args)]])]
   7.217 -        end
   7.218 -    @xrules_of false tail
   7.219 -(*####*)
   7.220 -  | xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail
   7.221 -  | xrules_of _ [] = [];
   7.222 -end; 
   7.223 -(**** producing the new axioms ****************)
   7.224 -
   7.225 -datatype arguments = Curried_args of ((typ*typ) list) |
   7.226 -                     Tupeled_args of (typ list);
   7.227 -
   7.228 -fun num_of_args (Curried_args l) = length l
   7.229 -  | num_of_args (Tupeled_args l) = length l;
   7.230 -
   7.231 -fun types_of (Curried_args l) = map fst l
   7.232 -  | types_of (Tupeled_args l) = l;
   7.233 -
   7.234 -fun mk_mkNotEqUU_vars (typ::tl) cnt = mkNotEqUU (Free("x"^(string_of_int cnt),typ))::
   7.235 -                            (mk_mkNotEqUU_vars tl (cnt+1))
   7.236 -  | mk_mkNotEqUU_vars [] _ = [];
   7.237 -
   7.238 -local
   7.239 - (* T1*...*Tn goes to [T1,...,Tn] *)
   7.240 - fun args_of_tupel (Type("*",[left,right])) = left::(args_of_tupel right)
   7.241 -   | args_of_tupel T = [T];
   7.242 - 
   7.243 - (* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R 
   7.244 -    Bi is the Type of the function that is applied to an Ai type argument *)
   7.245 - fun args_of_curried (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
   7.246 -      (S,typ) :: args_of_curried T else []
   7.247 -   | args_of_curried _ = [];
   7.248 -in
   7.249 - fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
   7.250 -   | args_of_op false (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
   7.251 -      Tupeled_args(args_of_tupel S) else Tupeled_args([])
   7.252 -   | args_of_op false _ = Tupeled_args([]);
   7.253 -end;
   7.254 -
   7.255 -(* generates for the type t the type of the fapp constant 
   7.256 -   that will be applied to t *)
   7.257 -fun mk_fapp_typ (typ as Type(_(*"->"*),argl)) = Type("fun",[typ,Type("fun",argl)]) 
   7.258 -  | mk_fapp_typ t = (
   7.259 -                    error("Internal error:mk_fapp_typ: wrong argument\n"));
   7.260 -                    
   7.261 -fun mk_arg_tupel_UU uu_pos [typ] n = 
   7.262 -     if n<>uu_pos then Free("x"^(string_of_int n),typ)
   7.263 -                  else Const("UU",typ)
   7.264 -  | mk_arg_tupel_UU uu_pos (typ::tail) n = 
   7.265 -     mkCPair
   7.266 -     (if n<>uu_pos then Free("x"^(string_of_int n),typ) 
   7.267 -                   else Const("UU",typ))
   7.268 -     (mk_arg_tupel_UU uu_pos tail (n+1))
   7.269 -  | mk_arg_tupel_UU _ [] _ = error("Internal error:mk_arg_tupel: empty list");
   7.270 -
   7.271 -fun mk_app_UU cnt uu_pos fname (Curried_args((typ,ftyp)::tl)) = 
   7.272 -     Const("fapp",mk_fapp_typ ftyp) $
   7.273 -     (mk_app_UU (cnt-1) uu_pos fname (Curried_args tl))$ 
   7.274 -     (if cnt = uu_pos then Const("UU",typ)
   7.275 -                      else Free("x"^(string_of_int cnt),typ))
   7.276 -  | mk_app_UU _ _ (name,typ) (Curried_args []) = Const(name,typ)
   7.277 -  | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args []) = Const(name,typ)
   7.278 -  | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args list) = 
   7.279 -     Const("fapp",mk_fapp_typ typ) $ Const(name,typ) $ 
   7.280 -     mk_arg_tupel_UU uu_pos list 0;
   7.281 -
   7.282 -fun mk_app cnt fname args = mk_app_UU cnt (~1) fname args;
   7.283 -
   7.284 -(* producing the strictness axioms *)
   7.285 -local
   7.286 - fun s_axm_of curried name typ args num cnt = 
   7.287 -       if cnt = num then 
   7.288 -        error("Internal error: s_axm_of: arg is no operation "^(external name))
   7.289 -       else 
   7.290 -       let val app = mk_app_UU (num-1) cnt (internal name,typ) args
   7.291 -           val equation = HOLogic.mk_eq(app,Const("UU",fastype_of app)) 
   7.292 -       in 
   7.293 -        if cnt = num-1 then equation
   7.294 -        else And $ equation $
   7.295 -             s_axm_of curried name typ args num (cnt+1)
   7.296 -       end;
   7.297 -in
   7.298 - fun strictness_axms curried ((rawname,typ,cmixfix)::tail) =
   7.299 -  let val name = case cmixfix of
   7.300 -                      (CInfixl _) => (mk_internal_name rawname,rawname)
   7.301 -                    | (CInfixr _) => (mk_internal_name rawname,rawname)
   7.302 -                    |  _          => (rawname,rawname)
   7.303 -      val args = args_of_op curried typ;
   7.304 -      val num  = num_of_args args;
   7.305 -  in
   7.306 -      ((external name)^"_strict",
   7.307 -       if num <> 0
   7.308 -       then HOLogic.mk_Trueprop(s_axm_of curried name typ args num 0) 
   7.309 -       else HOLogic.mk_Trueprop(True)) :: strictness_axms curried tail
   7.310 -  end
   7.311 -   | strictness_axms _ [] = [];
   7.312 -end; (*local*)
   7.313 -
   7.314 -(* producing the totality axioms *)
   7.315 -
   7.316 -fun totality_axms curried ((rawname,typ,cmixfix)::tail) =
   7.317 - let val name  = case cmixfix of
   7.318 -                     (CInfixl _) => (mk_internal_name rawname,rawname)
   7.319 -                   | (CInfixr _) => (mk_internal_name rawname,rawname)
   7.320 -                   | _           => (rawname,rawname)
   7.321 -     val args  = args_of_op curried typ;
   7.322 -     val prems = mk_mkNotEqUU_vars (if curried then rev (types_of args)
   7.323 -                                           else (types_of args)) 0;
   7.324 -     val term  = mk_app (num_of_args args - 1) (internal name,typ) args;
   7.325 - in
   7.326 -     ((external name)^"_total", 
   7.327 -      if num_of_args args <> 0 
   7.328 -      then Logic.list_implies (prems,mkNotEqUU term)
   7.329 -      else HOLogic.mk_Trueprop(True)) :: totality_axms curried tail
   7.330 - end
   7.331 -  | totality_axms _ [] = [];
   7.332 -
   7.333 -
   7.334 -
   7.335 -(* the theory extenders ****************************)
   7.336 -
   7.337 -fun add_ops {curried,strict,total} raw_decls thy =
   7.338 -  let val {sign,...} = rep_theory thy;
   7.339 -      val decls = map (apsnd_of_three (typ_of o read_ctyp sign)) raw_decls;
   7.340 -      val oldstyledecls = oldstyle decls;
   7.341 -      val syndecls = syn_decls curried sign decls;
   7.342 -      val xrules = xrules_of curried decls;
   7.343 -      val s_axms = (if strict then strictness_axms curried decls else []);
   7.344 -      val t_axms = (if total  then totality_axms   curried decls else []);
   7.345 -  in 
   7.346 -  Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms) 
   7.347 -                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   7.348 -  end;
   7.349 -
   7.350 -fun add_ops_i {curried,strict,total} decls thy =
   7.351 -  let val {sign,...} = rep_theory thy;
   7.352 -      val oldstyledecls = oldstyle decls;
   7.353 -      val syndecls = syn_decls curried sign decls;
   7.354 -      val xrules = xrules_of curried decls;
   7.355 -      val s_axms = (if strict then strictness_axms curried decls else []);
   7.356 -      val t_axms = (if total  then totality_axms   curried decls else []);
   7.357 -  in 
   7.358 -  Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms) 
   7.359 -                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   7.360 -  end;
   7.361 -
   7.362 -
   7.363 -(* parser: ops_decls ********************************)
   7.364 -
   7.365 -local open ThyParse 
   7.366 -in
   7.367 -(* the following is an adapted version of const_decls from thy_parse.ML *)
   7.368 -
   7.369 -val names1 = list1 name;
   7.370 -
   7.371 -fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls);
   7.372 -
   7.373 -fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
   7.374 -
   7.375 -fun mk_strict_vals [] = ""
   7.376 -  | mk_strict_vals [name] =
   7.377 -      "get_axiom thy \""^name^"_strict\"\n"
   7.378 -  | mk_strict_vals (name::tail) =
   7.379 -      "get_axiom thy \""^name^"_strict\",\n"^
   7.380 -      mk_strict_vals tail;
   7.381 -  
   7.382 -fun mk_total_vals [] = ""
   7.383 -  | mk_total_vals [name] = 
   7.384 -      "get_axiom thy \""^name^"_total\"\n"
   7.385 -  | mk_total_vals (name::tail) =
   7.386 -      "get_axiom thy \""^name^"_total\",\n"^
   7.387 -      mk_total_vals tail;
   7.388 -
   7.389 -fun mk_ops_decls (((curried,strict),total),list) =
   7.390 -          (* call for the theory extender *)
   7.391 -           ("|> ThyOps.add_ops \n"^
   7.392 -            "{ curried = "^curried^" , strict = "^strict^
   7.393 -               " , total = "^total^" } \n"^
   7.394 -            (mk_big_list o map mk_triple2) list^";\n"^
   7.395 -            "val strict_axms = []; val total_axms = [];\nval thy = thy\n",
   7.396 -          (* additional declarations *)
   7.397 -            (if strict="true" then "val strict_axms = strict_axms @ [\n"^
   7.398 -               mk_strict_vals (map (strip_quotes o fst) list)^
   7.399 -               "];\n"             
   7.400 -             else "")^
   7.401 -            (if total="true" then "val total_axms = total_axms @ [\n"^
   7.402 -               mk_total_vals (map (strip_quotes o fst) list)^
   7.403 -               "];\n"             
   7.404 -             else ""));
   7.405 -
   7.406 -(* mixfix annotations *)
   7.407 -
   7.408 -fun cat_parens pre1 pre2 s = cat pre1 (parens (cat pre2 s));
   7.409 -
   7.410 -val infxl = "infixl" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixl";
   7.411 -val infxr = "infixr" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixr";
   7.412 -
   7.413 -val cinfxl = "cinfixl" $$-- !! nat >> cat "ThyOps.CInfixl";
   7.414 -val cinfxr = "cinfixr" $$-- !! nat >> cat "ThyOps.CInfixr";
   7.415 -
   7.416 -val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
   7.417 -
   7.418 -val cmixfx = "cmixfix" $$-- string -- !! (opt_pris -- optional nat "max_pri")
   7.419 -  >> (cat "ThyOps.CMixfix" o mk_triple2);
   7.420 -
   7.421 -val bindr = "binder" $$--
   7.422 -  !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
   7.423 -                || nat >> (fn n => (n,n))
   7.424 -     )          )
   7.425 -  >> (cat_parens "ThyOps.Mixfix" "Binder" o mk_triple2);
   7.426 -
   7.427 -val mixfx = string -- !! (opt_pris -- optional nat "max_pri")
   7.428 -  >> (cat_parens "ThyOps.Mixfix" "Mixfix" o mk_triple2);
   7.429 -
   7.430 -fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "ThyOps.Mixfix NoSyn";
   7.431 -
   7.432 -val opt_cmixfix = opt_syn (mixfx || infxl || infxr || bindr || 
   7.433 -                              cinfxl || cinfxr || cmixfx);
   7.434 -
   7.435 -fun ops_decls toks= 
   7.436 -               (optional ($$ "curried" >> K "true") "false" --
   7.437 -                optional ($$ "strict" >> K "true") "false" --
   7.438 -                optional ($$ "total" >> K "true") "false" -- 
   7.439 -                (repeat1 (names1 --$$ "::" -- !! (string -- opt_cmixfix)) 
   7.440 -                 >> split_decls)
   7.441 -                >> mk_ops_decls) toks
   7.442 -
   7.443 -end;
   7.444 -
   7.445 -(*** new keywords and sections: ******************************************)
   7.446 -
   7.447 -val ops_keywords = ["curried","strict","total","cinfixl","cinfixr","cmixfix"];
   7.448 -     (* "::" is already a pure keyword *)
   7.449 -
   7.450 -val ops_sections = [("ops"    , ops_decls) ];
   7.451 -
   7.452 -end; (* the structure ThyOps *)
     8.1 --- a/src/HOLCF/ax_ops/thy_syntax.ML	Tue Nov 04 14:37:51 1997 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,10 +0,0 @@
     8.4 -(*  Title:      HOLCF/thy_syntax.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Tobias Mayr
     8.7 -
     8.8 -Additional thy file sections for HOLCF: axioms, ops.
     8.9 -*)
    8.10 -
    8.11 -ThySyn.add_syntax
    8.12 - (ThyAxioms.axioms_keywords @ ThyOps.ops_keywords)
    8.13 - (ThyAxioms.axioms_sections @ ThyOps.ops_sections);
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOLCF/contconsts.ML	Tue Nov 04 14:40:29 1997 +0100
     9.3 @@ -0,0 +1,99 @@
     9.4 +(*  Title:      HOLCF/contconsts.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Tobias Mayr and David von Oheimb
     9.7 +
     9.8 +theory extender for consts section
     9.9 +*)
    9.10 +
    9.11 +structure ContConsts =
    9.12 +struct
    9.13 +
    9.14 +local
    9.15 +
    9.16 +open HOLCFLogic;
    9.17 +
    9.18 +exception Impossible of string;
    9.19 +fun Imposs msg = raise Impossible ("ContConst:"^msg);
    9.20 +fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    9.21 +fun upd_first  f (x,y,z) = (f x,   y,   z);
    9.22 +fun upd_second f (x,y,z) = (  x, f y,   z);
    9.23 +fun upd_third  f (x,y,z) = (  x,   y, f z);
    9.24 +
    9.25 +fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
    9.26 +  let fun filt []      = ([],[])
    9.27 +        | filt (x::xs) = let val (ys,zs) = filt xs in
    9.28 +			 if pred x then (x::ys,zs) else (ys,x::zs) end
    9.29 +  in filt end;
    9.30 +
    9.31 +fun change_arrow 0 T               = T
    9.32 +|   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
    9.33 +|   change_arrow _ _               = Imposs "change_arrow";
    9.34 +
    9.35 +fun trans_rules name2 name1 n mx = let
    9.36 +  fun argnames _ 0 = []
    9.37 +  |   argnames c n = chr c::argnames (c+1) (n-1);
    9.38 +  val vnames = argnames (ord "A") n;
    9.39 +  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
    9.40 +  in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
    9.41 +			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
    9.42 +						[t,Variable arg]))
    9.43 +			  (Constant name1,vnames))]
    9.44 +     @(case mx of InfixlName _ => [extra_parse_rule] 
    9.45 +                | InfixrName _ => [extra_parse_rule] | _ => []) end; 
    9.46 +
    9.47 +
    9.48 +(* transforming infix/mixfix declarations of constants with type ...->...
    9.49 +   a declaration of such a constant is transformed to a normal declaration with 
    9.50 +   an internal name, the same type, and nofix. Additionally, a purely syntactic
    9.51 +   declaration with the original name, type ...=>..., and the original mixfix
    9.52 +   is generated and connected to the other declaration via some translation.
    9.53 +*)
    9.54 +fun fix_mixfix (syn                     , T, mx as Infixl           p ) = 
    9.55 +	       (Syntax.const_name syn mx, T,       InfixlName (syn, p))
    9.56 +  | fix_mixfix (syn                     , T, mx as Infixr           p ) = 
    9.57 +	       (Syntax.const_name syn mx, T,       InfixrName (syn, p))
    9.58 +  | fix_mixfix decl = decl;
    9.59 +fun transform decl = let 
    9.60 +	val (c, T, mx) = fix_mixfix decl; 
    9.61 +	val c2 = "@"^c;
    9.62 +	val n  = Syntax.mixfix_args mx
    9.63 +    in	   ((c ,               T,NoSyn),
    9.64 +	    (c2,change_arrow n T,mx   ),
    9.65 +	    trans_rules c2 c n mx) end;
    9.66 +
    9.67 +fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
    9.68 +|   cfun_arity _               = 0;
    9.69 +
    9.70 +fun is_contconst (_,_,NoSyn   ) = false
    9.71 +|   is_contconst (_,_,Binder _) = false
    9.72 +|   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    9.73 +			 handle ERROR => error ("in mixfix annotation for " ^
    9.74 +			 		       quote (Syntax.const_name c mx));
    9.75 +
    9.76 +in (* local *)
    9.77 +
    9.78 +fun ext_consts prep_typ raw_decls thy =
    9.79 +let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
    9.80 +    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
    9.81 +    val transformed_decls = map transform contconst_decls;
    9.82 +in thy |> Theory.add_consts_i                    normal_decls
    9.83 +       |> Theory.add_consts_i        (map first  transformed_decls)
    9.84 +       |> Theory.add_syntax_i        (map second transformed_decls)
    9.85 +       |> Theory.add_trrules_i (flat (map third  transformed_decls))
    9.86 +    handle ERROR =>
    9.87 +      error ("The error(s) above occurred in (cont)consts section")
    9.88 +end;
    9.89 +
    9.90 +fun cert_typ sg typ =
    9.91 +  ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
    9.92 +
    9.93 +val add_consts   = ext_consts read_ctyp;
    9.94 +val add_consts_i = ext_consts cert_typ;
    9.95 +
    9.96 +end; (* local *)
    9.97 +
    9.98 +end; (* struct *)
    9.99 +
   9.100 +val _ = ThySyn.add_syntax []
   9.101 +    [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
   9.102 +
    10.1 --- a/src/HOLCF/domain/axioms.ML	Tue Nov 04 14:37:51 1997 +0100
    10.2 +++ b/src/HOLCF/domain/axioms.ML	Tue Nov 04 14:40:29 1997 +0100
    10.3 @@ -137,25 +137,5 @@
    10.4         |> Theory.add_path ".."
    10.5  end;
    10.6  
    10.7 -
    10.8 -fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
    10.9 -  fun P_name typ = "P"^(if typs = [typ] then "" 
   10.10 -			else string_of_int(1 + find(typ,typs)));
   10.11 -  fun lift_adm t = lift (fn typ => %%"adm" $ %(P_name typ)) 
   10.12 -			(if finite then [] else typs,t);
   10.13 -  fun lift_pred_UU t = lift (fn typ => %(P_name typ) $ UU) (typs,t);
   10.14 -  fun one_cnstr (cnstr,vns,(args,res)) = let 
   10.15 -		val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args);
   10.16 -		val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns);
   10.17 -	     in foldr mk_All (vns,
   10.18 -			 lift (fn (vn,typ) => %(P_name typ) $ bound_arg vns vn)
   10.19 -			      (rec_args,defined app ==> %(P_name res)$app)) end;
   10.20 -  fun one_conc typ = let val pn = P_name typ 
   10.21 -		     in %pn $ %("x"^implode(tl(explode pn))) end;
   10.22 -  val concl = mk_trp(foldr' mk_conj (map one_conc typs));
   10.23 -  val induct = (tname^"_induct",lift_adm(lift_pred_UU(
   10.24 -			foldr (op ===>) (map one_cnstr cnstrs,concl))));
   10.25 -in thy' |> Theory.add_axioms_i (infer_types thy' [induct]) end;
   10.26 -
   10.27  end; (* local *)
   10.28  end; (* struct *)
    11.1 --- a/src/HOLCF/domain/extender.ML	Tue Nov 04 14:37:51 1997 +0100
    11.2 +++ b/src/HOLCF/domain/extender.ML	Tue Nov 04 14:40:29 1997 +0100
    11.3 @@ -17,7 +17,7 @@
    11.4  (* ----- general testing and preprocessing of constructor list -------------- *)
    11.5  
    11.6    fun check_and_sort_domain (dtnvs: (string * typ list) list, cons'' :
    11.7 -     ((string * ThyOps.cmixfix * (bool*string*typ) list) list) list) sg =
    11.8 +     ((string * mixfix * (bool*string*typ) list) list) list) sg =
    11.9    let
   11.10      val defaultS = Type.defaultS (tsig_of sg);
   11.11      val test_dupl_typs = (case duplicates (map fst dtnvs) of 
   11.12 @@ -65,52 +65,6 @@
   11.13    in ListPair.map analyse_equation (dtnvs,cons'')
   11.14    end; (* let *)
   11.15  
   11.16 -  fun check_gen_by sg' (typs': string list,cnstrss': string list list) = let
   11.17 -    val test_dupl_typs = (case duplicates typs' of [] => false
   11.18 -	  | dups => error ("Duplicate types: " ^ commas_quote dups));
   11.19 -    val test_dupl_cnstrs = map (fn cs => (case duplicates cs of [] => false 
   11.20 -	| ds => error ("Duplicate constructors: " ^ commas_quote ds))) cnstrss';
   11.21 -    val tycons = map fst (#tycons(Type.rep_tsig (tsig_of sg')));
   11.22 -    val test_types = forall (fn t => t mem tycons orelse 
   11.23 -				     error("Unknown type: "^t)) typs';
   11.24 -    val cnstrss = let
   11.25 -	fun type_of c = case (Sign.const_type sg' c) of Some t => t
   11.26 -				| None => error ("Unknown constructor: "^c);
   11.27 -	fun args_result_type (t as (Type(tn,[arg,rest]))) = 
   11.28 -		if tn = cfun_arrow orelse tn = "=>"
   11.29 -		then let val (ts,r) = args_result_type rest in (arg::ts,r) end
   11.30 -		else ([],t)
   11.31 -	|   args_result_type t = ([],t);
   11.32 -    in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in
   11.33 -	                 (cn,mk_var_names args,(args,res)) end)) cnstrss' 
   11.34 -	: (string * 			(* operator name of constr *)
   11.35 -	   string list *		(* argument name list *)
   11.36 -	   (typ list *			(* argument types *)
   11.37 -	    typ))			(* result type *)
   11.38 -	  list list end;
   11.39 -    fun test_equal_type tn (cn,_,(_,rt)) = fst (rep_Type rt) = tn orelse
   11.40 -		      error("Inappropriate result type for constructor "^cn);
   11.41 -    val typs = ListPair.map (fn (tn, cnstrs) =>(map (test_equal_type tn) cnstrs;
   11.42 -				snd(third(hd(cnstrs)))))  (typs',cnstrss);
   11.43 -    val test_typs = ListPair.map (fn (typ,cnstrs) => 
   11.44 -			if not (pcpo_type sg' typ)
   11.45 -			then error("Not a pcpo type: "^string_of_typ sg' typ)
   11.46 -			else map (fn (cn,_,(_,rt)) => rt=typ orelse error(
   11.47 -				"Non-identical result types for constructors "^
   11.48 -			        first(hd cnstrs)^" and "^ cn ))  cnstrs)
   11.49 -		    (typs,cnstrss);
   11.50 -    val proper_args = let
   11.51 -	fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
   11.52 -	|   occurs _  _              = false;
   11.53 -	fun proper_arg cn atyp = forall (fn typ => let 
   11.54 -				  val tn = fst (rep_Type typ) 
   11.55 -				  in atyp=typ orelse not (occurs tn atyp) orelse
   11.56 -				     error("Illegal use of type "^ tn ^
   11.57 -				   " as argument of constructor " ^cn)end )typs;
   11.58 -	fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
   11.59 -    in map (map proper_curry) cnstrss end;
   11.60 -  in (typs, flat cnstrss) end;
   11.61 -
   11.62  (* ----- calls for building new thy and thms -------------------------------- *)
   11.63  
   11.64  in
   11.65 @@ -130,22 +84,21 @@
   11.66      val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
   11.67      val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
   11.68      val dts  = map (Type o fst) eqs';
   11.69 +    fun strip ss = drop (find ("'", ss)+1, ss);
   11.70 +    fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
   11.71 +      | typid (TFree (id,_)   ) = hd (strip (tl (explode (Sign.base_name id))))
   11.72 +      | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
   11.73      fun cons cons' = (map (fn (con,syn,args) =>
   11.74 -	((ThyOps.const_name con syn),
   11.75 +	((Syntax.const_name con syn),
   11.76  	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
   11.77  					find (tp,dts) handle LIST "find" => ~1),
   11.78  					sel,vn))
   11.79 -	     (args,(mk_var_names(map third args)))
   11.80 +	     (args,(mk_var_names(map (typid o third) args)))
   11.81  	 )) cons') : cons list;
   11.82      val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
   11.83 -    val thy       = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
   11.84 +    val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
   11.85    in (foldl (fn (thy0,eq) => Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) 
   11.86                            |> Domain_Theorems.comp_theorems (comp_dnam, eqs) end;
   11.87  
   11.88 -  fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
   11.89 -   val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
   11.90 -  in
   11.91 -   Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
   11.92 -
   11.93  end (* local *)
   11.94  end (* struct *)
    12.1 --- a/src/HOLCF/domain/interface.ML	Tue Nov 04 14:37:51 1997 +0100
    12.2 +++ b/src/HOLCF/domain/interface.ML	Tue Nov 04 14:40:29 1997 +0100
    12.3 @@ -71,7 +71,7 @@
    12.4         ^ ";\n"
    12.5      end;
    12.6  
    12.7 -(* ----- string for calling (comp_)theorems and producing the structures ---- *)
    12.8 +(* ----- string for producing the structures -------------------------------- *)
    12.9  
   12.10      val val_gen_string =  let
   12.11        val comp_axioms   = [(* copy, *) "reach", "take_def", "finite_def"
   12.12 @@ -100,18 +100,6 @@
   12.13        "val thy = thy",
   12.14        "") end;
   12.15  
   12.16 -(* ----- strings for calling add_gen_by and producing the value binding ----- *)
   12.17 -
   12.18 -  fun mk_gen_by (finite,eqs) = let
   12.19 -      val typs    = map fst eqs;
   12.20 -      val cnstrss = map snd eqs;
   12.21 -      val tname = implode (separate "_" typs) in
   12.22 -      ("|> Domain_Extender.add_gen_by "
   12.23 -       ^ mk_pair(mk_pair(quote tname, Bool.toString finite),
   12.24 -		 mk_pair(mk_list(map quote typs), 
   12.25 -			 mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
   12.26 -       "val "^tname^"_induct = " ^get tname "induct" ^";") end;
   12.27 -
   12.28  (* ----- parser for domain declaration equation ----------------------------- *)
   12.29  
   12.30    val name' = name >> strip_quotes;
   12.31 @@ -122,7 +110,8 @@
   12.32  			|   esc ("]" ::xs) = "}"::esc xs
   12.33  			|   esc (x   ::xs) = x  ::esc xs
   12.34  		    in implode (esc (explode s)) end;
   12.35 -  val tvar = (type_var' ^^ optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
   12.36 +  val tvar = (type_var' ^^ 
   12.37 +	      optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
   12.38    fun type_args l = (tvar >> (fn x => [x])
   12.39                   ||  "(" $$-- !! (list1 tvar --$$ ")")
   12.40                   ||  empty >> K []) l
   12.41 @@ -131,20 +120,17 @@
   12.42                           to avoid ambiguity with standard mixfix option *)
   12.43    val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
   12.44  			  -- (optional ((name' >> Some) --$$ "::") None)
   12.45 -			  -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
   12.46 +			  -- typ --$$ ")" 
   12.47 +		    >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
   12.48  		 || typ >> (fn x => (false,None,x)) 
   12.49    val domain_cons = name' -- !! (repeat domain_arg) 
   12.50 -		    -- ThyOps.opt_cmixfix
   12.51 +		    -- ThyParse.opt_mixfix
   12.52  		    >> (fn ((con,args),syn) => (con,syn,args));
   12.53  in
   12.54    val domain_decl = (enum1 "and" (con_typ --$$ "="  -- !! 
   12.55  				 (enum1 "|" domain_cons))) >> mk_domain;
   12.56 -  val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
   12.57 -		    (enum1 "," (name'   --$$ "by" -- !!
   12.58 -			       (enum1 "|" name'))) >> mk_gen_by;
   12.59 -
   12.60    val _ = ThySyn.add_syntax
   12.61 -    ["lazy", "and", "by", "finite"]
   12.62 -    [("domain", domain_decl), ("generated", gen_by_decl)]
   12.63 +    ["lazy", "and"]
   12.64 +    [("domain", domain_decl)]
   12.65  
   12.66  end; (* local *)
    13.1 --- a/src/HOLCF/domain/library.ML	Tue Nov 04 14:37:51 1997 +0100
    13.2 +++ b/src/HOLCF/domain/library.ML	Tue Nov 04 14:40:29 1997 +0100
    13.3 @@ -39,6 +39,8 @@
    13.4  
    13.5  structure Domain_Library = struct
    13.6  
    13.7 +open HOLCFLogic;
    13.8 +
    13.9  exception Impossible of string;
   13.10  fun Imposs msg = raise Impossible ("Domain:"^msg);
   13.11  
   13.12 @@ -59,11 +61,7 @@
   13.13  (* make distinct names out of the type list, 
   13.14     forbidding "o", "x..","f..","P.." as names *)
   13.15  (* a number string is added if necessary *)
   13.16 -fun mk_var_names types : string list = let
   13.17 -    fun strip ss = drop (find ("'", ss)+1, ss);
   13.18 -    fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
   13.19 -      | typid (TFree (id,_)   ) = hd (strip (tl (explode (Sign.base_name id))))
   13.20 -      | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
   13.21 +fun mk_var_names ids : string list = let
   13.22      fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
   13.23      fun index_vnames(vn::vns,occupied) =
   13.24            (case assoc(occupied,vn) of
   13.25 @@ -73,13 +71,12 @@
   13.26             | Some(i) => (vn^(string_of_int (i+1)))
   13.27  				   :: index_vnames(vns,(vn,i+1)::occupied))
   13.28        | index_vnames([],occupied) = [];
   13.29 -in index_vnames(map (nonreserved o typid) types,[("O",0),("o",0)]) end;
   13.30 +in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
   13.31  
   13.32  fun rep_Type  (Type  x) = x | rep_Type  _ = Imposs "library:rep_Type";
   13.33  fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
   13.34  val tsig_of = #tsig o Sign.rep_sg;
   13.35 -val HOLCF_sg = sign_of HOLCF.thy;
   13.36 -val pcpoS = Sign.intern_sort HOLCF_sg ["pcpo"];
   13.37 +
   13.38  fun pcpo_type sg t = Type.of_sort (tsig_of sg) (Sign.certify_typ sg t, pcpoS);
   13.39  fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
   13.40  fun str2typ sg = typ_of o read_ctyp sg;
   13.41 @@ -107,12 +104,7 @@
   13.42  
   13.43  (* ----- support for type and mixfix expressions ----- *)
   13.44  
   13.45 -fun mk_tvar s = TFree("'"^s,pcpoS);
   13.46 -fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
   13.47  infixr 5 -->;
   13.48 -infixr 6 ~>; val op ~> = mk_typ "->";
   13.49 -val cfun_arrow = fst (rep_Type (dummyT ~> dummyT));
   13.50 -val NoSyn' = ThyOps.Mixfix NoSyn;
   13.51  
   13.52  (* ----- support for term expressions ----- *)
   13.53  
   13.54 @@ -140,9 +132,7 @@
   13.55  fun mk_constrain      (typ,T) = %%"_constrain" $ T $ tf typ;
   13.56  fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ);
   13.57  end;
   13.58 -			
   13.59  fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
   13.60 -fun mk_not     P  = Const("Not" ,boolT --> boolT) $ P;
   13.61  end;
   13.62  
   13.63  fun mk_All  (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *)
    14.1 --- a/src/HOLCF/domain/syntax.ML	Tue Nov 04 14:37:51 1997 +0100
    14.2 +++ b/src/HOLCF/domain/syntax.ML	Tue Nov 04 14:40:29 1997 +0100
    14.3 @@ -11,71 +11,67 @@
    14.4  local 
    14.5  
    14.6  open Domain_Library;
    14.7 -infixr 5 -->; infixr 6 ~>;
    14.8 -fun calc_syntax dtypeprod ((dname, typevars), (cons':
    14.9 -			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
   14.10 +infixr 5 -->; infixr 6 ->>;
   14.11 +fun calc_syntax dtypeprod ((dname, typevars), 
   14.12 +	(cons': (string * mixfix * (bool*string*typ) list) list)) =
   14.13  let
   14.14 -(* ----- constants concerning the isomorphism ------------------------------------- *)
   14.15 +(* ----- constants concerning the isomorphism ------------------------------- *)
   14.16  
   14.17  local
   14.18 -  fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
   14.19 -  fun prod     (_,_,args) = if args = [] then Type("one",[])
   14.20 -				         else foldr'(mk_typ "**") (map opt_lazy args);
   14.21 -  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
   14.22 -  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
   14.23 +  fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
   14.24 +  fun prod     (_,_,args) = if args = [] then oneT
   14.25 +			    else foldr' mk_sprodT (map opt_lazy args);
   14.26 +  fun freetvar s = let val tvar = mk_TFree s in
   14.27 +		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
   14.28 +  fun when_type (_   ,_,args) = foldr (op ->>) (map third args,freetvar "t");
   14.29  in
   14.30    val dtype  = Type(dname,typevars);
   14.31 -  val dtype2 = foldr' (mk_typ "++") (map prod cons');
   14.32 +  val dtype2 = foldr' mk_ssumT (map prod cons');
   14.33    val dnam = Sign.base_name dname;
   14.34 -  val const_rep  = (dnam^"_rep" ,              dtype  ~> dtype2, NoSyn');
   14.35 -  val const_abs  = (dnam^"_abs" ,              dtype2 ~> dtype , NoSyn');
   14.36 -  val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
   14.37 -					       	 dtype ~> freetvar "t"), NoSyn');
   14.38 -  val const_copy = (dnam^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
   14.39 +  val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   14.40 +  val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   14.41 +  val const_when = (dnam^"_when",foldr (op ->>) ((map when_type cons'),
   14.42 +					        dtype ->> freetvar "t"), NoSyn);
   14.43 +  val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
   14.44  end;
   14.45  
   14.46 -(* ----- constants concerning the constructors, discriminators and selectors ------ *)
   14.47 -
   14.48 -fun is_infix (ThyOps.CInfixl       _ ) = true
   14.49 -|   is_infix (ThyOps.CInfixr       _ ) = true
   14.50 -|   is_infix (ThyOps.Mixfix(Infixl _)) = true
   14.51 -|   is_infix (ThyOps.Mixfix(Infixr _)) = true
   14.52 -|   is_infix  _                        = false;
   14.53 +(* ----- constants concerning constructors, discriminators, and selectors --- *)
   14.54  
   14.55  local
   14.56    val escape = let
   14.57 -	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
   14.58 -							   else        c :: esc cs
   14.59 -	|   esc []        = []
   14.60 +	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
   14.61 +							 else      c::esc cs
   14.62 +	|   esc []      = []
   14.63  	in implode o esc o explode end;
   14.64 -  fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
   14.65 -  fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
   14.66 -			 	 ThyOps.Mixfix(Mixfix("is'_"^
   14.67 -				 (if is_infix s then Id else escape)con,[],max_pri)));
   14.68 -  fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
   14.69 +  fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
   14.70 +  fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
   14.71 +			   Mixfix(escape ("is_" ^ con), [], max_pri));
   14.72 +			(* stricly speaking, these constants have one argument,
   14.73 +			   but the mixfix (without arguments) is introduced only
   14.74 +			   to generate parse rules for non-alphanumeric names*)
   14.75 +  fun sel (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
   14.76  in
   14.77    val consts_con = map con cons';
   14.78    val consts_dis = map dis cons';
   14.79    val consts_sel = flat(map sel cons');
   14.80  end;
   14.81  
   14.82 -(* ----- constants concerning induction ------------------------------------------- *)
   14.83 +(* ----- constants concerning induction ------------------------------------- *)
   14.84  
   14.85 -  val const_take   = (dnam^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
   14.86 -  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
   14.87 +  val const_take   = (dnam^"_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
   14.88 +  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT       , NoSyn);
   14.89  
   14.90 -(* ----- case translation --------------------------------------------------------- *)
   14.91 +(* ----- case translation --------------------------------------------------- *)
   14.92  
   14.93  local open Syntax in
   14.94    val case_trans = let 
   14.95 -	fun c_ast con syn = Constant (ThyOps.const_name con syn);
   14.96 -	fun expvar n      = Variable ("e"^(string_of_int n));
   14.97 -	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
   14.98 +	fun c_ast con mx = Constant (const_name con mx);
   14.99 +	fun expvar n     = Variable ("e"^(string_of_int n));
  14.100 +	fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
  14.101 +					 (string_of_int m));
  14.102  	fun app s (l,r)   = mk_appl (Constant s) [l,r];
  14.103 -	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
  14.104 -		 [if is_infix syn
  14.105 -		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
  14.106 -		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
  14.107 +	fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
  14.108 +		 [foldl (app "fapp") (c_ast con mx, (mapn (argvar n) 1 args)),
  14.109  		  expvar n];
  14.110  	fun arg1 n (con,_,args) = if args = [] then expvar n 
  14.111  				  else mk_appl (Constant "LAM ") 
  14.112 @@ -83,10 +79,10 @@
  14.113    in
  14.114      ParsePrintRule
  14.115        (mk_appl (Constant "@case") [Variable "x", foldr'
  14.116 -				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
  14.117 +				(fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
  14.118  				 (mapn case1 1 cons')],
  14.119 -       mk_appl (Constant "@fapp") [foldl 
  14.120 -				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
  14.121 +       mk_appl (Constant "fapp") [foldl 
  14.122 +				(fn (w,a ) => mk_appl (Constant"fapp" ) [w,a ])
  14.123  				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
  14.124  				 Variable "x"])
  14.125    end;
  14.126 @@ -98,22 +94,23 @@
  14.127      [case_trans])
  14.128  end; (* let *)
  14.129  
  14.130 -(* ----- putting all the syntax stuff together ------------------------------------ *)
  14.131 +(* ----- putting all the syntax stuff together ------------------------------ *)
  14.132  
  14.133  in (* local *)
  14.134  
  14.135  fun add_syntax (comp_dnam,eqs': ((string * typ list) *
  14.136 -		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
  14.137 +	(string * mixfix * (bool*string*typ) list) list) list) thy'' =
  14.138  let
  14.139 -  val dtypes  = map (Type      o fst) eqs';
  14.140 -  val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
  14.141 -  val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
  14.142 -  val const_copy   = (comp_dnam^"_copy"  ,funprod ~> funprod       , NoSyn');
  14.143 -  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
  14.144 +  val dtypes  = map (Type o fst) eqs';
  14.145 +  val boolT   = HOLogic.boolT;
  14.146 +  val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
  14.147 +  val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
  14.148 +  val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
  14.149 +  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
  14.150    val ctt           = map (calc_syntax funprod) eqs';
  14.151 -  val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
  14.152 -in thy'' |> add_cur_ops_i (flat(map fst ctt))
  14.153 -	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
  14.154 +in thy'' |> ContConsts.add_consts_i (flat (map fst ctt) @ 
  14.155 +				    (if length eqs'>1 then [const_copy] else[])@
  14.156 +				    [const_bisim])
  14.157  	 |> Theory.add_trrules_i (flat(map snd ctt))
  14.158  end; (* let *)
  14.159  
    15.1 --- a/src/HOLCF/ex/Stream.thy	Tue Nov 04 14:37:51 1997 +0100
    15.2 +++ b/src/HOLCF/ex/Stream.thy	Tue Nov 04 14:40:29 1997 +0100
    15.3 @@ -8,7 +8,7 @@
    15.4  
    15.5  Stream = HOLCF + 
    15.6  
    15.7 -domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (cinfixr 65)
    15.8 +domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65)
    15.9  
   15.10  end
   15.11