author  wenzelm 
Thu, 31 May 2007 23:47:36 +0200  
changeset 23178  07ba6b58b3d2 
parent 20664  ffbc5a57191a 
child 24178  4ff1dc2aa18d 
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 
val trace_bound: int ref 
16 
val trace_simp: bool ref 

17 
val trace_types: bool ref 

18 
val search_bound: int ref 

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

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

20 
(Envir.env * (term * term) list) Seq.seq 
19864  21 
val smash_unifiers: theory > (term * term) list > Envir.env > Envir.env Seq.seq 
22 
val matchers: theory > (term * term) list > Envir.env Seq.seq 

23 
val matches_list: theory > term list > term list > bool 

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

24 
end 
0  25 

19864  26 
structure Unify : UNIFY = 
0  27 
struct 
28 

29 
(*Unification options*) 

30 

19864  31 
val trace_bound = ref 25 (*tracing starts above this depth, 0 for full*) 
32 
and search_bound = ref 30 (*unification quits above this depth*) 

33 
and trace_simp = ref false (*print dpairs before calling SIMPL*) 

19876  34 
and trace_types = ref false (*announce potential incompleteness of type unification*) 
0  35 

36 
type binderlist = (string*typ) list; 

37 

38 
type dpair = binderlist * term * term; 

39 

19864  40 
fun body_type(Envir.Envir{iTs,...}) = 
0  41 
let fun bT(Type("fun",[_,T])) = bT T 
15797  42 
 bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of 
19864  43 
NONE => T  SOME(T') => bT T') 
0  44 
 bT T = T 
45 
in bT end; 

46 

19864  47 
fun binder_types(Envir.Envir{iTs,...}) = 
0  48 
let fun bTs(Type("fun",[T,U])) = T :: bTs U 
15797  49 
 bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of 
19864  50 
NONE => []  SOME(T') => bTs T') 
0  51 
 bTs _ = [] 
52 
in bTs end; 

53 

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

55 

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

56 
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; 
0  57 

58 

59 
(*Eta normal form*) 

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

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

19864  62 
Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) 
63 
 etif (TVar ixnS, t) = 

64 
(case Type.lookup (iTs, ixnS) of 

65 
NONE => t  SOME(T) => etif(T,t)) 

66 
 etif (_,t) = t; 

0  67 
fun eta_nm (rbinder, Abs(a,T,body)) = 
19864  68 
Abs(a, T, eta_nm ((a,T)::rbinder, body)) 
69 
 eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) 

0  70 
in eta_nm end; 
71 

72 

