author  wenzelm 
Wed, 16 Nov 2005 17:45:30 +0100  
changeset 18184  43c4589a9a78 
parent 17344  8b2f56aff711 
child 18945  0b15863018a8 
permissions  rwrr 
15797  1 
(* Title: Pure/unify.ML 
0  2 
ID: $Id$ 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
5 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

6 
HigherOrder Unification. 
0  7 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

8 
Types as well as terms are unified. The outermost functions assume 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

9 
the terms to be unified already have the same type. In resolution, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

10 
this is assured because both have type "prop". 
0  11 
*) 
12 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

13 
signature UNIFY = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

14 
sig 
0  15 
(*references for control and tracing*) 
16 
val trace_bound: int ref 

17 
val trace_simp: bool ref 

18 
val trace_types: bool ref 

19 
val search_bound: int ref 

20 
(*other exports*) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

21 
val combound: term * int * int > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

22 
val rlist_abs: (string * typ) list * term > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

23 
val smash_unifiers: theory * Envir.env * (term * term) list > Envir.env Seq.seq 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

24 
val unifiers: theory * Envir.env * ((term * term) list) > 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

25 
(Envir.env * (term * term) list) Seq.seq 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

26 
end 
0  27 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

28 
structure Unify : UNIFY = 
0  29 
struct 
30 

31 
(*Unification options*) 

32 

15275  33 
val trace_bound = ref 25 (*tracing starts above this depth, 0 for full*) 
34 
and search_bound = ref 30 (*unification quits above this depth*) 

1460  35 
and trace_simp = ref false (*print dpairs before calling SIMPL*) 
36 
and trace_types = ref false (*announce potential incompleteness 

37 
of type unification*) 

0  38 

39 
type binderlist = (string*typ) list; 

40 

41 
type dpair = binderlist * term * term; 

42 

43 
fun body_type(Envir.Envir{iTs,...}) = 

44 
let fun bT(Type("fun",[_,T])) = bT T 

15797  45 
 bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of 
15531  46 
NONE => T  SOME(T') => bT T') 
0  47 
 bT T = T 
48 
in bT end; 

49 

50 
fun binder_types(Envir.Envir{iTs,...}) = 

51 
let fun bTs(Type("fun",[T,U])) = T :: bTs U 

15797  52 
 bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of 
15531  53 
NONE => []  SOME(T') => bTs T') 
0  54 
 bTs _ = [] 
55 
in bTs end; 

56 

57 
fun strip_type env T = (binder_types env T, body_type env T); 

58 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

59 
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; 
0  60 

61 

62 
(*Eta normal form*) 

63 
fun eta_norm(env as Envir.Envir{iTs,...}) = 

64 
let fun etif (Type("fun",[T,U]), t) = 

1460  65 
Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) 
15797  66 
 etif (TVar ixnS, t) = 
67 
(case Type.lookup (iTs, ixnS) of 

15531  68 
NONE => t  SOME(T) => etif(T,t)) 
1460  69 
 etif (_,t) = t; 
0  70 
fun eta_nm (rbinder, Abs(a,T,body)) = 
1460  71 
Abs(a, T, eta_nm ((a,T)::rbinder, body)) 
72 
 eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) 

0  73 
in eta_nm end; 
74 

75 

