eliminated NJ's List.nth;
authorwenzelm
Fri Feb 27 16:38:52 2009 +0100 (2009-02-27)
changeset 30146a77fc0209723
parent 30145 09817540ccae
child 30147 c1e1d96903ea
eliminated NJ's List.nth;
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/envir.ML
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/term.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Proof/proofchecker.ML	Fri Feb 27 16:33:11 2009 +0100
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Fri Feb 27 16:38:52 2009 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4        | thm_of _ _ (PAxm (name, _, SOME Ts)) =
     1.5            thm_of_atom (Thm.axiom thy name) Ts
     1.6  
     1.7 -      | thm_of _ Hs (PBound i) = List.nth (Hs, i)
     1.8 +      | thm_of _ Hs (PBound i) = nth Hs i
     1.9  
    1.10        | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
    1.11            let
     2.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Feb 27 16:33:11 2009 +0100
     2.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Feb 27 16:38:52 2009 +0100
     2.3 @@ -98,7 +98,7 @@
     2.4            let val (env3, V) = mk_tvar (env2, [])
     2.5            in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
     2.6        end
     2.7 -  | infer_type thy env Ts vTs (t as Bound i) = ((t, List.nth (Ts, i), vTs, env)
     2.8 +  | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
     2.9        handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
    2.10  
    2.11  fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
    2.12 @@ -152,7 +152,7 @@
    2.13      fun head_norm (prop, prf, cnstrts, env, vTs) =
    2.14        (Envir.head_norm env prop, prf, cnstrts, env, vTs);
    2.15  
    2.16 -    fun mk_cnstrts env _ Hs vTs (PBound i) = ((List.nth (Hs, i), PBound i, [], env, vTs)
    2.17 +    fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs)
    2.18            handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
    2.19        | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
    2.20            let
    2.21 @@ -304,7 +304,7 @@
    2.22  
    2.23  val head_norm = Envir.head_norm (Envir.empty 0);
    2.24  
    2.25 -fun prop_of0 Hs (PBound i) = List.nth (Hs, i)
    2.26 +fun prop_of0 Hs (PBound i) = nth Hs i
    2.27    | prop_of0 Hs (Abst (s, SOME T, prf)) =
    2.28        Term.all T $ (Abs (s, T, prop_of0 Hs prf))
    2.29    | prop_of0 Hs (AbsP (s, SOME t, prf)) =
     3.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 27 16:33:11 2009 +0100
     3.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 27 16:38:52 2009 +0100
     3.3 @@ -222,7 +222,7 @@
     3.4  (* implicit structures *)
     3.5  
     3.6  fun the_struct structs i =
     3.7 -  if 1 <= i andalso i <= length structs then List.nth (structs, i - 1)
     3.8 +  if 1 <= i andalso i <= length structs then nth structs (i - 1)
     3.9    else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
    3.10  
    3.11  fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
     4.1 --- a/src/Pure/envir.ML	Fri Feb 27 16:33:11 2009 +0100
     4.2 +++ b/src/Pure/envir.ML	Fri Feb 27 16:38:52 2009 +0100
     4.3 @@ -265,7 +265,7 @@
     4.4        | fast Ts (Const (_, T)) = T
     4.5        | fast Ts (Free (_, T)) = T
     4.6        | fast Ts (Bound i) =
     4.7 -        (List.nth (Ts, i)
     4.8 +        (nth Ts i
     4.9           handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
    4.10        | fast Ts (Var (_, T)) = T
    4.11        | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
     5.1 --- a/src/Pure/proofterm.ML	Fri Feb 27 16:33:11 2009 +0100
     5.2 +++ b/src/Pure/proofterm.ML	Fri Feb 27 16:38:52 2009 +0100
     5.3 @@ -470,8 +470,8 @@
     5.4      val n = length args;
     5.5      fun subst' lev (Bound i) =
     5.6           (if i<lev then raise SAME    (*var is locally bound*)
     5.7 -          else  incr_boundvars lev (List.nth (args, i-lev))
     5.8 -                  handle Subscript => Bound (i-n)  (*loose: change it*))
     5.9 +          else  incr_boundvars lev (nth args (i-lev))
    5.10 +                  handle Subscript => Bound (i-n))  (*loose: change it*)
    5.11        | subst' lev (Abs (a, T, body)) = Abs (a, T,  subst' (lev+1) body)
    5.12        | subst' lev (f $ t) = (subst' lev f $ substh' lev t
    5.13            handle SAME => f $ subst' lev t)
    5.14 @@ -494,7 +494,7 @@
    5.15      val n = length args;
    5.16      fun subst (PBound i) Plev tlev =
    5.17           (if i < Plev then raise SAME    (*var is locally bound*)
    5.18 -          else incr_pboundvars Plev tlev (List.nth (args, i-Plev))
    5.19 +          else incr_pboundvars Plev tlev (nth args (i-Plev))
    5.20                   handle Subscript => PBound (i-n)  (*loose: change it*))
    5.21        | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
    5.22        | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
    5.23 @@ -935,7 +935,7 @@
    5.24            in (is, ch orelse ch', ts',
    5.25                if ch orelse ch' then prf' % t' else prf) end
    5.26        | shrink' ls lev ts prfs (prf as PBound i) =
    5.27 -          (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
    5.28 +          (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
    5.29               orelse has_duplicates (op =)
    5.30                 (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
    5.31               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
     6.1 --- a/src/Pure/sign.ML	Fri Feb 27 16:33:11 2009 +0100
     6.2 +++ b/src/Pure/sign.ML	Fri Feb 27 16:38:52 2009 +0100
     6.3 @@ -338,7 +338,7 @@
     6.4      fun typ_of (_, Const (_, T)) = T
     6.5        | typ_of (_, Free  (_, T)) = T
     6.6        | typ_of (_, Var (_, T)) = T
     6.7 -      | typ_of (bs, Bound i) = snd (List.nth (bs, i) handle Subscript =>
     6.8 +      | typ_of (bs, Bound i) = snd (nth bs i handle Subscript =>
     6.9            raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
    6.10        | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
    6.11        | typ_of (bs, t $ u) =
     7.1 --- a/src/Pure/term.ML	Fri Feb 27 16:33:11 2009 +0100
     7.2 +++ b/src/Pure/term.ML	Fri Feb 27 16:38:52 2009 +0100
     7.3 @@ -297,7 +297,7 @@
     7.4    Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
     7.5  fun type_of1 (Ts, Const (_,T)) = T
     7.6    | type_of1 (Ts, Free  (_,T)) = T
     7.7 -  | type_of1 (Ts, Bound i) = (List.nth (Ts,i)
     7.8 +  | type_of1 (Ts, Bound i) = (nth Ts i
     7.9          handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
    7.10    | type_of1 (Ts, Var (_,T)) = T
    7.11    | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
    7.12 @@ -322,7 +322,7 @@
    7.13          | _ => raise TERM("fastype_of: expected function type", [f$u]))
    7.14    | fastype_of1 (_, Const (_,T)) = T
    7.15    | fastype_of1 (_, Free (_,T)) = T
    7.16 -  | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
    7.17 +  | fastype_of1 (Ts, Bound i) = (nth Ts i
    7.18           handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
    7.19    | fastype_of1 (_, Var (_,T)) = T
    7.20    | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
    7.21 @@ -638,7 +638,7 @@
    7.22      val n = length args;
    7.23      fun subst (t as Bound i, lev) =
    7.24           (if i < lev then raise SAME   (*var is locally bound*)
    7.25 -          else incr_boundvars lev (List.nth (args, i - lev))
    7.26 +          else incr_boundvars lev (nth args (i - lev))
    7.27              handle Subscript => Bound (i - n))  (*loose: change it*)
    7.28        | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    7.29        | subst (f $ t, lev) =
     8.1 --- a/src/Pure/type_infer.ML	Fri Feb 27 16:33:11 2009 +0100
     8.2 +++ b/src/Pure/type_infer.ML	Fri Feb 27 16:38:52 2009 +0100
     8.3 @@ -369,7 +369,7 @@
     8.4      fun inf _ (PConst (_, T)) = T
     8.5        | inf _ (PFree (_, T)) = T
     8.6        | inf _ (PVar (_, T)) = T
     8.7 -      | inf bs (PBound i) = snd (List.nth (bs, i) handle Subscript => err_loose i)
     8.8 +      | inf bs (PBound i) = snd (nth bs i handle Subscript => err_loose i)
     8.9        | inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t])
    8.10        | inf bs (PAppl (t, u)) =
    8.11            let