73 
(*OCCURS CHECK 

19864  74 
Does the uvar occur in the term t? 
0  75 
two forms of search, for whether there is a rigid path to the current term. 
76 
"seen" is list of variables passed thru, is a memo variable for sharing. 

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

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

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

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

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

89 
 occur (Var (w, T)) = 

20083  90 
if member (op =) (!seen) w then false 
19864  91 
else if eq_ix(v,w) then true 
92 
(*no need to lookup: v has no assignment*) 

93 
else (seen := w:: !seen; 

94 
case Envir.lookup (env, (w, T)) of 

95 
NONE => false 

96 
 SOME t => occur t) 

97 
 occur (Abs(_,_,body)) = occur body 

98 
 occur (f$t) = occur t orelse occur f 

0  99 
in occurs ts end; 
100 

101 

102 

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

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

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

19864  106 
 Var vT => (case Envir.lookup (env, vT) of 
107 
SOME u => head_of_in(env,u)  NONE => t) 

0  108 
 _ => t; 
109 

110 

111 
datatype occ = NoOcc  Nonrigid  Rigid; 

112 

113 
(* Rigid occur check 

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

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

116 
NoOcc otherwise. 

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

118 

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

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

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

122 
reject ALL rigid paths to the variable. 

19864  123 
Could check for rigid paths to bound variables that are out of scope. 
0  124 
Not necessary because the assignment test looks at variable's ENTIRE rbinder. 
125 

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

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

19864  128 
for arg1,...,argn. 
129 
If head is an abstraction then possibly no rigid path (head could be a 

0  130 
constant function) so again use nonrigid search. Happens only if 
19864  131 
term is not in normal form. 
0  132 

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

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

135 
*) 

19864  136 
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
137 
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 

138 
else NoOcc 

0  139 
fun occurs [] = NoOcc 
19864  140 
 occurs (t::ts) = 
0  141 
(case occur t of 
142 
Rigid => Rigid 

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

144 
and occomb (f$t) = 

145 
(case occur t of 

146 
Rigid => Rigid 

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

148 
 occomb t = occur t 

149 
and occur (Const _) = NoOcc 

19864  150 
 occur (Bound _) = NoOcc 
151 
 occur (Free _) = NoOcc 

152 
 occur (Var (w, T)) = 

20083  153 
if member (op =) (!seen) w then NoOcc 
19864  154 
else if eq_ix(v,w) then Rigid 
155 
else (seen := w:: !seen; 

156 
case Envir.lookup (env, (w, T)) of 

157 
NONE => NoOcc 

158 
 SOME t => occur t) 

159 
 occur (Abs(_,_,body)) = occur body 

160 
 occur (t as f$_) = (*switch to nonrigid search?*) 

161 
(case head_of_in (env,f) of 

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

163 
if eq_ix(v,w) then Rigid 

164 
else nonrigid t 

165 
 Abs(_,_,body) => nonrigid t (*not in normal form*) 

166 
 _ => occomb t) 

0  167 
in occur t end; 
168 

169 

19864  170 
exception CANTUNIFY; (*Signals nonunifiability. Does not signal errors!*) 
171 
exception ASSIGN; (*Raised if not an assignment*) 

0  172 

173 

16664  174 
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

175 
if T=U then env 
16934  176 
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

177 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
1505  178 
handle Type.TUNIFY => raise CANTUNIFY; 
0  179 

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

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

183 
val env' = unify_types thy args 

0  184 
in if is_TVar(T) orelse is_TVar(U) then warn() else (); 
185 
env' 

186 
end; 

187 

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

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

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

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

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

19864  193 
if n=i then get_eta_var (rbinder, n+1, f) 
194 
else raise ASSIGN 

0  195 
 get_eta_var _ = raise ASSIGN; 
196 

197 

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

199 
If v occurs rigidly then nonunifiable. 

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

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

19864  204 
NoOcc => let val env = unify_types thy (body_type env T, 
205 
fastype env (rbinder,u),env) 

206 
in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end 

207 
 Nonrigid => raise ASSIGN 

208 
 Rigid => raise CANTUNIFY 

0  209 
end; 
210 

211 

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

213 
Tries to unify types of the bound variables! 

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

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

19864  216 
Uses variable a (unless the null string) to preserve user's naming.*) 
16664  217 
fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = 
19864  218 
let val env' = unify_types thy (T,U,env) 
219 
val c = if a="" then b else a 

220 
in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end 

16664  221 
 new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", []) 
222 
 new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", []) 

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

0  224 

225 

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

19864  228 
eta_norm env (rbinder, Envir.head_norm env t), 
229 
eta_norm env (rbinder, Envir.head_norm env u), env); 

0  230 

231 

232 

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

234 
Does not perform assignments for flexflex pairs: 

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

237 
do so caused numerous problems with no compensating advantage. 

238 
*) 

16664  239 
fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) 
19864  240 
: Envir.env * dpair list * dpair list = 
16664  241 
let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0); 
19864  242 
fun SIMRANDS(f$t, g$u, env) = 
243 
SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env)) 

244 
 SIMRANDS (t as _$_, _, _) = 

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

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

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

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

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

19864  251 
let val T' = body_type env T and U' = body_type env U; 
252 
val env = unify_types thy (T',U',env) 

253 
in (env, dp::flexflex, flexrigid) end 

0  254 
 (Var _, _) => 
19864  255 
((assignment thy (env,rbinder,t,u), flexflex, flexrigid) 
256 
handle ASSIGN => (env, flexflex, dp::flexrigid)) 