76 
(*OCCURS CHECK 

77 
Does the uvar occur in the term t? 

78 
two forms of search, for whether there is a rigid path to the current term. 

79 
"seen" is list of variables passed thru, is a memo variable for sharing. 

15797  80 
This version searches for nonrigid occurrence, returns true if found. 
81 
Since terms may contain variables with same name and different types, 

82 
the occurs check must ignore the types of variables. This avoids 

83 
that ?x::?'a is unified with f(?x::T), which may lead to a cyclic 

84 
substitution when ?'a is instantiated with T later. *) 

0  85 
fun occurs_terms (seen: (indexname list) ref, 
1460  86 
env: Envir.env, v: indexname, ts: term list): bool = 
0  87 
let fun occurs [] = false 
1460  88 
 occurs (t::ts) = occur t orelse occurs ts 
0  89 
and occur (Const _) = false 
1460  90 
 occur (Bound _) = false 
91 
 occur (Free _) = false 

15797  92 
 occur (Var (w, T)) = 
2178  93 
if mem_ix (w, !seen) then false 
2753  94 
else if eq_ix(v,w) then true 
1460  95 
(*no need to lookup: v has no assignment*) 
96 
else (seen := w:: !seen; 

15797  97 
case Envir.lookup (env, (w, T)) of 
15531  98 
NONE => false 
99 
 SOME t => occur t) 

1460  100 
 occur (Abs(_,_,body)) = occur body 
101 
 occur (f$t) = occur t orelse occur f 

0  102 
in occurs ts end; 
103 

104 

105 

106 
(* f(a1,...,an) > (f, [a1,...,an]) using the assignments*) 

107 
fun head_of_in (env,t) : term = case t of 

108 
f$_ => head_of_in(env,f) 

15797  109 
 Var vT => (case Envir.lookup (env, vT) of 
15531  110 
SOME u => head_of_in(env,u)  NONE => t) 
0  111 
 _ => t; 
112 

113 

114 
datatype occ = NoOcc  Nonrigid  Rigid; 

115 

116 
(* Rigid occur check 

117 
Returns Rigid if it finds a rigid occurrence of the variable, 

118 
Nonrigid if it finds a nonrigid path to the variable. 

119 
NoOcc otherwise. 

120 
Continues searching for a rigid occurrence even if it finds a nonrigid one. 

121 

122 
Condition for detecting nonunifable terms: [ section 5.3 of Huet (1975) ] 

123 
a rigid path to the variable, appearing with no arguments. 

124 
Here completeness is sacrificed in order to reduce danger of divergence: 

125 
reject ALL rigid paths to the variable. 

126 
Could check for rigid paths to bound variables that are out of scope. 

127 
Not necessary because the assignment test looks at variable's ENTIRE rbinder. 

128 

129 
Treatment of head(arg1,...,argn): 

130 
If head is a variable then no rigid path, switch to nonrigid search 

131 
for arg1,...,argn. 

132 
If head is an abstraction then possibly no rigid path (head could be a 

133 
constant function) so again use nonrigid search. Happens only if 

134 
term is not in normal form. 

135 

136 
Warning: finds a rigid occurrence of ?f in ?f(t). 

137 
Should NOT be called in this case: there is a flexflex unifier 

138 
*) 

139 
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 

140 
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 

1460  141 
else NoOcc 
0  142 
fun occurs [] = NoOcc 
1460  143 
 occurs (t::ts) = 
0  144 
(case occur t of 
145 
Rigid => Rigid 

146 
 oc => (case occurs ts of NoOcc => oc  oc2 => oc2)) 

147 
and occomb (f$t) = 

148 
(case occur t of 

149 
Rigid => Rigid 

150 
 oc => (case occomb f of NoOcc => oc  oc2 => oc2)) 

151 
 occomb t = occur t 

152 
and occur (Const _) = NoOcc 

1460  153 
 occur (Bound _) = NoOcc 
154 
 occur (Free _) = NoOcc 

15797  155 
 occur (Var (w, T)) = 
2178  156 
if mem_ix (w, !seen) then NoOcc 
2753  157 
else if eq_ix(v,w) then Rigid 
1460  158 
else (seen := w:: !seen; 
15797  159 
case Envir.lookup (env, (w, T)) of 
15531  160 
NONE => NoOcc 
161 
 SOME t => occur t) 

1460  162 
 occur (Abs(_,_,body)) = occur body 
163 
 occur (t as f$_) = (*switch to nonrigid search?*) 

164 
(case head_of_in (env,f) of 

165 
Var (w,_) => (*w is not assigned*) 

2753  166 
if eq_ix(v,w) then Rigid 
1460  167 
else nonrigid t 
168 
 Abs(_,_,body) => nonrigid t (*not in normal form*) 

169 
 _ => occomb t) 

0  170 
in occur t end; 
171 

172 

1460  173 
exception CANTUNIFY; (*Signals nonunifiability. Does not signal errors!*) 
174 
exception ASSIGN; (*Raised if not an assignment*) 

0  175 

176 

16664  177 
fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) = 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

