# HG changeset patch # User wenzelm # Date 1369821211 -7200 # Node ID c4264f71dc3bbca92aa4381e5b25ca896269cee2 # Parent c8ee9c0a3a648eee62f7f25b541a8cdf38cd1c96 backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types; diff -r c8ee9c0a3a64 -r c4264f71dc3b src/Pure/pattern.ML --- a/src/Pure/pattern.ML Wed May 29 11:06:38 2013 +0200 +++ b/src/Pure/pattern.ML Wed May 29 11:53:31 2013 +0200 @@ -242,15 +242,8 @@ and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of ((Var(F,Fty),ss),(Var(G,Gty),ts)) => - if F = G then - let val env' = unify_types thy (Fty, Gty) env - in flexflex1(env',binders,F,Fty,ints_of' env' ss,ints_of' env' ts) end - else - let val env' = - unify_types thy - (Envir.body_type env (length ss) Fty, - Envir.body_type env (length ts) Gty) env - in flexflex2(env',binders,F,Fty,ints_of' env' ss,G,Gty,ints_of' env' ts) end + if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) + else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) | ((Var(F,Fty),ss),_) => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t) | (_,(Var(F,Fty),ts)) => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s) | ((Const c,ss),(Const d,ts)) => rigidrigid thy (env,binders,c,d,ss,ts) diff -r c8ee9c0a3a64 -r c4264f71dc3b src/Pure/unify.ML --- a/src/Pure/unify.ML Wed May 29 11:06:38 2013 +0200 +++ b/src/Pure/unify.ML Wed May 29 11:53:31 2013 +0200 @@ -186,9 +186,6 @@ fun unify_types thy TU env = Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY; -fun unify_types_of thy (rbinder, t, u) env = - unify_types thy (fastype env (rbinder, t), fastype env (rbinder, u)) env; - fun test_unify_types thy (T, U) env = let val str_of = Syntax.string_of_typ_global thy; @@ -199,44 +196,49 @@ (*Is the term eta-convertible to a single variable with the given rbinder? Examples: ?a ?f(B.0) ?g(B.1,B.0) Result is var a for use in SIMPL. *) -fun get_eta_var [] n (Var vT) = (n, vT) - | get_eta_var (_ :: rbinder) n (f $ Bound i) = - if n = i then get_eta_var rbinder (n + 1) f +fun get_eta_var ([], _, Var vT) = vT + | get_eta_var (_::rbinder, n, f $ Bound i) = + if n = i then get_eta_var (rbinder, n + 1, f) else raise ASSIGN - | get_eta_var _ _ _ = raise ASSIGN; + | get_eta_var _ = raise ASSIGN; (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u. If v occurs rigidly then nonunifiable. If v occurs nonrigidly then must use full algorithm. *) fun assignment thy (rbinder, t, u) env = - let val (n, (v, T)) = get_eta_var rbinder 0 t in + let val vT as (v,T) = get_eta_var (rbinder, 0, t) in (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of NoOcc => - let val env = unify_types thy (Envir.body_type env n T, fastype env (rbinder, u)) env - in Envir.update ((v, T), Logic.rlist_abs (rbinder, u)) env end + let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env + in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end | Nonrigid => raise ASSIGN | Rigid => raise CANTUNIFY) end; (*Extends an rbinder with a new disagreement pair, if both are abstractions. + Tries to unify types of the bound variables! Checks that binders have same length, since terms should be eta-normal; if not, raises TERM, probably indicating type mismatch. Uses variable a (unless the null string) to preserve user's naming.*) fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env = - let val c = if a = "" then b else a - in new_dpair thy ((c, T) :: rbinder, body1, body2) env end + let + val env' = unify_types thy (T, U) env; + val c = if a = "" then b else a; + in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end | new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", []) | new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", []) | new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env); + fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env = new_dpair thy (rbinder, eta_norm env (rbinder, Envir.head_norm env t), eta_norm env (rbinder, Envir.head_norm env u)) env; + (*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs Does not perform assignments for flex-flex pairs: may create nonrigid paths, which prevent other assignments. @@ -245,8 +247,7 @@ *) fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list = let - val (dp as (rbinder, t, u), env) = - head_norm_dpair thy (unify_types_of thy dp0 env, dp0); + val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0); fun SIMRANDS (f $ t, g $ u, env) = SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env)) | SIMRANDS (t as _$_, _, _) = @@ -256,9 +257,11 @@ | SIMRANDS (_, _, env) = (env, flexflex, flexrigid); in (case (head_of t, head_of u) of - (Var (v, T), Var (w, U)) => - let val env' = if v = w then unify_types thy (T, U) env else env - in (env', dp :: flexflex, flexrigid) end + (Var (_, T), Var (_, U)) => + let + val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U; + val env = unify_types thy (T', U') env; + in (env, dp :: flexflex, flexrigid) end | (Var _, _) => ((assignment thy (rbinder,t,u) env, flexflex, flexrigid) handle ASSIGN => (env, flexflex, dp :: flexrigid)) @@ -412,11 +415,11 @@ (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) Attempts to update t with u, raising ASSIGN if impossible*) fun ff_assign thy (env, rbinder, t, u) : Envir.env = - let val (n, (v, T)) = get_eta_var rbinder 0 t in + let val vT as (v, T) = get_eta_var (rbinder, 0, t) in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN else - let val env = unify_types thy (Envir.body_type env n T, fastype env (rbinder, u)) env - in Envir.vupdate ((v, T), Logic.rlist_abs (rbinder, u)) env end + let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env + in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end end;