0  257 
 (_, Var _) => 
19864  258 
((assignment thy (env,rbinder,u,t), flexflex, flexrigid) 
259 
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) 

0  260 
 (Const(a,T), Const(b,U)) => 
19864  261 
if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) 
262 
else raise CANTUNIFY 

0  263 
 (Bound i, Bound j) => 
19864  264 
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY 
0  265 
 (Free(a,T), Free(b,U)) => 
19864  266 
if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) 
267 
else raise CANTUNIFY 

0  268 
 _ => raise CANTUNIFY 
269 
end; 

270 

271 

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

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

15797  274 
 changed (env, Var v) = 
15531  275 
(case Envir.lookup(env,v) of NONE=>false  _ => true) 
0  276 
 changed _ = false; 
277 

278 

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

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

16664  281 
fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = 
0  282 
let val all as (env',flexflex,flexrigid) = 
23178  283 
List.foldr (SIMPL0 thy) (env,[],[]) dpairs; 
19864  284 
val dps = flexrigid@flexflex 
0  285 
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps 
16664  286 
then SIMPL thy (env',dps) else all 
0  287 
end; 
288 

289 

19864  290 
(*Makes the terms E1,...,Em, where Ts = [T...Tm]. 
0  291 
Each Ei is ?Gi(B.(n1),...,B.0), and has type Ti 
292 
The B.j are bound vars of binder. 

19864  293 
The terms are not made in etanormalform, SIMPL does that later. 
0  294 
If done here, etaexpansion must be recursive in the arguments! *) 
295 
fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*) 

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

297 
let fun funtype T = binder>T; 

19864  298 
val (env', vars) = Envir.genvars name (env, map funtype Ts) 
18945  299 
in (env', map (fn var=> Logic.combound(var, 0, length binder)) vars) end; 
0  300 

301 

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

303 
fun types_abs ([],u) = u 

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

305 

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

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

308 

309 

310 
(*MATCH taking "big steps". 

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

312 
A projection is allowed unless SIMPL raises an exception. 

313 
Allocates new variables in projection on a higherorder argument, 

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

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

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

19864  317 
The order for trying projections is crucial in ?b'(?a) 
0  318 
NB "vname" is only used in the call to make_args!! *) 
19864  319 
fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
320 
: (term * (Envir.env * dpair list))Seq.seq = 

0  321 
let (*Produce copies of uarg and cons them in front of uargs*) 
322 
fun copycons uarg (uargs, (env, dpairs)) = 

19864  323 
Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) 
324 
(mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), 

325 
(env, dpairs))); 

326 
(*Produce sequence of all possible ways of copying the arg list*) 

19473  327 
fun copyargs [] = Seq.cons ([],ed) Seq.empty 
17344  328 
 copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs); 
0  329 
val (uhead,uargs) = strip_comb u; 
330 
val base = body_type env (fastype env (rbinder,uhead)); 

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

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

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

19864  334 
fun projenv (head, (Us,bary), targ, tail) = 
335 
let val env = if !trace_types then test_unify_types thy (base,bary,env) 

336 
else unify_types thy (base,bary,env) 

337 
in Seq.make (fn () => 

338 
let val (env',args) = make_args vname (Ts,env,Us); 

339 
(*higherorder projection: plug in targs for bound vars*) 

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

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

342 
val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs) 

343 
(*may raise exception CANTUNIFY*) 

344 
in SOME ((list_comb(head,args), (env2, frigid@fflex)), 

345 
tail) 

346 
end handle CANTUNIFY => Seq.pull tail) 

347 
end handle CANTUNIFY => tail; 

0  348 
(*make a list of projections*) 
349 
fun make_projs (T::Ts, targ::targs) = 

19864  350 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) 
0  351 
 make_projs ([],[]) = [] 
352 
 make_projs _ = raise TERM ("make_projs", u::targs); 

353 
(*try projections and imitation*) 

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

19864  355 
(projenv(bvar, strip_type env T, targ, matchfun projs)) 
0  356 
 matchfun [] = (*imitation last of all*) 
