Sign.typ_unify;
authorwenzelm
Thu Jul 28 15:19:56 2005 +0200 (2005-07-28)
changeset 1693987fc64d2409f
parent 16938 04bdd18e0ad1
child 16940 d14ec6f2d29b
Sign.typ_unify;
Term.bound;
tuned rewrite_term;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Thu Jul 28 15:19:55 2005 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Jul 28 15:19:56 2005 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4  
     1.5  fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     1.6    if T=U then env
     1.7 -  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (U, T)
     1.8 +  else let val (iTs',maxidx') = Sign.typ_unify sg (U, T) (iTs, maxidx)
     1.9         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.10         handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif);
    1.11  
    1.12 @@ -343,8 +343,8 @@
    1.13  
    1.14  exception MATCH;
    1.15  
    1.16 -fun typ_match tsig args = (Type.typ_match tsig args)
    1.17 -                          handle Type.TYPE_MATCH => raise MATCH;
    1.18 +fun typ_match tsig (tyenv, TU) = Type.typ_match tsig TU tyenv
    1.19 +  handle Type.TYPE_MATCH => raise MATCH;
    1.20  
    1.21  (*First-order matching;
    1.22    fomatch tsig (pattern, object) returns a (tyvar,typ)list and (var,term)list.
    1.23 @@ -475,19 +475,16 @@
    1.24    let
    1.25      val skel0 = Bound 0;
    1.26  
    1.27 -    val rhs_names =
    1.28 -      foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) [] rules;
    1.29 -
    1.30 -    fun variant_absfree (x, T, t) =
    1.31 +    fun variant_absfree bounds (x, T, t) =
    1.32        let
    1.33 -        val x' = variant (add_term_free_names (t, rhs_names)) x;
    1.34 -        val t' = subst_bound (Free (x', T), t);
    1.35 -      in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
    1.36 +        val (x', t') = Term.dest_abs (Term.bound bounds x, T, t);
    1.37 +        fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
    1.38 +      in (abs, t') end;
    1.39  
    1.40      fun match_rew tm (tm1, tm2) =
    1.41 -      let val rtm = getOpt (Term.rename_abs tm1 tm tm2, tm2)
    1.42 -      in SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm)
    1.43 -        handle MATCH => NONE
    1.44 +      let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 in
    1.45 +        SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm)
    1.46 +          handle MATCH => NONE
    1.47        end;
    1.48  
    1.49      fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
    1.50 @@ -495,42 +492,42 @@
    1.51            NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
    1.52          | x => x);
    1.53  
    1.54 -    fun rew1 (Var _) _ = NONE
    1.55 -      | rew1 skel tm = (case rew2 skel tm of
    1.56 +    fun rew1 bounds (Var _) _ = NONE
    1.57 +      | rew1 bounds skel tm = (case rew2 bounds skel tm of
    1.58            SOME tm1 => (case rew tm1 of
    1.59 -              SOME (tm2, skel') => SOME (getOpt (rew1 skel' tm2, tm2))
    1.60 +              SOME (tm2, skel') => SOME (if_none (rew1 bounds skel' tm2) tm2)
    1.61              | NONE => SOME tm1)
    1.62          | NONE => (case rew tm of
    1.63 -              SOME (tm1, skel') => SOME (getOpt (rew1 skel' tm1, tm1))
    1.64 +              SOME (tm1, skel') => SOME (if_none (rew1 bounds skel' tm1) tm1)
    1.65              | NONE => NONE))
    1.66  
    1.67 -    and rew2 skel (tm1 $ tm2) = (case tm1 of
    1.68 +    and rew2 bounds skel (tm1 $ tm2) = (case tm1 of
    1.69              Abs (_, _, body) =>
    1.70                let val tm' = subst_bound (tm2, body)
    1.71 -              in SOME (getOpt (rew2 skel0 tm', tm')) end
    1.72 +              in SOME (if_none (rew2 bounds skel0 tm') tm') end
    1.73            | _ =>
    1.74              let val (skel1, skel2) = (case skel of
    1.75                  skel1 $ skel2 => (skel1, skel2)
    1.76                | _ => (skel0, skel0))
    1.77 -            in case rew1 skel1 tm1 of
    1.78 -                SOME tm1' => (case rew1 skel2 tm2 of
    1.79 +            in case rew1 bounds skel1 tm1 of
    1.80 +                SOME tm1' => (case rew1 bounds skel2 tm2 of
    1.81                      SOME tm2' => SOME (tm1' $ tm2')
    1.82                    | NONE => SOME (tm1' $ tm2))
    1.83 -              | NONE => (case rew1 skel2 tm2 of
    1.84 +              | NONE => (case rew1 bounds skel2 tm2 of
    1.85                      SOME tm2' => SOME (tm1 $ tm2')
    1.86                    | NONE => NONE)
    1.87              end)
    1.88 -      | rew2 skel (Abs (x, T, tm)) =
    1.89 +      | rew2 bounds skel (Abs body) =
    1.90            let
    1.91 -            val (abs, tm') = variant_absfree (x, T, tm);
    1.92 +            val (abs, tm') = variant_absfree bounds body;
    1.93              val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
    1.94 -          in case rew1 skel' tm' of
    1.95 +          in case rew1 (bounds + 1) skel' tm' of
    1.96                SOME tm'' => SOME (abs tm'')
    1.97              | NONE => NONE
    1.98            end
    1.99 -      | rew2 _ _ = NONE
   1.100 +      | rew2 _ _ _ = NONE;
   1.101  
   1.102 -  in getOpt (rew1 skel0 tm, tm) end;
   1.103 +  in if_none (rew1 0 skel0 tm) tm end;
   1.104  
   1.105  end;
   1.106