178 
if T=U then env 
16934  179 
else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

180 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
1505  181 
handle Type.TUNIFY => raise CANTUNIFY; 
0  182 

16664  183 
fun test_unify_types thy (args as (T,U,_)) = 
184 
let val str_of = Sign.string_of_typ thy; 

185 
fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T); 

186 
val env' = unify_types thy args 

0  187 
in if is_TVar(T) orelse is_TVar(U) then warn() else (); 
188 
env' 

189 
end; 

190 

191 
(*Is the term etaconvertible to a single variable with the given rbinder? 

192 
Examples: ?a ?f(B.0) ?g(B.1,B.0) 

193 
Result is var a for use in SIMPL. *) 

194 
fun get_eta_var ([], _, Var vT) = vT 

195 
 get_eta_var (_::rbinder, n, f $ Bound i) = 

1460  196 
if n=i then get_eta_var (rbinder, n+1, f) 
197 
else raise ASSIGN 

0  198 
 get_eta_var _ = raise ASSIGN; 
199 

200 

201 
(* ([xn,...,x1], t) ======> (x1,...,xn)t *) 

202 
fun rlist_abs ([], body) = body 

203 
 rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); 

204 

205 

206 
(*Solve v=u by assignment  "fixedpoint" to Huet  if v not in u. 

207 
If v occurs rigidly then nonunifiable. 

208 
If v occurs nonrigidly then must use full algorithm. *) 

16664  209 
fun assignment thy (env, rbinder, t, u) = 
15797  210 
let val vT as (v,T) = get_eta_var (rbinder, 0, t) 
211 
in case rigid_occurs_term (ref [], env, v, u) of 

16664  212 
NoOcc => let val env = unify_types thy (body_type env T, 
1460  213 
fastype env (rbinder,u),env) 
15797  214 
in Envir.update ((vT, rlist_abs (rbinder, u)), env) end 
1460  215 
 Nonrigid => raise ASSIGN 
216 
 Rigid => raise CANTUNIFY 

0  217 
end; 
218 

219 

220 
(*Extends an rbinder with a new disagreement pair, if both are abstractions. 

221 
Tries to unify types of the bound variables! 

222 
Checks that binders have same length, since terms should be etanormal; 

223 
if not, raises TERM, probably indicating type mismatch. 

224 
Uses variable a (unless the null string) to preserve user's naming.*) 

16664  225 
fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = 
226 
let val env' = unify_types thy (T,U,env) 

1460  227 
val c = if a="" then b else a 
16664  228 
in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end 
229 
 new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", []) 

230 
 new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", []) 

231 
 new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); 

0  232 

233 

16664  234 
fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env = 
235 
new_dpair thy (rbinder, 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

236 
eta_norm env (rbinder, Envir.head_norm env t), 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

237 
eta_norm env (rbinder, Envir.head_norm env u), env); 
0  238 

239 

240 

241 
(*flexflex: the flexflex pairs, flexrigid: the flexrigid pairs 

242 
Does not perform assignments for flexflex pairs: 

646  243 
may create nonrigid paths, which prevent other assignments. 
244 
Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to 

245 
do so caused numerous problems with no compensating advantage. 

246 
*) 