19864  357 
(case uhead of 
358 
Const _ => Seq.map joinargs (copyargs uargs) 

359 
 Free _ => Seq.map joinargs (copyargs uargs) 

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

0  361 
in case uhead of 
19864  362 
Abs(a, T, body) => 
363 
Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 

364 
(mc ((a,T)::rbinder, 

365 
(map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) 

366 
 Var (w,uary) => 

367 
(*a flexflex dpair: make variable for t*) 

368 
let val (env', newhd) = Envir.genvar (#1 w) (env, Ts> base) 

369 
val tabs = Logic.combound(newhd, 0, length Ts) 

370 
val tsub = list_comb(newhd,targs) 

371 
in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 

372 
end 

0  373 
 _ => matchfun(rev(make_projs(Ts, targs))) 
374 
end 

375 
in mc end; 

376 

377 

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

16664  379 
fun MATCH thy (env, (rbinder,t,u), dpairs) 
19864  380 
: (Envir.env * dpair list)Seq.seq = 
15797  381 
let val (Var (vT as (v, T)), targs) = strip_comb t; 
0  382 
val Ts = binder_types env T; 
383 
fun new_dset (u', (env',dpairs')) = 

19864  384 
(*if v was updated to s, must unify s with u' *) 
385 
case Envir.lookup (env', vT) of 

386 
NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') 

387 
 SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') 

4270  388 
in Seq.map new_dset 
16664  389 
(matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs))) 
0  390 
end; 
391 

392 

393 

394 
(**** Flexflex processing ****) 

395 

19864  396 
(*At end of unification, do flexflex assignments like ?a > ?f(?b) 
0  397 
Attempts to update t with u, raising ASSIGN if impossible*) 
19864  398 
fun ff_assign thy (env, rbinder, t, u) : Envir.env = 
15797  399 
let val vT as (v,T) = get_eta_var(rbinder,0,t) 
400 
in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN 

16664  401 
else let val env = unify_types thy (body_type env T, 
19864  402 
fastype env (rbinder,u), 
403 
env) 

404 
in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end 

0  405 
end; 
406 

407 

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

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

410 

411 

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

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

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

415 
 flexargs _ = error"flexargs"; 

416 

417 

418 
(*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

419 
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

420 
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

421 
exception CHANGE_FAIL; (*flexible occurrence of banned variable*) 
0  422 

423 

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

424 
(*Check whether the 'banned' bound var indices occur rigidly in t*) 
19864  425 
fun rigid_bound (lev, banned) t = 
426 
let val (head,args) = strip_comb t 

427 
in 

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

428 
case head of 
20664  429 
Bound i => member (op =) banned (ilev) orelse 
19864  430 
exists (rigid_bound (lev, banned)) args 
431 
 Var _ => false (*no rigid occurrences here!*) 

432 
 Abs (_,_,u) => 

433 
rigid_bound(lev+1, banned) u orelse 

434 
exists (rigid_bound (lev, banned)) args 

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

0  436 
end; 
437 

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

438 
(*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

439 
fun change_bnos banned = 
19864  440 
let fun change lev (Bound i) = 
441 
if i<lev then Bound i 

20664  442 
else if member (op =) banned (ilev) 
19864  443 
then raise CHANGE_FAIL (**flexible occurrence: give up**) 
444 
else Bound (i  length (List.filter (fn j => j < ilev) banned)) 

445 
 change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) 

446 
 change lev (t$u) = change lev t $ change lev u 

447 
 change lev t = t 

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

448 
in change 0 end; 
0  449 

450 
(*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

451 
fun change_arg banned ({j,t,T}, args) : flarg list = 
19864  452 
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

453 
else {j=j, t= change_bnos banned t, T=T} :: args; 
0  454 

455 

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

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

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

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

460 

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

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

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

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

465 

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

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

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

469 
fun clean_term banned (env,t) = 

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

19864  471 
val (Ts,U) = strip_type env T 
472 
and js = length ts  1 downto 0 

473 
val args = sort (make_ord arg_less) 

23178  474 
(List.foldr (change_arg banned) [] (flexargs (js,ts,Ts))) 
19864  475 
val ts' = map (#t) args 
0  476 
in 
477 
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts'))) 

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

19864  479 
val body = list_comb(v', map (Bound o #j) args) 
480 
val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)), env')) 

481 
(*the vupdate affects ts' if they contain v*) 

482 
in 

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

0  484 
end 
485 
end; 

486 

487 

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

489 
Should check for swapped pairs??*) 

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

19864  491 
if t0 aconv u0 then tpairs 
0  492 
else 
18945  493 
let val t = Logic.rlist_abs(rbinder, t0) and u = Logic.rlist_abs(rbinder, u0); 
0  494 
fun same(t',u') = (t aconv t') andalso (u aconv u') 
495 
in if exists same tpairs then tpairs else (t,u)::tpairs end; 

496 

497 

498 
(*Simplify both terms and check for assignments. 

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

19864  500 
fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = 
0  501 
let val loot = loose_bnos t and loou = loose_bnos u 
19864  502 
fun add_index (((a,T), j), (bnos, newbinder)) = 
20664  503 
if member (op =) loot j andalso member (op =) loou j 
19864  504 
then (bnos, (a,T)::newbinder) (*needed by both: keep*) 
505 
else (j::bnos, newbinder); (*remove*) 

0  506 
val indices = 0 upto (length rbinder  1); 
23178  507 
val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices); 
0  508 
val (env', t') = clean_term banned (env, t); 
509 
val (env'',u') = clean_term banned (env',u) 

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

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

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

515 

516 

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

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

19864  519 
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t 
0  520 
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) 
19864  521 
fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) 
0  522 
: Envir.env * (term*term)list = 
523 
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0 

524 
in case (head_of t, head_of u) of 

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

19864  526 
if eq_ix(v,w) then (*...occur check would falsely return true!*) 
527 
if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) 

528 
else raise TERM ("add_ffpair: Var name confusion", [t,u]) 

20098  529 
else if Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*) 
19864  530 
clean_ffpair thy ((rbinder, u, t), (env,tpairs)) 
16664  531 
else clean_ffpair thy ((rbinder, t, u), (env,tpairs)) 
0  532 
 _ => raise TERM ("add_ffpair: Vars expected", [t,u]) 
533 
end; 

534 

535 

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

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

538 
t is always flexible.*) 

16664  539 
fun print_dpairs thy msg (env,dpairs) = 
0  540 
let fun pdp (rbinder,t,u) = 
16664  541 
let fun termT t = Sign.pretty_term thy 
18945  542 
(Envir.norm_term env (Logic.rlist_abs(rbinder,t))) 
0  543 
val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, 
544 
termT t]; 

