tuned;
authorwenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14 ago)
changeset 168425979c46853d1
parent 16841 228d663cc9b3
child 16843 8ff9a80f3c93
tuned;
src/HOLCF/adm_tac.ML
src/HOLCF/cont_consts.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/skip_proof.ML
src/Pure/ROOT.ML
src/Pure/Tools/ROOT.ML
src/Pure/Tools/am_compiler.ML
src/Pure/Tools/am_interpreter.ML
src/Pure/Tools/am_util.ML
src/Pure/library.ML
src/Pure/meta_simplifier.ML
src/Pure/net.ML
     1.1 --- a/src/HOLCF/adm_tac.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/HOLCF/adm_tac.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -80,9 +80,9 @@
     1.4  
     1.5  
     1.6  (*figure out internal names*)
     1.7 -val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"];
     1.8 -val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
     1.9 -val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm";
    1.10 +val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
    1.11 +val cont_name = Sign.intern_const (the_context ()) "cont";
    1.12 +val adm_name = Sign.intern_const (the_context ()) "adm";
    1.13  
    1.14  
    1.15  (*** check whether type of terms in list is chain finite ***)
     2.1 --- a/src/HOLCF/cont_consts.ML	Thu Jul 14 19:28:23 2005 +0200
     2.2 +++ b/src/HOLCF/cont_consts.ML	Thu Jul 14 19:28:24 2005 +0200
     2.3 @@ -80,7 +80,7 @@
     2.4  
     2.5  fun gen_add_consts prep_typ raw_decls thy =
     2.6    let
     2.7 -    val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls;
     2.8 +    val decls = map (upd_second (Thm.typ_of o prep_typ thy)) raw_decls;
     2.9      val (contconst_decls, normal_decls) = List.partition is_contconst decls;
    2.10      val transformed_decls = map transform contconst_decls;
    2.11    in
     3.1 --- a/src/HOLCF/domain/axioms.ML	Thu Jul 14 19:28:23 2005 +0200
     3.2 +++ b/src/HOLCF/domain/axioms.ML	Thu Jul 14 19:28:24 2005 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
     3.5  
     3.6    fun con_def outer recu m n (_,args) = let
     3.7 -     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id)
     3.8 +     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I)
     3.9  			(if recu andalso is_rec arg then (cproj (Bound z) eqs
    3.10  				  (rec_of arg))`Bound(z-x) else Bound(z-x));
    3.11       fun parms [] = %%:ONE_N
    3.12 @@ -47,7 +47,7 @@
    3.13  
    3.14    val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo 
    3.15  	Library.foldl (op `) (%%:(dname^"_when") , 
    3.16 -	              mapn (con_def Id true (length cons)) 0 cons)));
    3.17 +	              mapn (con_def I true (length cons)) 0 cons)));
    3.18  
    3.19  (* -- definitions concerning the constructors, discriminators and selectors - *)
    3.20  
    3.21 @@ -75,7 +75,7 @@
    3.22  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    3.23  			(fn (con',args) => if con'<>con then UU else
    3.24  			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    3.25 -	in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    3.26 +	in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    3.27  
    3.28  
    3.29  (* ----- axiom and definitions concerning induction ------------------------- *)
     4.1 --- a/src/HOLCF/domain/library.ML	Thu Jul 14 19:28:23 2005 +0200
     4.2 +++ b/src/HOLCF/domain/library.ML	Thu Jul 14 19:28:24 2005 +0200
     4.3 @@ -8,8 +8,6 @@
     4.4  
     4.5  (* ----- general support ---------------------------------------------------- *)
     4.6  
     4.7 -fun Id x = x;
     4.8 -
     4.9  fun mapn f n []      = []
    4.10  |   mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
    4.11  
    4.12 @@ -17,7 +15,7 @@
    4.13  			     | itr [a] = f2 a
    4.14  			     | itr (a::l) = f(a, itr l)
    4.15  in  itr l  end;
    4.16 -fun foldr' f l = foldr'' f (l,Id);
    4.17 +fun foldr' f l = foldr'' f (l,I);
    4.18  fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
    4.19  						  (y::ys,res2)) ([],start) xs;
    4.20  
    4.21 @@ -175,9 +173,9 @@
    4.22  infixr 0 ==>;   fun S ==> T = mk_trp S ===> mk_trp T;
    4.23  infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    4.24  infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
    4.25 -infix 1 ~=;     fun S ~=  T = mk_not (S === T);
    4.26 +infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
    4.27  infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
    4.28 -infix 1 ~<<;    fun S ~<< T = mk_not (S << T);
    4.29 +infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
    4.30  
    4.31  infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
    4.32  infix 9 `% ; fun f`% s = f` %: s;
    4.33 @@ -186,7 +184,7 @@
    4.34  fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args);
    4.35  fun con_app con = con_app2 con %#;
    4.36  fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
    4.37 -fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
    4.38 +fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
    4.39  fun prj _  _  x (   _::[]) _ = x
    4.40  |   prj f1 _  x (_::y::ys) 0 = f1 x y
    4.41  |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
    4.42 @@ -195,11 +193,11 @@
    4.43  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
    4.44  fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
    4.45  fun prj' _  _  x (   _::[]) _ = x
    4.46 -|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' mk_prodT ys)
    4.47 +|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' HOLogic.mk_prodT ys)
    4.48  |   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
    4.49  fun cproj' T eqs = prj'
    4.50 -	(fn S => fn t => Const(cfstN,mk_prodT(dummyT,t)->>dummyT)`S)
    4.51 -	(fn S => fn t => Const(csndN,mk_prodT(t,dummyT)->>dummyT)`S) 
    4.52 +	(fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
    4.53 +	(fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S) 
    4.54  		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
    4.55  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
    4.56  
    4.57 @@ -215,7 +213,7 @@
    4.58  |   mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
    4.59  fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
    4.60  |   mk_ctupleT (T::[]) = T
    4.61 -|   mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts);
    4.62 +|   mk_ctupleT (T::Ts) = HOLogic.mk_prodT(T, mk_ctupleT Ts);
    4.63  fun lift_defined f = lift (fn x => defined (f x));
    4.64  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
    4.65  
    4.66 @@ -236,13 +234,13 @@
    4.67  	|   one_fun n (_,args) = let
    4.68  		val l2 = length args;
    4.69  		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
    4.70 -					         else Id) (Bound(l2-m));
    4.71 +					         else I) (Bound(l2-m));
    4.72  		in cont_eta_contract (foldr'' 
    4.73  			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
    4.74  			(args,
    4.75  			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
    4.76  			) end;
    4.77  in (if length cons = 1 andalso length(snd(hd cons)) <= 1
    4.78 -    then fn t => %%:strictifyN`t else Id)
    4.79 +    then fn t => %%:strictifyN`t else I)
    4.80       (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
    4.81  end; (* struct *)
     5.1 --- a/src/HOLCF/domain/syntax.ML	Thu Jul 14 19:28:23 2005 +0200
     5.2 +++ b/src/HOLCF/domain/syntax.ML	Thu Jul 14 19:28:24 2005 +0200
     5.3 @@ -105,8 +105,8 @@
     5.4  let
     5.5    val dtypes  = map (Type o fst) eqs';
     5.6    val boolT   = HOLogic.boolT;
     5.7 -  val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
     5.8 -  val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
     5.9 +  val funprod = foldr' HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
    5.10 +  val relprod = foldr' HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
    5.11    val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
    5.12    val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
    5.13    val ctt           = map (calc_syntax funprod) eqs';
     6.1 --- a/src/HOLCF/domain/theorems.ML	Thu Jul 14 19:28:23 2005 +0200
     6.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Jul 14 19:28:24 2005 +0200
     6.3 @@ -6,6 +6,7 @@
     6.4  Proof generator for domain section.
     6.5  *)
     6.6  
     6.7 +val HOLCF_ss = simpset();
     6.8  
     6.9  structure Domain_Theorems = struct
    6.10  
    6.11 @@ -233,7 +234,7 @@
    6.12                                                    (List.nth(vns,n))] else [])
    6.13                       @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
    6.14  in List.concat(map  (fn (c,args) => 
    6.15 -     List.concat(List.mapPartial Id (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
    6.16 +     List.concat(List.mapPartial I (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
    6.17  val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==> 
    6.18                          defined(%%:sel`%x_name)) [
    6.19                                  rtac casedist 1,
    6.20 @@ -442,7 +443,7 @@
    6.21      fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
    6.22      fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (warning
    6.23          ("domain "^List.nth(dnames,n)^" is empty!"); true) else false;
    6.24 -    fun lazy_rec_to ns = rec_to exists Id  lazy_rec_to ns;
    6.25 +    fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
    6.26  
    6.27    in val n__eqs     = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
    6.28       val is_emptys = map warn n__eqs;
     7.1 --- a/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:23 2005 +0200
     7.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:24 2005 +0200
     7.3 @@ -118,11 +118,10 @@
     7.4      |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
     7.5      |> Proof.fix_i [([thesisN], NONE)]
     7.6      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
     7.7 -    |> (fn state' =>
     7.8 -        state'
     7.9 -        |> Proof.from_facts chain_facts
    7.10 -        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    7.11 -        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
    7.12 +    |> `Proof.the_facts
    7.13 +    ||> Proof.from_facts chain_facts
    7.14 +    ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    7.15 +    |-> (fn facts => Method.refine (Method.Basic (K (Method.insert facts))))
    7.16    end;
    7.17  
    7.18  val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
     8.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:23 2005 +0200
     8.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:24 2005 +0200
     8.3 @@ -41,13 +41,13 @@
     8.4  (* basic cheating *)
     8.5  
     8.6  fun make_thm thy t =
     8.7 -  Thm.invoke_oracle_i thy "Pure.skip_proof" (Theory.sign_of thy, SkipProof t);
     8.8 +  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
     8.9  
    8.10  fun cheat_tac thy st =
    8.11    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    8.12  
    8.13  fun prove thy xs asms prop tac =
    8.14 -  Tactic.prove (Theory.sign_of thy) xs asms prop
    8.15 +  Tactic.prove thy xs asms prop
    8.16      (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
    8.17  
    8.18  
     9.1 --- a/src/Pure/ROOT.ML	Thu Jul 14 19:28:23 2005 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Thu Jul 14 19:28:24 2005 +0200
     9.3 @@ -1,9 +1,7 @@
     9.4  (*  Title:      Pure/ROOT.ML
     9.5      ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1993  University of Cambridge
     9.8  
     9.9 -Root file for Pure Isabelle.
    9.10 +Pure Isabelle.
    9.11  *)
    9.12  
    9.13  val banner = "Pure Isabelle";
    9.14 @@ -93,10 +91,8 @@
    9.15  (*configuration for Proof General*)
    9.16  use "proof_general.ML";
    9.17  
    9.18 -(* loading the Tools directory *)
    9.19  cd "Tools"; use "ROOT.ML"; cd "..";
    9.20  
    9.21 -(*the Pure theories*)
    9.22  use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
    9.23  use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
    9.24  
    10.1 --- a/src/Pure/Tools/ROOT.ML	Thu Jul 14 19:28:23 2005 +0200
    10.2 +++ b/src/Pure/Tools/ROOT.ML	Thu Jul 14 19:28:24 2005 +0200
    10.3 @@ -1,8 +1,11 @@
    10.4  (*  Title:      Pure/Tools/ROOT.ML
    10.5      ID:         $Id$
    10.6 +
    10.7 +Miscellaneous tools and packages for Pure Isabelle.
    10.8  *)
    10.9  
   10.10 +(*Steven Obua's evaluator*)
   10.11  use "am_interpreter.ML";
   10.12 -use "am_compiler.ML"; 
   10.13 +use "am_compiler.ML";
   10.14  use "am_util.ML";
   10.15  use "compute.ML";
    11.1 --- a/src/Pure/Tools/am_compiler.ML	Thu Jul 14 19:28:23 2005 +0200
    11.2 +++ b/src/Pure/Tools/am_compiler.ML	Thu Jul 14 19:28:24 2005 +0200
    11.3 @@ -5,14 +5,14 @@
    11.4  
    11.5  signature COMPILING_AM = 
    11.6  sig
    11.7 -    include ABSTRACT_MACHINE
    11.8 +  include ABSTRACT_MACHINE
    11.9  
   11.10 -    datatype closure = CVar of int | CConst of int
   11.11 -		     | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
   11.12 +  datatype closure = CVar of int | CConst of int
   11.13 +    | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
   11.14  
   11.15 -    val set_compiled_rewriter : (term -> closure) -> unit
   11.16 -    val list_nth : 'a list * int -> 'a
   11.17 -    val list_map : ('a -> 'b) -> 'a list -> 'b list
   11.18 +  val set_compiled_rewriter : (term -> closure) -> unit
   11.19 +  val list_nth : 'a list * int -> 'a
   11.20 +  val list_map : ('a -> 'b) -> 'a list -> 'b list
   11.21  end
   11.22  
   11.23  structure AM_Compiler :> COMPILING_AM = struct
   11.24 @@ -25,7 +25,8 @@
   11.25  datatype pattern = PVar | PConst of int * (pattern list)
   11.26  
   11.27  datatype closure = CVar of int | CConst of int
   11.28 -		 | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
   11.29 +	         | CApp of closure * closure | CAbs of closure
   11.30 +                 | Closure of (closure list) * closure
   11.31  
   11.32  val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
   11.33  
   11.34 @@ -47,19 +48,22 @@
   11.35    | term_of_clos (CConst c) = Const c
   11.36    | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
   11.37    | term_of_clos (CAbs u) = Abs (term_of_clos u)
   11.38 -  | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
   11.39 +  | term_of_clos (Closure (e, u)) =
   11.40 +      raise (Run "internal error: closure in normalized term found")
   11.41  
   11.42  fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
   11.43    | strip_closure args x = (x, args)
   11.44  
   11.45 -(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
   11.46 +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
   11.47 +  check_freevars 0 t iff t is closed*)
   11.48  fun check_freevars free (Var x) = x < free
   11.49    | check_freevars free (Const c) = true
   11.50    | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
   11.51    | check_freevars free (Abs m) = check_freevars (free+1) m
   11.52  
   11.53  fun count_patternvars PVar = 1
   11.54 -  | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
   11.55 +  | count_patternvars (PConst (_, ps)) =
   11.56 +      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
   11.57  
   11.58  fun print_rule (p, t) = 
   11.59      let	
   11.60 @@ -81,17 +85,22 @@
   11.61  	    end
   11.62  
   11.63  	val (n, pattern) = print_pattern 0 p
   11.64 -	val pattern = if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")" else pattern
   11.65 +	val pattern =
   11.66 +            if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")"
   11.67 +            else pattern
   11.68  	
   11.69 -	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) "Var "^(str x)
   11.70 -	  | print_term d (Const c) = "c"^(str c)
   11.71 -	  | print_term d (App (a,b)) = "App ("^(print_term d a)^", "^(print_term d b)^")"
   11.72 -	  | print_term d (Abs c) = "Abs ("^(print_term (d+1) c)^")"
   11.73 +	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
   11.74 +              "Var " ^ str x
   11.75 +	  | print_term d (Const c) = "c" ^ str c
   11.76 +	  | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
   11.77 +	  | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
   11.78  
   11.79  	fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))
   11.80  
   11.81  	val term = print_term 0 t
   11.82 -	val term = if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")" else "Closure ([], "^term^")"
   11.83 +	val term =
   11.84 +            if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
   11.85 +            else "Closure ([], "^term^")"
   11.86  			   
   11.87      in
   11.88  	"lookup stack "^pattern^" = weak stack ("^term^")"
   11.89 @@ -104,7 +113,7 @@
   11.90    | remove_dups [] = []
   11.91  
   11.92  fun constants_of PVar = []
   11.93 -  | constants_of (PConst (c, ps)) = c::(List.concat (map constants_of ps))
   11.94 +  | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
   11.95  
   11.96  fun constants_of_term (Var _) = []
   11.97    | constants_of_term (Abs m) = constants_of_term m
   11.98 @@ -113,6 +122,7 @@
   11.99      
  11.100  fun load_rules sname name prog = 
  11.101      let
  11.102 +        (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
  11.103  	val buffer = ref ""
  11.104  	fun write s = (buffer := (!buffer)^s)
  11.105  	fun writeln s = (write s; write "\n")
  11.106 @@ -210,11 +220,9 @@
  11.107  	    in
  11.108  		()
  11.109  	    end
  11.110 -	    
  11.111 -	val dummy = (fn s => ())		    
  11.112      in
  11.113  	compiled_rewriter := NONE;	
  11.114 -	use_text (dummy, dummy) false (!buffer);
  11.115 +	use_text (K (), K ()) false (!buffer);
  11.116  	case !compiled_rewriter of 
  11.117  	    NONE => raise (Compile "cannot communicate with compiled function")
  11.118  	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
    12.1 --- a/src/Pure/Tools/am_interpreter.ML	Thu Jul 14 19:28:23 2005 +0200
    12.2 +++ b/src/Pure/Tools/am_interpreter.ML	Thu Jul 14 19:28:24 2005 +0200
    12.3 @@ -3,7 +3,9 @@
    12.4      Author:     Steven Obua
    12.5  *)
    12.6  
    12.7 -signature ABSTRACT_MACHINE = sig							     
    12.8 +signature ABSTRACT_MACHINE =
    12.9 +sig
   12.10 +
   12.11  datatype term = Var of int | Const of int | App of term * term | Abs of term
   12.12  
   12.13  datatype pattern = PVar | PConst of int * (pattern list)
   12.14 @@ -12,7 +14,7 @@
   12.15  
   12.16  exception Compile of string;
   12.17  val compile : (pattern * term) list -> program
   12.18 - 
   12.19 +
   12.20  exception Run of string;
   12.21  val run : program -> term -> term
   12.22  
   12.23 @@ -25,8 +27,8 @@
   12.24  datatype pattern = PVar | PConst of int * (pattern list)
   12.25  
   12.26  datatype closure = CVar of int | CConst of int
   12.27 -		 | CApp of closure * closure | CAbs of closure 
   12.28 -		 | Closure of (closure list) * closure 
   12.29 +                 | CApp of closure * closure | CAbs of closure
   12.30 +                 | Closure of (closure list) * closure
   12.31  
   12.32  structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
   12.33  
   12.34 @@ -57,22 +59,22 @@
   12.35  
   12.36  (* earlier occurrence of PVar corresponds to higher de Bruijn index *)
   12.37  fun pattern_match args PVar clos = SOME (clos::args)
   12.38 -  | pattern_match args (PConst (c, patterns)) clos = 
   12.39 +  | pattern_match args (PConst (c, patterns)) clos =
   12.40      let
   12.41 -	val (f, closargs) = strip_closure [] clos
   12.42 +        val (f, closargs) = strip_closure [] clos
   12.43      in
   12.44 -	case f of 
   12.45 -	    CConst d => 
   12.46 -	    if c = d then 
   12.47 -		pattern_match_list args patterns closargs
   12.48 -	    else 
   12.49 -		NONE
   12.50 -	  | _ => NONE
   12.51 +        case f of
   12.52 +            CConst d =>
   12.53 +            if c = d then
   12.54 +                pattern_match_list args patterns closargs
   12.55 +            else
   12.56 +                NONE
   12.57 +          | _ => NONE
   12.58      end
   12.59  and pattern_match_list args [] [] = SOME args
   12.60 -  | pattern_match_list args (p::ps) (c::cs) = 
   12.61 +  | pattern_match_list args (p::ps) (c::cs) =
   12.62      (case pattern_match args p c of
   12.63 -	NONE => NONE
   12.64 +        NONE => NONE
   12.65        | SOME args => pattern_match_list args ps cs)
   12.66    | pattern_match_list _ _ _ = NONE
   12.67  
   12.68 @@ -88,26 +90,26 @@
   12.69  fun pattern_key (PConst (c, ps)) = (c, length ps)
   12.70    | pattern_key _ = raise (Compile "pattern reduces to variable")
   12.71  
   12.72 -fun compile eqs = 
   12.73 +fun compile eqs =
   12.74      let
   12.75 -	val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r; 
   12.76 -				     (pattern_key p, (p, clos_of_term r)))) eqs
   12.77 +        val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
   12.78 +                                     (pattern_key p, (p, clos_of_term r)))) eqs
   12.79      in
   12.80 -	prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
   12.81 -    end	
   12.82 +        prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
   12.83 +    end
   12.84  
   12.85  fun match_rules n [] clos = NONE
   12.86    | match_rules n ((p,eq)::rs) clos =
   12.87      case pattern_match [] p clos of
   12.88 -	NONE => match_rules (n+1) rs clos
   12.89 +        NONE => match_rules (n+1) rs clos
   12.90        | SOME args => SOME (Closure (args, eq))
   12.91  
   12.92 -fun match_closure prog clos = 
   12.93 +fun match_closure prog clos =
   12.94      case len_head_of_closure 0 clos of
   12.95 -	(len, CConst c) =>
   12.96 -	(case prog_struct.lookup (prog, (c, len)) of
   12.97 -	    NONE => NONE
   12.98 -	  | SOME rules => match_rules 0 rules clos)
   12.99 +        (len, CConst c) =>
  12.100 +        (case prog_struct.lookup (prog, (c, len)) of
  12.101 +            NONE => NONE
  12.102 +          | SOME rules => match_rules 0 rules clos)
  12.103        | _ => NONE
  12.104  
  12.105  fun lift n (c as (CConst _)) = c
  12.106 @@ -121,21 +123,21 @@
  12.107    | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
  12.108    | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
  12.109    | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
  12.110 -  | weak prog stack clos =    
  12.111 +  | weak prog stack clos =
  12.112      case match_closure prog clos of
  12.113 -	NONE => weak_last prog stack clos
  12.114 +        NONE => weak_last prog stack clos
  12.115        | SOME r => weak prog stack r
  12.116  and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
  12.117    | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
  12.118 -  | weak_last prog stack c = (stack, c) 
  12.119 +  | weak_last prog stack c = (stack, c)
  12.120  
  12.121 -fun strong prog stack (Closure (e, CAbs m)) = 
  12.122 +fun strong prog stack (Closure (e, CAbs m)) =
  12.123      let
  12.124 -	val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
  12.125 +        val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
  12.126      in
  12.127 -	case stack' of
  12.128 -	    SEmpty => strong prog (SAbs stack) wnf
  12.129 -	  | _ => raise (Run "internal error in strong: weak failed")
  12.130 +        case stack' of
  12.131 +            SEmpty => strong prog (SAbs stack) wnf
  12.132 +          | _ => raise (Run "internal error in strong: weak failed")
  12.133      end
  12.134    | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
  12.135    | strong prog stack clos = strong_last prog stack clos
  12.136 @@ -144,17 +146,17 @@
  12.137    | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
  12.138    | strong_last prog stack clos = (stack, clos)
  12.139  
  12.140 -fun run prog t = 
  12.141 +fun run prog t =
  12.142      let
  12.143 -	val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
  12.144 +        val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
  12.145      in
  12.146 -	case stack of 
  12.147 -	    SEmpty => (case strong prog SEmpty wnf of
  12.148 -			   (SEmpty, snf) => term_of_clos snf
  12.149 -			 | _ => raise (Run "internal error in run: strong failed"))
  12.150 -	  | _ => raise (Run "internal error in run: weak failed")
  12.151 +        case stack of
  12.152 +            SEmpty => (case strong prog SEmpty wnf of
  12.153 +                           (SEmpty, snf) => term_of_clos snf
  12.154 +                         | _ => raise (Run "internal error in run: strong failed"))
  12.155 +          | _ => raise (Run "internal error in run: weak failed")
  12.156      end
  12.157 -	  
  12.158 +
  12.159  end
  12.160  
  12.161  structure AbstractMachine = AM_Interpreter
    13.1 --- a/src/Pure/Tools/am_util.ML	Thu Jul 14 19:28:23 2005 +0200
    13.2 +++ b/src/Pure/Tools/am_util.ML	Thu Jul 14 19:28:24 2005 +0200
    13.3 @@ -4,11 +4,11 @@
    13.4  *)
    13.5  
    13.6  signature AM_UTIL = sig
    13.7 -    
    13.8 +
    13.9      type naming = string -> int
   13.10  
   13.11      exception Parse of string
   13.12 -    exception Tokenize 
   13.13 +    exception Tokenize
   13.14  
   13.15      (* takes a naming for the constants *)
   13.16      val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
   13.17 @@ -25,7 +25,8 @@
   13.18  
   13.19  fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
   13.20    | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
   13.21 -  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) = (prod_ord term_ord term_ord) (a1, a2)
   13.22 +  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
   13.23 +      prod_ord term_ord term_ord (a1, a2)
   13.24    | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
   13.25    | term_ord (AbstractMachine.Const _, _) = LESS
   13.26    | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
   13.27 @@ -36,68 +37,72 @@
   13.28  
   13.29  type naming = string -> int
   13.30  
   13.31 -datatype token = TokenConst of string | TokenLeft | TokenRight | TokenVar of string | TokenLambda | TokenDot | TokenNone | TokenEq
   13.32 +datatype token =
   13.33 +  TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
   13.34 +  TokenLambda | TokenDot | TokenNone | TokenEq
   13.35  
   13.36  exception Tokenize;
   13.37  
   13.38  fun tokenize s =
   13.39      let
   13.40 -	val s = String.explode s
   13.41 -	fun str c = Char.toString c
   13.42 -	fun app s c = s^(str c)
   13.43 -	fun tz TokenNone [] = []
   13.44 -	  | tz x [] = [x]
   13.45 -	  | tz TokenNone (c::cs) = 
   13.46 -	    if Char.isSpace c then tz TokenNone cs
   13.47 -	    else if Char.isLower c then (tz (TokenVar (str c)) cs)
   13.48 -	    else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
   13.49 -	    else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
   13.50 -	    else if c = #"." then (TokenDot :: (tz TokenNone cs))
   13.51 -	    else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
   13.52 -	    else if c = #")" then (TokenRight :: (tz TokenNone cs))
   13.53 -	    else if c = #"=" then (TokenEq :: (tz TokenNone cs))
   13.54 -	    else raise Tokenize
   13.55 -	  | tz (TokenConst s) (c::cs) = 
   13.56 -	    if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
   13.57 -	    else (TokenConst s)::(tz TokenNone (c::cs))
   13.58 -	  | tz (TokenVar s) (c::cs) = 
   13.59 -	    if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
   13.60 -	    else (TokenVar s)::(tz TokenNone (c::cs))
   13.61 -	  | tz _ _ = raise Tokenize
   13.62 +        val s = String.explode s
   13.63 +        fun str c = Char.toString c
   13.64 +        fun app s c = s^(str c)
   13.65 +        fun tz TokenNone [] = []
   13.66 +          | tz x [] = [x]
   13.67 +          | tz TokenNone (c::cs) =
   13.68 +            if Char.isSpace c then tz TokenNone cs
   13.69 +            else if Char.isLower c then (tz (TokenVar (str c)) cs)
   13.70 +            else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
   13.71 +            else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
   13.72 +            else if c = #"." then (TokenDot :: (tz TokenNone cs))
   13.73 +            else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
   13.74 +            else if c = #")" then (TokenRight :: (tz TokenNone cs))
   13.75 +            else if c = #"=" then (TokenEq :: (tz TokenNone cs))
   13.76 +            else raise Tokenize
   13.77 +          | tz (TokenConst s) (c::cs) =
   13.78 +            if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
   13.79 +            else (TokenConst s)::(tz TokenNone (c::cs))
   13.80 +          | tz (TokenVar s) (c::cs) =
   13.81 +            if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
   13.82 +            else (TokenVar s)::(tz TokenNone (c::cs))
   13.83 +          | tz _ _ = raise Tokenize
   13.84      in
   13.85 -	tz TokenNone s
   13.86 +        tz TokenNone s
   13.87      end
   13.88  
   13.89  exception Parse of string;
   13.90  
   13.91 -fun cons x xs = if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x)) else (x::xs)
   13.92 +fun cons x xs =
   13.93 +  if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
   13.94 +  else (x::xs)
   13.95  
   13.96 -fun parse_pattern f pvars ((TokenConst c)::ts) = 
   13.97 +fun parse_pattern f pvars ((TokenConst c)::ts) =
   13.98      let
   13.99 -	val (pvars, ts, plist) = parse_pattern_list f pvars ts
  13.100 +        val (pvars, ts, plist) = parse_pattern_list f pvars ts
  13.101      in
  13.102 -	(pvars, ts, AbstractMachine.PConst (f c, plist))
  13.103 +        (pvars, ts, AbstractMachine.PConst (f c, plist))
  13.104      end
  13.105    | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
  13.106 -and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)	
  13.107 +and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
  13.108    | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
  13.109 -  | parse_pattern_single f pvars (TokenLeft::ts) = 
  13.110 +  | parse_pattern_single f pvars (TokenLeft::ts) =
  13.111      let
  13.112 -	val (pvars, ts, p) = parse_pattern f pvars ts
  13.113 +        val (pvars, ts, p) = parse_pattern f pvars ts
  13.114      in
  13.115 -	case ts of
  13.116 -	    TokenRight::ts => (pvars, ts, p)
  13.117 -	  | _ => raise (Parse "parse_pattern_single: closing bracket expected")
  13.118 +        case ts of
  13.119 +            TokenRight::ts => (pvars, ts, p)
  13.120 +          | _ => raise (Parse "parse_pattern_single: closing bracket expected")
  13.121      end
  13.122    | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
  13.123  and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
  13.124    | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
  13.125 -  | parse_pattern_list f pvars ts = 
  13.126 +  | parse_pattern_list f pvars ts =
  13.127      let
  13.128 -	val (pvars, ts, p) = parse_pattern_single f pvars ts
  13.129 -	val (pvars, ts, ps) = parse_pattern_list f pvars ts
  13.130 +        val (pvars, ts, p) = parse_pattern_single f pvars ts
  13.131 +        val (pvars, ts, ps) = parse_pattern_list f pvars ts
  13.132      in
  13.133 -	(pvars, ts, p::ps)
  13.134 +        (pvars, ts, p::ps)
  13.135      end
  13.136  
  13.137  fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
  13.138 @@ -105,66 +110,66 @@
  13.139  
  13.140  fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
  13.141    | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
  13.142 -  | parse_term_single f vars (TokenLeft::ts) = 
  13.143 +  | parse_term_single f vars (TokenLeft::ts) =
  13.144      let
  13.145 -	val (ts, term) = parse_term f vars ts
  13.146 +        val (ts, term) = parse_term f vars ts
  13.147      in
  13.148 -	case ts of 
  13.149 -	    TokenRight::ts => (ts, term)
  13.150 -	  | _ => raise Parse ("parse_term_single: closing bracket expected")
  13.151 +        case ts of
  13.152 +            TokenRight::ts => (ts, term)
  13.153 +          | _ => raise Parse ("parse_term_single: closing bracket expected")
  13.154      end
  13.155 -  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) = 
  13.156 +  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
  13.157      let
  13.158 -	val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
  13.159 +        val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
  13.160      in
  13.161 -	(ts, AbstractMachine.Abs term)
  13.162 +        (ts, AbstractMachine.Abs term)
  13.163      end
  13.164    | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
  13.165  and parse_term_list f vars [] = ([], [])
  13.166    | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
  13.167 -  | parse_term_list f vars ts = 
  13.168 +  | parse_term_list f vars ts =
  13.169      let
  13.170 -	val (ts, term) = parse_term_single f vars ts
  13.171 -	val (ts, terms) = parse_term_list f vars ts
  13.172 +        val (ts, term) = parse_term_single f vars ts
  13.173 +        val (ts, terms) = parse_term_list f vars ts
  13.174      in
  13.175 -	(ts, term::terms)
  13.176 +        (ts, term::terms)
  13.177      end
  13.178 -and parse_term f vars ts = 
  13.179 +and parse_term f vars ts =
  13.180      let
  13.181 -	val (ts, terms) = parse_term_list f vars ts
  13.182 +        val (ts, terms) = parse_term_list f vars ts
  13.183      in
  13.184 -	case terms of 
  13.185 -	    [] => raise (Parse "parse_term: no term found")
  13.186 -	  | (t::terms) => (ts, app_terms t terms)
  13.187 +        case terms of
  13.188 +            [] => raise (Parse "parse_term: no term found")
  13.189 +          | (t::terms) => (ts, app_terms t terms)
  13.190      end
  13.191  
  13.192 -fun read_rule f s = 
  13.193 +fun read_rule f s =
  13.194      let
  13.195 -	val t = tokenize s
  13.196 -	val (v, ts, pattern) = parse_pattern f [] t
  13.197 -	fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
  13.198 -	  | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
  13.199 +        val t = tokenize s
  13.200 +        val (v, ts, pattern) = parse_pattern f [] t
  13.201 +        fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
  13.202 +          | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
  13.203      in
  13.204 -	case ts of 
  13.205 -	    TokenEq::ts => 
  13.206 -	    let
  13.207 -		val (ts, term) = parse_term f (vars v) ts
  13.208 -	    in
  13.209 -		case ts of 
  13.210 -		    [] => (pattern, term)
  13.211 -		  | _ => raise (Parse "read_rule: still tokens left, end expected")
  13.212 -	    end
  13.213 -	  | _ => raise (Parse ("read_rule: = expected"))
  13.214 +        case ts of
  13.215 +            TokenEq::ts =>
  13.216 +            let
  13.217 +                val (ts, term) = parse_term f (vars v) ts
  13.218 +            in
  13.219 +                case ts of
  13.220 +                    [] => (pattern, term)
  13.221 +                  | _ => raise (Parse "read_rule: still tokens left, end expected")
  13.222 +            end
  13.223 +          | _ => raise (Parse ("read_rule: = expected"))
  13.224      end
  13.225  
  13.226 -fun read_term f g s = 
  13.227 +fun read_term f g s =
  13.228      let
  13.229 -	val t = tokenize s
  13.230 -	val (ts, term) = parse_term f g t
  13.231 +        val t = tokenize s
  13.232 +        val (ts, term) = parse_term f g t
  13.233      in
  13.234 -	case ts of 
  13.235 -	    [] => term
  13.236 -	  | _ => raise (Parse ("read_term: still tokens left, end expected"))
  13.237 +        case ts of
  13.238 +            [] => term
  13.239 +          | _ => raise (Parse ("read_term: still tokens left, end expected"))
  13.240      end
  13.241  
  13.242  end
    14.1 --- a/src/Pure/library.ML	Thu Jul 14 19:28:23 2005 +0200
    14.2 +++ b/src/Pure/library.ML	Thu Jul 14 19:28:24 2005 +0200
    14.3 @@ -8,19 +8,20 @@
    14.4  tables, balanced trees, orders, current directory, misc.
    14.5  *)
    14.6  
    14.7 -infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    14.8 -  mem mem_int mem_string union union_int union_string inter inter_int
    14.9 -  inter_string subset subset_int subset_string;
   14.10 +infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
   14.11 +  orf andf prefix upto downto mem mem_int mem_string union union_int
   14.12 +  union_string inter inter_int inter_string subset subset_int
   14.13 +  subset_string;
   14.14  
   14.15  infix 3 oo ooo oooo;
   14.16  
   14.17  signature BASIC_LIBRARY =
   14.18  sig
   14.19    (*functions*)
   14.20 +  val I: 'a -> 'a
   14.21 +  val K: 'a -> 'b -> 'a
   14.22    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   14.23    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   14.24 -  val I: 'a -> 'a
   14.25 -  val K: 'a -> 'b -> 'a
   14.26    val |> : 'a * ('a -> 'b) -> 'b
   14.27    val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
   14.28    val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
   14.29 @@ -33,9 +34,9 @@
   14.30    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
   14.31    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
   14.32    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
   14.33 +  val funpow: int -> ('a -> 'a) -> 'a -> 'a
   14.34    val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
   14.35    val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
   14.36 -  val funpow: int -> ('a -> 'a) -> 'a -> 'a
   14.37  
   14.38    (*old options -- invalidated*)
   14.39    datatype invalid = None of invalid
   14.40 @@ -295,11 +296,10 @@
   14.41  
   14.42  (** functions **)
   14.43  
   14.44 -(*handy combinators*)
   14.45 +fun I x = x;
   14.46 +fun K x = fn _ => x;
   14.47  fun curry f x y = f (x, y);
   14.48  fun uncurry f (x, y) = f x y;
   14.49 -fun I x = x;
   14.50 -fun K x = fn _ => x;
   14.51  
   14.52  (*reverse application and structured results*)
   14.53  fun x |> f = f x;
   14.54 @@ -308,25 +308,28 @@
   14.55  fun (x, y) ||> f = (x, f y);
   14.56  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
   14.57  fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
   14.58 +
   14.59 +(*reverse composition*)
   14.60  fun f #> g = g o f;
   14.61 -fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
   14.62 -fun ` h = fn s => (h s, s)
   14.63 +fun f #-> g = uncurry g o f;
   14.64 +
   14.65 +(*view results*)
   14.66 +fun `f = fn x => (f x, x);
   14.67  
   14.68  (*composition with multiple args*)
   14.69  fun (f oo g) x y = f (g x y);
   14.70  fun (f ooo g) x y z = f (g x y z);
   14.71  fun (f oooo g) x y z w = f (g x y z w);
   14.72  
   14.73 -(*application of (infix) operator to its left or right argument*)
   14.74 -fun apl (x, f) y = f (x, y);
   14.75 -fun apr (f, y) x = f (x, y);
   14.76 -
   14.77  (*function exponentiation: f(...(f x)...) with n applications of f*)
   14.78  fun funpow n f x =
   14.79    let fun rep (0, x) = x
   14.80          | rep (n, x) = rep (n - 1, f x)
   14.81    in rep (n, x) end;
   14.82  
   14.83 +(*application of (infix) operator to its left or right argument*)
   14.84 +fun apl (x, f) y = f (x, y);
   14.85 +fun apr (f, y) x = f (x, y);
   14.86  
   14.87  
   14.88  (** options **)
   14.89 @@ -1268,12 +1271,13 @@
   14.90    Preserves order of elements in both lists.*)
   14.91  val partition = List.partition;
   14.92  
   14.93 -
   14.94  fun partition_eq (eq:'a * 'a -> bool) =
   14.95 -    let fun part [] = []
   14.96 -          | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys
   14.97 -                           in (x::xs)::(part xs') end
   14.98 -    in part end;
   14.99 +  let
  14.100 +    fun part [] = []
  14.101 +      | part (x :: ys) =
  14.102 +          let val (xs, xs') = partition (fn y => eq (x, y)) ys
  14.103 +          in (x::xs)::(part xs') end
  14.104 +  in part end;
  14.105  
  14.106  
  14.107  (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
    15.1 --- a/src/Pure/meta_simplifier.ML	Thu Jul 14 19:28:23 2005 +0200
    15.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jul 14 19:28:24 2005 +0200
    15.3 @@ -419,7 +419,7 @@
    15.4    andalso not(exists_subterm is_Var lhs)
    15.5      orelse
    15.6  *)
    15.7 -  exists (apl (lhs, Logic.occs)) (rhs :: prems)
    15.8 +  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
    15.9      orelse
   15.10    null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
   15.11      (*the condition "null prems" is necessary because conditional rewrites
    16.1 --- a/src/Pure/net.ML	Thu Jul 14 19:28:23 2005 +0200
    16.2 +++ b/src/Pure/net.ML	Thu Jul 14 19:28:24 2005 +0200
    16.3 @@ -222,10 +222,10 @@
    16.4        | subtr (Leaf _) (net as Net _) = subtr emptynet net
    16.5        | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
    16.6              (Net {comb = comb2, var = var2, atoms = atoms2}) =
    16.7 -          Symtab.fold (fn (a, net) =>
    16.8 -            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2 o
    16.9 -          subtr var1 var2 o
   16.10 -          subtr comb1 comb2;
   16.11 +          subtr comb1 comb2
   16.12 +          #> subtr var1 var2
   16.13 +          #> Symtab.fold (fn (a, net) =>
   16.14 +            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2
   16.15    in subtr net1 net2 [] end;
   16.16  
   16.17  fun entries net = subtract (K false) empty net;