16664  247 
fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) 
1460  248 
: Envir.env * dpair list * dpair list = 
16664  249 
let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0); 
1460  250 
fun SIMRANDS(f$t, g$u, env) = 
16664  251 
SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env)) 
1460  252 
 SIMRANDS (t as _$_, _, _) = 
253 
raise TERM ("SIMPL: operands mismatch", [t,u]) 

254 
 SIMRANDS (t, u as _$_, _) = 

255 
raise TERM ("SIMPL: operands mismatch", [t,u]) 

256 
 SIMRANDS(_,_,env) = (env,flexflex,flexrigid); 

0  257 
in case (head_of t, head_of u) of 
258 
(Var(_,T), Var(_,U)) => 

1460  259 
let val T' = body_type env T and U' = body_type env U; 
16664  260 
val env = unify_types thy (T',U',env) 
1460  261 
in (env, dp::flexflex, flexrigid) end 
0  262 
 (Var _, _) => 
16664  263 
((assignment thy (env,rbinder,t,u), flexflex, flexrigid) 
1460  264 
handle ASSIGN => (env, flexflex, dp::flexrigid)) 
0  265 
 (_, Var _) => 
16664  266 
((assignment thy (env,rbinder,u,t), flexflex, flexrigid) 
1460  267 
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) 
0  268 
 (Const(a,T), Const(b,U)) => 
16664  269 
if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) 
1460  270 
else raise CANTUNIFY 
0  271 
 (Bound i, Bound j) => 
1460  272 
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY 
0  273 
 (Free(a,T), Free(b,U)) => 
16664  274 
if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) 
1460  275 
else raise CANTUNIFY 
0  276 
 _ => raise CANTUNIFY 
277 
end; 

278 

279 

280 
(* changed(env,t) checks whether the head of t is a variable assigned in env*) 

281 
fun changed (env, f$_) = changed (env,f) 

15797  282 
 changed (env, Var v) = 
15531  283 
(case Envir.lookup(env,v) of NONE=>false  _ => true) 
0  284 
 changed _ = false; 
285 

286 

287 
(*Recursion needed if any of the 'head variables' have been updated 

288 
Clever would be to redo just the affected dpairs*) 

16664  289 
fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = 
0  290 
let val all as (env',flexflex,flexrigid) = 
16664  291 
foldr (SIMPL0 thy) (env,[],[]) dpairs; 
1460  292 
val dps = flexrigid@flexflex 
0  293 
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps 
16664  294 
then SIMPL thy (env',dps) else all 
0  295 
end; 
296 

297 

298 
(*computes t(Bound(n+k1),...,Bound(n)) *) 

299 
fun combound (t, n, k) = 

300 
if k>0 then combound (t,n+1,k1) $ (Bound n) else t; 

301 

302 

303 
(*Makes the terms E1,...,Em, where Ts = [T...Tm]. 

304 
Each Ei is ?Gi(B.(n1),...,B.0), and has type Ti 

305 
The B.j are bound vars of binder. 

306 
The terms are not made in etanormalform, SIMPL does that later. 

307 
If done here, etaexpansion must be recursive in the arguments! *) 

308 
fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*) 

309 
 make_args name (binder: typ list, env, Ts) : Envir.env * term list = 

310 
let fun funtype T = binder>T; 

1460  311 
val (env', vars) = Envir.genvars name (env, map funtype Ts) 
0  312 
in (env', map (fn var=> combound(var, 0, length binder)) vars) end; 
313 

314 

315 
(*Abstraction over a list of types, like list_abs*) 

316 
fun types_abs ([],u) = u 

317 
 types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u)); 

318 

319 
(*Abstraction over the binder of a type*) 

320 
fun type_abs (env,T,t) = types_abs(binder_types env T, t); 

321 

322 

323 
(*MATCH taking "big steps". 

324 
Copies u into the Var v, using projection on targs or imitation. 

325 
A projection is allowed unless SIMPL raises an exception. 

326 
Allocates new variables in projection on a higherorder argument, 

327 
or if u is a variable (flexflex dpair). 

328 
Returns long sequence of every way of copying u, for backtracking 

329 
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. 

330 
The order for trying projections is crucial in ?b'(?a) 

331 
NB "vname" is only used in the call to make_args!! *) 

16664  332 
fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
4270  333 
: (term * (Envir.env * dpair list))Seq.seq = 
0  334 
let (*Produce copies of uarg and cons them in front of uargs*) 
335 
fun copycons uarg (uargs, (env, dpairs)) = 

4270  336 
Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) 
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