12262  545 
in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end; 
15570  546 
in tracing msg; List.app pdp dpairs end; 
0  547 

548 

549 
(*Unify the dpairs in the environment. 

19864  550 
Returns flexflex disagreement pairs NOT IN normal form. 
0  551 
SIMPL may raise exception CANTUNIFY. *) 
19864  552 
fun hounifiers (thy,env, tus : (term*term)list) 
4270  553 
: (Envir.env * (term*term)list)Seq.seq = 
0  554 
let fun add_unify tdepth ((env,dpairs), reseq) = 
19864  555 
Seq.make (fn()=> 
556 
let val (env',flexflex,flexrigid) = 

557 
(if tdepth> !trace_bound andalso !trace_simp 

558 
then print_dpairs thy "Enter SIMPL" (env,dpairs) else (); 

559 
SIMPL thy (env,dpairs)) 

560 
in case flexrigid of 

23178  561 
[] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq) 
19864  562 
 dp::frigid' => 
563 
if tdepth > !search_bound then 

564 
(warning "Unification bound exceeded"; Seq.pull reseq) 

565 
else 

566 
(if tdepth > !trace_bound then 

567 
print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) 

568 
else (); 

569 
Seq.pull (Seq.it_right (add_unify (tdepth+1)) 

570 
(MATCH thy (env',dp, frigid'@flexflex), reseq))) 

