src/Pure/pattern.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/pattern.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/pattern.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  fun string_of_term sg env binders t = Sign.string_of_term sg
     1.5    (Envir.norm_term env (subst_bounds(map Free binders,t)));
     1.6  
     1.7 -fun bname binders i = fst(nth_elem(i,binders));
     1.8 +fun bname binders i = fst(List.nth(binders,i));
     1.9  fun bnames binders is = space_implode " " (map (bname binders) is);
    1.10  
    1.11  fun typ_clash sg (tye,T,U) =
    1.12 @@ -113,10 +113,10 @@
    1.13  fun idx [] j     = raise Unif
    1.14    | idx(i::is) j = if i=j then length is else idx is j;
    1.15  
    1.16 -fun at xs i = nth_elem (i,xs);
    1.17 +fun at xs i = List.nth (xs,i);
    1.18  
    1.19  fun mkabs (binders,is,t)  =
    1.20 -    let fun mk(i::is) = let val (x,T) = nth_elem(i,binders)
    1.21 +    let fun mk(i::is) = let val (x,T) = List.nth(binders,i)
    1.22                          in Abs(x,T,mk is) end
    1.23            | mk []     = t
    1.24      in mk is end;
    1.25 @@ -158,7 +158,7 @@
    1.26  
    1.27  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
    1.28  fun mk_proj_list is =
    1.29 -    let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
    1.30 +    let fun mk(i::is,j) = if isSome i then j :: mk(is,j-1) else mk(is,j-1)
    1.31            | mk([],_)    = []
    1.32      in mk(is,length is - 1) end;
    1.33  
    1.34 @@ -182,7 +182,7 @@
    1.35                        let val js = ints_of' env ts;
    1.36                            val js' = map (try (trans d)) js;
    1.37                            val ks = mk_proj_list js';
    1.38 -                          val ls = mapfilter I js'
    1.39 +                          val ls = List.mapPartial I js'
    1.40                            val Hty = type_of_G env (Fty,length js,ks)
    1.41                            val (env',H) = Envir.genvar a (env,Hty)
    1.42                            val env'' =
    1.43 @@ -260,11 +260,11 @@
    1.44  
    1.45  and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) =
    1.46        if a<>b then (clash a b; raise Unif)
    1.47 -      else foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts)
    1.48 +      else Library.foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts)
    1.49  
    1.50  and rigidrigidB sg (env,binders,i,j,ss,ts) =
    1.51       if i <> j then (clashBB binders i j; raise Unif)
    1.52 -     else foldl (unif sg binders) (env ,ss~~ts)
    1.53 +     else Library.foldl (unif sg binders) (env ,ss~~ts)
    1.54  
    1.55  and flexrigid sg (params as (env,binders,F,is,t)) =
    1.56        if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
    1.57 @@ -272,7 +272,7 @@
    1.58              in Envir.update((F,mkabs(binders,is,u)),env') end
    1.59              handle Unif => (proj_fail sg params; raise Unif));
    1.60  
    1.61 -fun unify(sg,env,tus) = foldl (unif sg []) (env,tus);
    1.62 +fun unify(sg,env,tus) = Library.foldl (unif sg []) (env,tus);
    1.63  
    1.64  
    1.65  (*Eta-contract a term (fully)*)
    1.66 @@ -407,7 +407,7 @@
    1.67    and cases(binders,env as (iTs,itms),pat,obj) =
    1.68      let val (ph,pargs) = strip_comb pat
    1.69          fun rigrig1(iTs,oargs) =
    1.70 -              foldl (mtch binders) ((iTs,itms), pargs~~oargs)
    1.71 +              Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
    1.72          fun rigrig2((a,Ta),(b,Tb),oargs) =
    1.73                if a<> b then raise MATCH
    1.74                else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
    1.75 @@ -476,7 +476,7 @@
    1.76      val skel0 = Bound 0;
    1.77  
    1.78      val rhs_names =
    1.79 -      foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
    1.80 +      Library.foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
    1.81  
    1.82      fun variant_absfree (x, T, t) =
    1.83        let
    1.84 @@ -485,29 +485,29 @@
    1.85        in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
    1.86  
    1.87      fun match_rew tm (tm1, tm2) =
    1.88 -      let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2
    1.89 +      let val rtm = getOpt (Term.rename_abs tm1 tm tm2, tm2)
    1.90        in SOME (subst_vars (match tsig (tm1, tm)) rtm, rtm)
    1.91          handle MATCH => NONE
    1.92        end;
    1.93  
    1.94      fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
    1.95        | rew tm = (case get_first (match_rew tm) rules of
    1.96 -          NONE => apsome (rpair skel0) (get_first (fn p => p tm) procs)
    1.97 +          NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
    1.98          | x => x);
    1.99  
   1.100      fun rew1 (Var _) _ = NONE
   1.101        | rew1 skel tm = (case rew2 skel tm of
   1.102            SOME tm1 => (case rew tm1 of
   1.103 -              SOME (tm2, skel') => SOME (if_none (rew1 skel' tm2) tm2)
   1.104 +              SOME (tm2, skel') => SOME (getOpt (rew1 skel' tm2, tm2))
   1.105              | NONE => SOME tm1)
   1.106          | NONE => (case rew tm of
   1.107 -              SOME (tm1, skel') => SOME (if_none (rew1 skel' tm1) tm1)
   1.108 +              SOME (tm1, skel') => SOME (getOpt (rew1 skel' tm1, tm1))
   1.109              | NONE => NONE))
   1.110  
   1.111      and rew2 skel (tm1 $ tm2) = (case tm1 of
   1.112              Abs (_, _, body) =>
   1.113                let val tm' = subst_bound (tm2, body)
   1.114 -              in SOME (if_none (rew2 skel0 tm') tm') end
   1.115 +              in SOME (getOpt (rew2 skel0 tm', tm')) end
   1.116            | _ =>
   1.117              let val (skel1, skel2) = (case skel of
   1.118                  skel1 $ skel2 => (skel1, skel2)
   1.119 @@ -530,7 +530,7 @@
   1.120            end
   1.121        | rew2 _ _ = NONE
   1.122  
   1.123 -  in if_none (rew1 skel0 tm) tm end;
   1.124 +  in getOpt (rew1 skel0 tm, tm) end;
   1.125  
   1.126  end;
   1.127