337 
(mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), 
1460  338 
(env, dpairs))); 
339 
(*Produce sequence of all possible ways of copying the arg list*) 

4270  340 
fun copyargs [] = Seq.cons( ([],ed), Seq.empty) 
17344  341 
 copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs); 
0  342 
val (uhead,uargs) = strip_comb u; 
343 
val base = body_type env (fastype env (rbinder,uhead)); 

344 
fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed'); 

345 
(*attempt projection on argument with given typ*) 

346 
val Ts = map (curry (fastype env) rbinder) targs; 

347 
fun projenv (head, (Us,bary), targ, tail) = 

16664  348 
let val env = if !trace_types then test_unify_types thy (base,bary,env) 
349 
else unify_types thy (base,bary,env) 

4270  350 
in Seq.make (fn () => 
1460  351 
let val (env',args) = make_args vname (Ts,env,Us); 
352 
(*higherorder projection: plug in targs for bound vars*) 

353 
fun plugin arg = list_comb(head_of arg, targs); 

354 
val dp = (rbinder, list_comb(targ, map plugin args), u); 

16664  355 
val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs) 
1460  356 
(*may raise exception CANTUNIFY*) 
15531  357 
in SOME ((list_comb(head,args), (env2, frigid@fflex)), 
1460  358 
tail) 
4270  359 
end handle CANTUNIFY => Seq.pull tail) 
1460  360 
end handle CANTUNIFY => tail; 
0  361 
(*make a list of projections*) 
362 
fun make_projs (T::Ts, targ::targs) = 

1460  363 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) 
0  364 
 make_projs ([],[]) = [] 
365 
 make_projs _ = raise TERM ("make_projs", u::targs); 

366 
(*try projections and imitation*) 

367 
fun matchfun ((bvar,T,targ)::projs) = 

1460  368 
(projenv(bvar, strip_type env T, targ, matchfun projs)) 
0  369 
 matchfun [] = (*imitation last of all*) 
1460  370 
(case uhead of 
4270  371 
Const _ => Seq.map joinargs (copyargs uargs) 
372 
 Free _ => Seq.map joinargs (copyargs uargs) 

373 
 _ => Seq.empty) (*if Var, would be a loop!*) 