571 
end 

572 
handle CANTUNIFY => 

573 
(if tdepth > !trace_bound then tracing"Failure node" else (); 

574 
Seq.pull reseq)); 

0  575 
val dps = map (fn(t,u)=> ([],t,u)) tus 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

576 
in add_unify 1 ((env, dps), Seq.empty) end; 
0  577 

18184  578 
fun unifiers (params as (thy, env, tus)) = 
19473  579 
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

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

581 
 Pattern.Pattern => hounifiers params; 
0  582 

583 

584 
(*For smash_flexflex1*) 

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

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

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

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

589 

590 

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

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

19864  593 
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g > %(x,y)?a, 
594 
though just ?g>?f is a more general unifier. 

0  595 
Unlike Huet (1975), does not smash together all variables of same type  
596 
requires more work yet gives a less general unifier (fewer variables). 

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

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

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

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

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

0  605 
end; 
606 

607 

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

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

23178  610 
List.foldr smash_flexflex1 env tpairs; 
0  611 

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

19864  613 
fun smash_unifiers thy tus env = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

614 
Seq.map smash_flexflex (unifiers(thy,env,tus)); 
0  615 

19864  616 

617 
(*Pattern matching*) 

20020
9e7d3d06c643
matchers: fall back on plain first_order_matchers, not pattern;
wenzelm
parents:
19920
diff
changeset

618 
fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) = 
9e7d3d06c643
matchers: fall back on plain first_order_matchers, not pattern;
wenzelm
parents:
19920
diff
changeset

619 
let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) 
19864  620 
in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end 
621 
handle Pattern.MATCH => Seq.empty; 

622 

623 
(*General matching  keeps variables disjoint*) 

624 
fun matchers _ [] = Seq.single (Envir.empty ~1) 

625 
 matchers thy pairs = 

626 
let 

627 
val maxidx = fold (Term.maxidx_term o #2) pairs ~1; 

628 
val offset = maxidx + 1; 

629 
val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs; 

630 
val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; 

631 

632 
val pat_tvars = fold (Term.add_tvars o #1) pairs' []; 

633 
val pat_vars = fold (Term.add_vars o #1) pairs' []; 

634 

635 
val decr_indexesT = 

636 
Term.map_atyps (fn T as TVar ((x, i), S) => 

637 
if i > maxidx then TVar ((x, i  offset), S) else T  T => T); 

638 
val decr_indexes = 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20098
diff
changeset

639 
Term.map_types decr_indexesT #> 
19864  640 
Term.map_aterms (fn t as Var ((x, i), T) => 
641 
if i > maxidx then Var ((x, i  offset), T) else t  t => t); 

642 

643 
fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) = 

644 
((x, i  offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S))))); 

645 
fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) = 

646 
let 

647 
val T' = Envir.norm_type tyenv T; 

648 
val t' = Envir.norm_term env (Var ((x, i), T')); 

649 
in ((x, i  offset), (decr_indexesT T', decr_indexes t')) end; 

650 

651 
fun result env = 

19876  652 
if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) 
19864  653 
SOME (Envir.Envir {maxidx = maxidx, 
19866  654 
iTs = Vartab.make (map (norm_tvar env) pat_tvars), 
655 
asol = Vartab.make (map (norm_var env) pat_vars)}) 

656 
else NONE; 

19864  657 

658 
val empty = Envir.empty maxidx'; 

659 
in 

19876  660 
Seq.append 
19920
8257e52164a1
matchers: try pattern_matchers only *after* general matching (The
wenzelm
parents:
19876
diff
changeset

661 
(Seq.map_filter result (smash_unifiers thy pairs' empty)) 
20020
9e7d3d06c643
matchers: fall back on plain first_order_matchers, not pattern;
wenzelm
parents:
19920
diff
changeset

662 
(first_order_matchers thy pairs empty) 
19864  663 
end; 
664 

665 
fun matches_list thy ps os = 

666 
length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os))); 

667 

0  668 
end; 