changed libraray function find to find_index_eq, currying it
authoroheimb
Fri Nov 07 18:02:15 1997 +0100 (1997-11-07 ago)
changeset 41881025a27b08f9
parent 4187 2fafec5868fe
child 4189 b8c7a6bc6c16
changed libraray function find to find_index_eq, currying it
src/FOL/simpdata.ML
src/HOL/datatype.ML
src/HOL/simpdata.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/library.ML
src/Pure/library.ML
src/Pure/term.ML
     1.1 --- a/src/FOL/simpdata.ML	Fri Nov 07 17:51:26 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
     1.3 @@ -247,16 +247,11 @@
     1.4    fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
     1.5      | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
     1.6      | is_eq _ = false;
     1.7 -  fun find_eq n [] = None
     1.8 -    | find_eq n (t :: ts) = if (is_eq t) then Some n 
     1.9 -			    else find_eq (n + 1) ts;
    1.10 +  val find_eq = find_index is_eq;
    1.11  in
    1.12  val rot_eq_tac = 
    1.13 -     SUBGOAL (fn (Bi,i) => 
    1.14 -	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
    1.15 -		  None   => no_tac
    1.16 -		| Some 0 => no_tac
    1.17 -		| Some n => rotate_tac n i)
    1.18 +     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
    1.19 +		if n>0 then rotate_tac n i else no_tac end)
    1.20  end;
    1.21  
    1.22  
     2.1 --- a/src/HOL/datatype.ML	Fri Nov 07 17:51:26 1997 +0100
     2.2 +++ b/src/HOL/datatype.ML	Fri Nov 07 18:02:15 1997 +0100
     2.3 @@ -194,7 +194,7 @@
     2.4          | trans_recs' cis (eq::eqs) = 
     2.5            let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
     2.6              val tc = assoc(tcs,c);
     2.7 -            val i = (1 + find (c,cs))  handle LIST "find" => 0; 
     2.8 +            val i = 1 + find_index_eq c cs;
     2.9            in
    2.10            if name <> name1 then 
    2.11              raise RecError "function names inconsistent"
     3.1 --- a/src/HOL/simpdata.ML	Fri Nov 07 17:51:26 1997 +0100
     3.2 +++ b/src/HOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
     3.3 @@ -456,16 +456,11 @@
     3.4  local
     3.5    fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
     3.6      | is_eq _ = false;
     3.7 -  fun find_eq n [] = None
     3.8 -    | find_eq n (t :: ts) = if (is_eq t) then Some n 
     3.9 -			    else find_eq (n + 1) ts;
    3.10 +  val find_eq = find_index is_eq;
    3.11  in
    3.12  val rot_eq_tac = 
    3.13 -     SUBGOAL (fn (Bi,i) => 
    3.14 -	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
    3.15 -		  None   => no_tac
    3.16 -		| Some 0 => no_tac
    3.17 -		| Some n => rotate_tac n i)
    3.18 +     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
    3.19 +		if n>0 then rotate_tac n i else no_tac end)
    3.20  end;
    3.21  
    3.22  (*an unsatisfactory fix for the incomplete asm_full_simp_tac!
     4.1 --- a/src/HOLCF/domain/extender.ML	Fri Nov 07 17:51:26 1997 +0100
     4.2 +++ b/src/HOLCF/domain/extender.ML	Fri Nov 07 18:02:15 1997 +0100
     4.3 @@ -84,14 +84,14 @@
     4.4      val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
     4.5      val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
     4.6      val dts  = map (Type o fst) eqs';
     4.7 -    fun strip ss = drop (find ("'", ss)+1, ss);
     4.8 +    fun strip ss = drop (find_index_eq "'" ss +1, ss);
     4.9      fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
    4.10        | typid (TFree (id,_)   ) = hd (strip (tl (explode (Sign.base_name id))))
    4.11        | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
    4.12      fun cons cons' = (map (fn (con,syn,args) =>
    4.13  	((Syntax.const_name con syn),
    4.14  	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
    4.15 -					find (tp,dts) handle LIST "find" => ~1),
    4.16 +					find_index_eq tp dts),
    4.17  					sel,vn))
    4.18  	     (args,(mk_var_names(map (typid o third) args)))
    4.19  	 )) cons') : cons list;
     5.1 --- a/src/HOLCF/domain/library.ML	Fri Nov 07 17:51:26 1997 +0100
     5.2 +++ b/src/HOLCF/domain/library.ML	Fri Nov 07 18:02:15 1997 +0100
     5.3 @@ -168,7 +168,7 @@
     5.4  fun defined t = t ~= UU;
     5.5  fun cpair (S,T) = %%"cpair"`S`T;
     5.6  fun lift_defined f = lift (fn x => defined (f x));
     5.7 -fun bound_arg vns v = Bound(length vns-find(v,vns)-1);
     5.8 +fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
     5.9  
    5.10  fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = 
    5.11        (case cont_eta_contract body  of
     6.1 --- a/src/Pure/library.ML	Fri Nov 07 17:51:26 1997 +0100
     6.2 +++ b/src/Pure/library.ML	Fri Nov 07 18:02:15 1997 +0100
     6.3 @@ -245,10 +245,11 @@
     6.4  
     6.5  
     6.6  (*find the position of an element in a list*)
     6.7 -fun find (x, ys) =
     6.8 -  let fun f (y :: ys, i) = if x = y then i else f (ys, i + 1)
     6.9 -        | f (_, _) = raise LIST "find"
    6.10 -  in f (ys, 0) end;
    6.11 +fun find_index (pred: 'a->bool) : 'a list -> int =
    6.12 +  let fun find _ []      = ~1
    6.13 +        | find n (x::xs) = if pred x then n else find (n+1) xs
    6.14 +  in find 0 end;
    6.15 +fun find_index_eq x = find_index (fn y => y = x);
    6.16  
    6.17  (*flatten a list of lists to a list*)
    6.18  fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
    6.19 @@ -294,10 +295,10 @@
    6.20        | Some y => y :: mapfilter f xs);
    6.21  
    6.22  
    6.23 -fun find_first _ [] = None
    6.24 -  | find_first pred (x :: xs) =
    6.25 -      if pred x then Some x else find_first pred xs;
    6.26 -
    6.27 +fun find_first pred = let
    6.28 +  fun f [] = None
    6.29 +  |   f (x :: xs) = if pred x then Some x else f  xs
    6.30 +  in f end;
    6.31  
    6.32  (* lists of pairs *)
    6.33  
     7.1 --- a/src/Pure/term.ML	Fri Nov 07 17:51:26 1997 +0100
     7.2 +++ b/src/Pure/term.ML	Fri Nov 07 18:02:15 1997 +0100
     7.3 @@ -715,6 +715,7 @@
     7.4  
     7.5  val memo_types = ref (Symtab.null : typ list Symtab.table);
     7.6  
     7.7 +(* special case of library/find_first *)
     7.8  fun find_type (T, []: typ list) = None
     7.9    | find_type (T, T'::Ts) =
    7.10         if T=T' then Some T'
    7.11 @@ -744,6 +745,7 @@
    7.12  
    7.13  val memo_terms = ref (Symtab.null : term list Symtab.table);
    7.14  
    7.15 +(* special case of library/find_first *)
    7.16  fun find_term (t, []: term list) = None
    7.17    | find_term (t, t'::ts) =
    7.18         if t=t' then Some t'