0  374 
in case uhead of 
1460  375 
Abs(a, T, body) => 
4270  376 
Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 
1460  377 
(mc ((a,T)::rbinder, 
378 
(map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) 

0  379 
 Var (w,uary) => 
1460  380 
(*a flexflex dpair: make variable for t*) 
381 
let val (env', newhd) = Envir.genvar (#1 w) (env, Ts> base) 

382 
val tabs = combound(newhd, 0, length Ts) 

383 
val tsub = list_comb(newhd,targs) 

4270  384 
in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
1460  385 
end 
0  386 
 _ => matchfun(rev(make_projs(Ts, targs))) 
387 
end 

388 
in mc end; 

389 

390 

391 
(*Call matchcopy to produce assignments to the variable in the dpair*) 

16664  392 
fun MATCH thy (env, (rbinder,t,u), dpairs) 
4270  393 
: (Envir.env * dpair list)Seq.seq = 
15797  394 
let val (Var (vT as (v, T)), targs) = strip_comb t; 
0  395 
val Ts = binder_types env T; 
396 
fun new_dset (u', (env',dpairs')) = 

1460  397 
(*if v was updated to s, must unify s with u' *) 
15797  398 
case Envir.lookup (env', vT) of 
399 
NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') 

15531  400 
 SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') 
4270  401 
in Seq.map new_dset 
16664  402 
(matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs))) 
0  403 
end; 
404 

405 

406 

407 
(**** Flexflex processing ****) 

408 

409 
(*At end of unification, do flexflex assignments like ?a > ?f(?b) 

410 
Attempts to update t with u, raising ASSIGN if impossible*) 

16664  411 
fun ff_assign thy (env, rbinder, t, u) : Envir.env = 
15797  412 
let val vT as (v,T) = get_eta_var(rbinder,0,t) 
413 
in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN 

16664  414 
else let val env = unify_types thy (body_type env T, 
1460  415 
fastype env (rbinder,u), 
416 
env) 

15797  417 
in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end 
0  418 
end; 
419 

420 

421 
(*Flex argument: a term, its type, and the index that refers to it.*) 

422 
type flarg = {t: term, T: typ, j: int}; 

423 

424 

425 
(*Form the arguments into records for deletion/sorting.*) 

426 
fun flexargs ([],[],[]) = [] : flarg list 

427 
 flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts) 

428 
 flexargs _ = error"flexargs"; 

429 

430 

431 
(*If an argument contains a banned Bound, then it should be deleted. 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

432 
But if the only path is flexible, this is difficult; the code gives up! 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

433 
In %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

434 
exception CHANGE_FAIL; (*flexible occurrence of banned variable*) 
0  435 

436 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

437 
(*Check whether the 'banned' bound var indices occur rigidly in t*) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

438 
fun rigid_bound (lev, banned) t = 
0  439 
let val (head,args) = strip_comb t 
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

440 
in 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

441 
case head of 
2140
eaa7ab39889d
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson
parents:
1505
diff
changeset

442 
Bound i => (ilev) mem_int banned orelse 
1460  443 
exists (rigid_bound (lev, banned)) args 
444 
 Var _ => false (*no rigid occurrences here!*) 

445 
 Abs (_,_,u) => 

446 
rigid_bound(lev+1, banned) u orelse 

447 
exists (rigid_bound (lev, banned)) args 

448 
 _ => exists (rigid_bound (lev, banned)) args 

0  449 
end; 
450 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

451 
(*Squash down indices at level >=lev to delete the banned from a term.*) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

452 
fun change_bnos banned = 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

453 
let fun change lev (Bound i) = 
1460  454 
if i<lev then Bound i 
2140
eaa7ab39889d
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson
parents:
1505
diff
changeset

455 
else if (ilev) mem_int banned 
1460  456 
then raise CHANGE_FAIL (**flexible occurrence: give up**) 
15570  457 
else Bound (i  length (List.filter (fn j => j < ilev) banned)) 
1460  458 
 change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) 
459 
 change lev (t$u) = change lev t $ change lev u 

460 
 change lev t = t 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

461 
in change 0 end; 
0  462 

463 
(*Change indices, delete the argument if it contains a banned Bound*) 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

464 
fun change_arg banned ({j,t,T}, args) : flarg list = 
1460  465 
if rigid_bound (0, banned) t then args (*delete argument!*) 
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

466 
else {j=j, t= change_bnos banned t, T=T} :: args; 
0  467 

468 

469 
(*Sort the arguments to create assignments if possible: 

470 
create etaterms like ?g(B.1,B.0) *) 

471 
fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1) 

472 
 arg_less (_:flarg, _:flarg) = false; 

473 

474 
(*Test whether the new term would be etaequivalent to a variable  

475 
if so then there is no point in creating a new variable*) 

476 
fun decreasing n ([]: flarg list) = (n=0) 

477 
 decreasing n ({j,...}::args) = j=n1 andalso decreasing (n1) args; 

478 

479 
(*Delete banned indices in the term, simplifying it. 

480 
Force an assignment, if possible, by sorting the arguments. 

481 
Update its head; squash indices in arguments. *) 

482 
fun clean_term banned (env,t) = 

483 
let val (Var(v,T), ts) = strip_comb t 

1460  484 
val (Ts,U) = strip_type env T 
485 
and js = length ts  1 downto 0 

4438  486 
val args = sort (make_ord arg_less) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

487 
(foldr (change_arg banned) [] (flexargs (js,ts,Ts))) 
1460  488 
val ts' = map (#t) args 
0  489 
in 
490 
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts'))) 

491 
else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args > U) 

1460  492 
val body = list_comb(v', map (Bound o #j) args) 
15797  493 
val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)), env')) 
1460  494 
(*the vupdate affects ts' if they contain v*) 
495 
in 

496 
(env2, Envir.norm_term env2 (list_comb(v',ts'))) 

0  497 
end 
498 
end; 

499 

500 

501 
(*Add tpair if not trivial or already there. 

502 
Should check for swapped pairs??*) 

503 
fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list = 

504 
if t0 aconv u0 then tpairs 

505 
else 

506 
let val t = rlist_abs(rbinder, t0) and u = rlist_abs(rbinder, u0); 

507 
fun same(t',u') = (t aconv t') andalso (u aconv u') 

508 
in if exists same tpairs then tpairs else (t,u)::tpairs end; 

509 

510 

511 
(*Simplify both terms and check for assignments. 

512 
Bound vars in the binder are "banned" unless used in both t AND u *) 

16664  513 
fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = 
0  514 
let val loot = loose_bnos t and loou = loose_bnos u 
515 
fun add_index (((a,T), j), (bnos, newbinder)) = 

2140
eaa7ab39889d
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson
parents:
1505
diff
changeset

516 
if j mem_int loot andalso j mem_int loou 
1460  517 
then (bnos, (a,T)::newbinder) (*needed by both: keep*) 
518 
else (j::bnos, newbinder); (*remove*) 

0  519 
val indices = 0 upto (length rbinder  1); 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

520 
val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices); 
0  521 
val (env', t') = clean_term banned (env, t); 
522 
val (env'',u') = clean_term banned (env',u) 

16664  523 
in (ff_assign thy (env'', rbin', t', u'), tpairs) 
524 
handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs) 

0  525 
handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) 
526 
end 

527 
handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs)); 

528 

529 

530 
(*IF the flexflex dpair is an assignment THEN do it ELSE put in tpairs 

531 
eliminates trivial tpairs like t=t, as well as repeated ones 

532 
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t 

533 
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) 

16664  534 
fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) 
0  535 
: Envir.env * (term*term)list = 
536 
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0 

537 
in case (head_of t, head_of u) of 

538 
(Var(v,T), Var(w,U)) => (*Check for identical variables...*) 

2753  539 
if eq_ix(v,w) then (*...occur check would falsely return true!*) 
1460  540 
if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) 
541 
else raise TERM ("add_ffpair: Var name confusion", [t,u]) 

542 
else if xless(v,w) then (*prefer to update the LARGER variable*) 

16664  543 
clean_ffpair thy ((rbinder, u, t), (env,tpairs)) 
544 
else clean_ffpair thy ((rbinder, t, u), (env,tpairs)) 

0  545 
 _ => raise TERM ("add_ffpair: Vars expected", [t,u]) 
546 
end; 

547 

548 

549 
(*Print a tracing message + list of dpairs. 

550 
In t==u print u first because it may be rigid or flexible  

551 
t is always flexible.*) 

16664  552 
fun print_dpairs thy msg (env,dpairs) = 
0  553 
let fun pdp (rbinder,t,u) = 
16664  554 
let fun termT t = Sign.pretty_term thy 
0  555 
(Envir.norm_term env (rlist_abs(rbinder,t))) 
556 
val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, 

557 
termT t]; 

12262  558 
in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end; 
15570  559 
in tracing msg; List.app pdp dpairs end; 
0  560 

561 

562 
(*Unify the dpairs in the environment. 

563 
Returns flexflex disagreement pairs NOT IN normal form. 

564 
SIMPL may raise exception CANTUNIFY. *) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

565 
fun hounifiers (thy,env, tus : (term*term)list) 
4270  566 
: (Envir.env * (term*term)list)Seq.seq = 
0  567 
let fun add_unify tdepth ((env,dpairs), reseq) = 
4270  568 
Seq.make (fn()=> 
1460  569 
let val (env',flexflex,flexrigid) = 
570 
(if tdepth> !trace_bound andalso !trace_simp 

16664  571 
then print_dpairs thy "Enter SIMPL" (env,dpairs) else (); 
572 
SIMPL thy (env,dpairs)) 

1460  573 
in case flexrigid of 
16664  574 
[] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq) 
1460  575 
 dp::frigid' => 
576 
if tdepth > !search_bound then 

4314  577 
(warning "Unification bound exceeded"; Seq.pull reseq) 
1460  578 
else 
579 
(if tdepth > !trace_bound then 

16664  580 
print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) 
1460  581 
else (); 
4270  582 
Seq.pull (Seq.it_right (add_unify (tdepth+1)) 
16664  583 
(MATCH thy (env',dp, frigid'@flexflex), reseq))) 
1460  584 
end 
585 
handle CANTUNIFY => 

12262  586 
(if tdepth > !trace_bound then tracing"Failure node" else (); 
4270  587 
Seq.pull reseq)); 
0  588 
val dps = map (fn(t,u)=> ([],t,u)) tus 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

589 
in add_unify 1 ((env, dps), Seq.empty) end; 
0  590 

18184  591 
fun unifiers (params as (thy, env, tus)) = 
592 
Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

593 
handle Pattern.Unif => Seq.empty 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

594 
 Pattern.Pattern => hounifiers params; 
0  595 

596 

597 
(*For smash_flexflex1*) 

598 
fun var_head_of (env,t) : indexname * typ = 

599 
case head_of (strip_abs_body (Envir.norm_term env t)) of 

600 
Var(v,T) => (v,T) 

601 
 _ => raise CANTUNIFY; (*not flexible, cannot use trivial substitution*) 

602 

603 

604 
(*Eliminate a flexflex pair by the trivial substitution, see Huet (1975) 

605 
Unifies ?f(t1...rm) with ?g(u1...un) by ?f > %x1...xm.?a, ?g > %x1...xn.?a 

606 
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g > %(x,y)?a, 

1460  607 
though just ?g>?f is a more general unifier. 
0  608 
Unlike Huet (1975), does not smash together all variables of same type  
609 
requires more work yet gives a less general unifier (fewer variables). 

610 
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) 

611 
fun smash_flexflex1 ((t,u), env) : Envir.env = 

15797  612 
let val vT as (v,T) = var_head_of (env,t) 
613 
and wU as (w,U) = var_head_of (env,u); 

0  614 
val (env', var) = Envir.genvar (#1v) (env, body_type env T) 
15797  615 
val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env') 
616 
in if vT = wU then env'' (*the other update would be identical*) 

617 
else Envir.vupdate ((vT, type_abs (env', T, var)), env'') 

0  618 
end; 
619 

620 

621 
(*Smash all flexflexpairs. Should allow selection of pairs by a predicate?*) 

622 
fun smash_flexflex (env,tpairs) : Envir.env = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

623 
foldr smash_flexflex1 env tpairs; 
0  624 

625 
(*Returns unifiers with no remaining disagreement pairs*) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

626 
fun smash_unifiers (thy, env, tus) : Envir.env Seq.seq = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

627 
Seq.map smash_flexflex (unifiers(thy,env,tus)); 
0  628 

629 
end; 