author  wenzelm 
Thu, 17 Jan 2002 21:00:38 +0100  
changeset 12797  4de06a8f67ef 
parent 12784  bab3b002cbbb 
child 12817  fcbb6ad5c790 
permissions  rwrr 
12784  1 
(* Title: Pure/pattern.ML 
0  2 
ID: $Id$ 
12784  3 
Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

0  5 

6 
Unification of HigherOrder Patterns. 

7 

8 
See also: 

9 
Tobias Nipkow. Functional Unification of HigherOrder Patterns. 

10 
In Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993. 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

11 

6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

12 
TODO: optimize red by specialcasing it 
0  13 
*) 
14 

2751  15 
infix aeconv; 
16 

0  17 
signature PATTERN = 
1501  18 
sig 
0  19 
type type_sig 
20 
type sg 

21 
type env 

2751  22 
val aeconv : term * term > bool 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

23 
val eta_contract : term > term 
12781  24 
val beta_eta_contract : term > term 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

25 
val eta_contract_atom : term > term 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

26 
val match : type_sig > term * term 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

27 
> (indexname*typ)list * (indexname*term)list 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

28 
val first_order_match : type_sig > term * term 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

29 
> (indexname*typ)list * (indexname*term)list 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

30 
val matches : type_sig > term * term > bool 
4667
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

31 
val matches_subterm : type_sig > term * term > bool 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

32 
val unify : sg * env * (term * term)list > env 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

33 
val first_order : term > bool 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

34 
val pattern : term > bool 
12784  35 
val rewrite_term : type_sig > (term * term) list > term > term 
0  36 
exception Unif 
37 
exception MATCH 

38 
exception Pattern 

1501  39 
end; 
0  40 

1501  41 
structure Pattern : PATTERN = 
0  42 
struct 
43 

44 
type type_sig = Type.type_sig 

45 
type sg = Sign.sg 

46 
type env = Envir.env 

47 

48 
exception Unif; 

49 
exception Pattern; 

50 

12784  51 
fun occurs(F,t,env) = 
0  52 
let fun occ(Var(G,_)) = (case Envir.lookup(env,G) of 
53 
Some(t) => occ t 

54 
 None => F=G) 

55 
 occ(t1$t2) = occ t1 orelse occ t2 

56 
 occ(Abs(_,_,t)) = occ t 

57 
 occ _ = false 

58 
in occ t end; 

59 

60 

61 
fun mapbnd f = 

62 
let fun mpb d (Bound(i)) = if i < d then Bound(i) else Bound(f(id)+d) 

63 
 mpb d (Abs(s,T,t)) = Abs(s,T,mpb(d+1) t) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

64 
 mpb d ((u1 $ u2)) = (mpb d u1)$(mpb d u2) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

65 
 mpb _ atom = atom 
0  66 
in mpb 0 end; 
67 

68 
fun idx [] j = ~10000 

69 
 idx(i::is) j = if i=j then length is else idx is j; 

70 

71 
fun at xs i = nth_elem (i,xs); 

72 

73 
fun mkabs (binders,is,t) = 

74 
let fun mk(i::is) = let val (x,T) = nth_elem(i,binders) 

12784  75 
in Abs(x,T,mk is) end 
0  76 
 mk [] = t 
77 
in mk is end; 

78 

79 
val incr = mapbnd (fn i => i+1); 

80 

81 
fun ints_of [] = [] 

12784  82 
 ints_of (Bound i ::bs) = 
0  83 
let val is = ints_of bs 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1501
diff
changeset

84 
in if i mem_int is then raise Pattern else i::is end 
0  85 
 ints_of _ = raise Pattern; 
86 

12232  87 
fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); 
88 

0  89 

90 
fun app (s,(i::is)) = app (s$Bound(i),is) 

91 
 app (s,[]) = s; 

92 

93 
fun red (Abs(_,_,s)) (i::is) js = red s is (i::js) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

94 
 red t [] [] = t 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

95 
 red t is jn = app (mapbnd (at jn) t,is); 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

96 

0  97 

98 
(* split_type ([T1,....,Tn]> T,n,[]) = ([Tn,...,T1],T) *) 

99 
fun split_type (T,0,Ts) = (Ts,T) 

100 
 split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n1,T1::Ts) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

101 
 split_type _ = error("split_type"); 
0  102 

103 
fun type_of_G (T,n,is) = 

104 
let val (Ts,U) = split_type(T,n,[]) in map(at Ts)is > U end; 

105 

106 
fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); 

107 

108 
fun mknewhnf(env,binders,is,F as (a,_),T,js) = 

109 
let val (env',G) = Envir.genvar a (env,type_of_G(T,length is,js)) 

110 
in Envir.update((F,mkhnf(binders,is,G,js)),env') end; 

111 

112 

113 
(* mk_proj_list(is) = [ is  k  1 <= k <= is and is[k] >= 0 ] *) 

114 
fun mk_proj_list is = 

115 
let fun mk(i::is,j) = if i >= 0 then j :: mk(is,j1) else mk(is,j1) 

116 
 mk([],_) = [] 

117 
in mk(is,length is  1) end; 

118 

119 
fun proj(s,env,binders,is) = 

120 
let fun trans d i = if i<d then i else (idx is (id))+d; 

12232  121 
fun pr(s,env,d,binders) = (case Envir.head_norm env s of 
0  122 
Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders)) 
123 
in (Abs(a,T,t'),env') end 

124 
 t => (case strip_comb t of 

125 
(c as Const _,ts) => 

126 
let val (ts',env') = prs(ts,env,d,binders) 

127 
in (list_comb(c,ts'),env') end 

128 
 (f as Free _,ts) => 

129 
let val (ts',env') = prs(ts,env,d,binders) 

130 
in (list_comb(f,ts'),env') end 

131 
 (Bound(i),ts) => 

132 
let val j = trans d i 

133 
in if j < 0 then raise Unif 

134 
else let val (ts',env') = prs(ts,env,d,binders) 

135 
in (list_comb(Bound j,ts'),env') end 

136 
end 

137 
 (Var(F as (a,_),Fty),ts) => 

12232  138 
let val js = ints_of' env ts; 
0  139 
val js' = map (trans d) js; 
140 
val ks = mk_proj_list js'; 

141 
val ls = filter (fn i => i >= 0) js' 

142 
val Hty = type_of_G(Fty,length js,ks) 

143 
val (env',H) = Envir.genvar a (env,Hty) 

144 
val env'' = 

145 
Envir.update((F,mkhnf(binders,js,H,ks)),env') 

146 
in (app(H,ls),env'') end 

147 
 _ => raise Pattern)) 

148 
and prs(s::ss,env,d,binders) = 

149 
let val (s',env1) = pr(s,env,d,binders) 

150 
val (ss',env2) = prs(ss,env1,d,binders) 

151 
in (s'::ss',env2) end 

152 
 prs([],env,_,_) = ([],env) 

153 
in if downto0(is,length binders  1) then (s,env) 

154 
else pr(s,env,0,binders) 

155 
end; 

156 

157 

158 
(* mk_ff_list(is,js) = [ length(is)  k  1 <= k <= is and is[k] = js[k] ] *) 

12784  159 
fun mk_ff_list(is,js) = 
160 
let fun mk([],[],_) = [] 

0  161 
 mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k1) 
162 
else mk(is,js,k1) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

163 
 mk _ = error"mk_ff_list" 
0  164 
in mk(is,js,length is1) end; 
165 

166 
fun flexflex1(env,binders,F,Fty,is,js) = 

167 
if is=js then env 

168 
else let val ks = mk_ff_list(is,js) 

169 
in mknewhnf(env,binders,is,F,Fty,ks) end; 

170 

171 
fun flexflex2(env,binders,F,Fty,is,G,Gty,js) = 

172 
let fun ff(F,Fty,is,G as (a,_),Gty,js) = 

1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1501
diff
changeset

173 
if js subset_int is 
0  174 
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js)) 
175 
in Envir.update((F,t),env) end 

1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1501
diff
changeset

176 
else let val ks = is inter_int js 
0  177 
val Hty = type_of_G(Fty,length is,map (idx is) ks) 
178 
val (env',H) = Envir.genvar a (env,Hty) 

179 
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); 

180 
in Envir.update((G,lam js), Envir.update((F,lam is),env')) 

181 
end; 

182 
in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end 

183 

184 
val tsgr = ref(Type.tsig0); 

185 

186 
fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) = 

187 
if T=U then env 

12527  188 
else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1029
diff
changeset

189 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
0  190 
handle Type.TUNIFY => raise Unif; 
191 

12232  192 
fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of 
0  193 
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => 
194 
let val name = if ns = "" then nt else ns 

195 
in unif ((name,Ts)::binders) (env,(ts,tt)) end 

196 
 (Abs(ns,Ts,ts),t) => unif ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0))) 

197 
 (t,Abs(nt,Tt,tt)) => unif ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt)) 

198 
 p => cases(binders,env,p) 

199 

200 
and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of 

12784  201 
((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
12232  202 
if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) 
203 
else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) 

204 
 ((Var(F,_),ss),_) => flexrigid(env,binders,F,ints_of' env ss,t) 

205 
 (_,(Var(F,_),ts)) => flexrigid(env,binders,F,ints_of' env ts,s) 

0  206 
 ((Const c,ss),(Const d,ts)) => rigidrigid(env,binders,c,d,ss,ts) 
207 
 ((Free(f),ss),(Free(g),ts)) => rigidrigid(env,binders,f,g,ss,ts) 

12784  208 
 ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
0  209 
 ((Abs(_),_),_) => raise Pattern 
210 
 (_,(Abs(_),_)) => raise Pattern 

211 
 _ => raise Unif 

212 

213 
and rigidrigid (env,binders,(a,Ta),(b,Tb),ss,ts) = 

214 
if a<>b then raise Unif 

215 
else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts) 

216 

217 
and rigidrigidB (env,binders,i,j,ss,ts) = 

218 
if i <> j then raise Unif else foldl (unif binders) (env ,ss~~ts) 

219 

220 
and flexrigid (env,binders,F,is,t) = 

221 
if occurs(F,t,env) then raise Unif 

222 
else let val (u,env') = proj(t,env,binders,is) 

223 
in Envir.update((F,mkabs(binders,is,u)),env') end; 

224 

225 
fun unify(sg,env,tus) = (tsgr := #tsig(Sign.rep_sg sg); 

226 
foldl (unif []) (env,tus)); 

227 

228 

2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

229 
(*Etacontract a term (fully)*) 
2792  230 

12797  231 
fun eta_contract t = 
232 
let 

233 
exception SAME; 

234 
fun eta (Abs (a, T, body)) = 

235 
((case eta body of 

236 
body' as (f $ Bound 0) => 

237 
if loose_bvar1 (f, 0) then Abs(a, T, body') 

238 
else incr_boundvars ~1 f 

239 
 body' => Abs (a, T, body')) handle SAME => 

240 
(case body of 

241 
(f $ Bound 0) => 

242 
if loose_bvar1 (f, 0) then raise SAME 

243 
else incr_boundvars ~1 f 

244 
 _ => raise SAME)) 

245 
 eta (f $ t) = 

246 
(let val f' = eta f 

247 
in f' $ etah t end handle SAME => f $ eta t) 

248 
 eta _ = raise SAME 

249 
and etah t = (eta t handle SAME => t) 

250 
in etah t end; 

0  251 

12781  252 
val beta_eta_contract = eta_contract o Envir.beta_norm; 
253 

6539
2e7d2fba9f6c
Eta contraction is now performed all the time during rewriting.
nipkow
parents:
4820
diff
changeset

254 
(*Etacontract a term from outside: just enough to reduce it to an atom 
2e7d2fba9f6c
Eta contraction is now performed all the time during rewriting.
nipkow
parents:
4820
diff
changeset

255 
DOESN'T QUITE WORK! 
2e7d2fba9f6c
Eta contraction is now performed all the time during rewriting.
nipkow
parents:
4820
diff
changeset

256 
*) 
12784  257 
fun eta_contract_atom (t0 as Abs(a, T, body)) = 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

258 
(case eta_contract2 body of 
12784  259 
body' as (f $ Bound 0) => 
260 
if loose_bvar1(f,0) then Abs(a,T,body') 

261 
else eta_contract_atom (incr_boundvars ~1 f) 

2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

262 
 _ => t0) 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

263 
 eta_contract_atom t = t 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

264 
and eta_contract2 (f$t) = f $ eta_contract_atom t 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

265 
 eta_contract2 t = eta_contract_atom t; 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

266 

9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

267 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

268 
(*Tests whether 2 terms are alpha/etaconvertible and have same type. 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

269 
Note that Consts and Vars may have more than one type.*) 
2751  270 
fun t aeconv u = aconv_aux (eta_contract_atom t, eta_contract_atom u) 
271 
and aconv_aux (Const(a,T), Const(b,U)) = a=b andalso T=U 

272 
 aconv_aux (Free(a,T), Free(b,U)) = a=b andalso T=U 

273 
 aconv_aux (Var(v,T), Var(w,U)) = eq_ix(v,w) andalso T=U 

12784  274 
 aconv_aux (Bound i, Bound j) = i=j 
2751  275 
 aconv_aux (Abs(_,T,t), Abs(_,U,u)) = (t aeconv u) andalso T=U 
12784  276 
 aconv_aux (f$t, g$u) = (f aeconv g) andalso (t aeconv u) 
2751  277 
 aconv_aux _ = false; 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

278 

6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

279 

4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

280 
(*** Matching ***) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

281 

8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

282 
exception MATCH; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

283 

8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

284 
fun typ_match tsig args = (Type.typ_match tsig args) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

285 
handle Type.TYPE_MATCH => raise MATCH; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

286 

8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

287 
(*Firstorder matching; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

288 
fomatch tsig (pattern, object) returns a (tyvar,typ)list and (var,term)list. 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

289 
The pattern and object may have variables in common. 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

290 
Instantiation does not affect the object, so matching ?a with ?a+1 works. 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

291 
Object is etacontracted on the fly (by etaexpanding the pattern). 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

292 
Precondition: the pattern is already etacontracted! 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

293 
Note: types are matched on the fly *) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

294 
fun fomatch tsig = 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

295 
let 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

296 
fun mtch (instsp as (tyinsts,insts)) = fn 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

297 
(Var(ixn,T), t) => 
12784  298 
if loose_bvar(t,0) then raise MATCH 
299 
else (case assoc_string_int(insts,ixn) of 

300 
None => (typ_match tsig (tyinsts, (T, fastype_of t)), 

301 
(ixn,t)::insts) 

302 
 Some u => if t aeconv u then instsp else raise MATCH) 

4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

303 
 (Free (a,T), Free (b,U)) => 
12784  304 
if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

305 
 (Const (a,T), Const (b,U)) => 
12784  306 
if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

307 
 (Bound i, Bound j) => if i=j then instsp else raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

308 
 (Abs(_,T,t), Abs(_,U,u)) => 
12784  309 
mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u) 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

310 
 (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

311 
 (t, Abs(_,U,u)) => mtch instsp ((incr t)$(Bound 0), u) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

312 
 _ => raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

313 
in mtch end; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

314 

8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset

315 
fun first_order_match tsig = apfst Vartab.dest o fomatch tsig (Vartab.empty, []); 
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset

316 

4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

317 
(* Matching of higherorder patterns *) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

318 

8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

319 
fun match_bind(itms,binders,ixn,is,t) = 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

320 
let val js = loose_bnos t 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

321 
in if null is 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

322 
then if null js then (ixn,t)::itms else raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

323 
else if js subset_int is 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

324 
then let val t' = if downto0(is,length binders  1) then t 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

325 
else mapbnd (idx is) t 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

326 
in (ixn, mkabs(binders,is,t')) :: itms end 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

327 
else raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

328 
end; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

329 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

330 
fun match tsg (po as (pat,obj)) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

331 
let 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

332 
(* Pre: pat and obj have same type *) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

333 
fun mtch binders (env as (iTs,itms),(pat,obj)) = 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

334 
case pat of 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

335 
Abs(ns,Ts,ts) => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

336 
(case obj of 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

337 
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt)) 
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset

338 
 _ => let val Tt = typ_subst_TVars_Vartab iTs Ts 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

339 
in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

340 
 _ => (case obj of 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

341 
Abs(nt,Tt,tt) => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

342 
mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt)) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

343 
 _ => cases(binders,env,pat,obj)) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

344 

4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

345 
and cases(binders,env as (iTs,itms),pat,obj) = 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

346 
let val (ph,pargs) = strip_comb pat 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

347 
fun rigrig1(iTs,oargs) = 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

348 
foldl (mtch binders) ((iTs,itms), pargs~~oargs) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

349 
fun rigrig2((a,Ta),(b,Tb),oargs) = 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

350 
if a<> b then raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

351 
else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

352 
in case ph of 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

353 
Var(ixn,_) => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

354 
let val is = ints_of pargs 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

355 
in case assoc_string_int(itms,ixn) of 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

356 
None => (iTs,match_bind(itms,binders,ixn,is,obj)) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

357 
 Some u => if obj aeconv (red u is []) then env 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

358 
else raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

359 
end 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

360 
 _ => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

361 
let val (oh,oargs) = strip_comb obj 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

362 
in case (ph,oh) of 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

363 
(Const c,Const d) => rigrig2(c,d,oargs) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

364 
 (Free f,Free g) => rigrig2(f,g,oargs) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

365 
 (Bound i,Bound j) => if i<>j then raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

366 
else rigrig1(iTs,oargs) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

367 
 (Abs _, _) => raise Pattern 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

368 
 (_, Abs _) => raise Pattern 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

369 
 _ => raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

370 
end 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

371 
end; 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

372 

4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

373 
val pT = fastype_of pat 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

374 
and oT = fastype_of obj 
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset

375 
val iTs = typ_match tsg (Vartab.empty, (pT,oT)) 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

376 
val insts2 = (iTs,[]) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

377 

8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset

378 
in apfst Vartab.dest (mtch [] (insts2, po) 
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset

379 
handle Pattern => fomatch tsg insts2 po) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

380 
end; 
0  381 

382 
(*Predicate: does the pattern match the object?*) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

383 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  384 

4667
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

385 
(* Does pat match a subterm of obj? *) 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

386 
fun matches_subterm tsig (pat,obj) = 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

387 
let fun msub(bounds,obj) = matches tsig (pat,obj) orelse 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

388 
case obj of 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

389 
Abs(x,T,t) => let val y = variant bounds x 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

390 
val f = Free(":" ^ y,T) 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

391 
in msub(x::bounds,subst_bound(f,t)) end 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

392 
 s$t => msub(bounds,s) orelse msub(bounds,t) 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

393 
 _ => false 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

394 
in msub([],obj) end; 
6328d427a339
Tried to reorganize rewriter a little. More to be done.
nipkow
parents:
2792
diff
changeset

395 

4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

396 
fun first_order(Abs(_,_,t)) = first_order t 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

397 
 first_order(t $ u) = first_order t andalso first_order u andalso 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

398 
not(is_Var t) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

399 
 first_order _ = true; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

400 

8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

401 
fun pattern(Abs(_,_,t)) = pattern t 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

402 
 pattern(t) = let val (head,args) = strip_comb t 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

403 
in if is_Var head 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

404 
then let val _ = ints_of args in true end 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

405 
handle Pattern => false 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

406 
else forall pattern args 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

407 
end; 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

408 

12784  409 

410 
(* rewriting  simple but fast *) 

411 

412 
fun rewrite_term tsig rules tm = 

413 
let 

12797  414 
val rhs_names = 
415 
foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []); 

416 
fun variant_absfree (x, T, t) = 

417 
let 

418 
val x' = variant (add_term_free_names (t, rhs_names)) x; 

419 
val t' = subst_bound (Free (x', T), t); 

420 
in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end; 

421 

12784  422 
fun match_rew tm (tm1, tm2) = 
423 
Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None; 

424 
fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body)) 

425 
 rew tm = get_first (match_rew tm) rules; 

426 

427 
fun rew0 (tm as Abs (_, _, tm' $ Bound 0)) = 

428 
if loose_bvar1 (tm', 0) then rew tm 

429 
else 

430 
let val tm'' = incr_boundvars ~1 tm' 

431 
in Some (if_none (rew tm'') tm'') end 

432 
 rew0 tm = rew tm; 

433 

434 
fun rew1 tm = (case rew2 tm of 

435 
Some tm1 => (case rew0 tm1 of 

436 
Some tm2 => Some (if_none (rew1 tm2) tm2) 

437 
 None => Some tm1) 

438 
 None => (case rew0 tm of 

439 
Some tm1 => Some (if_none (rew1 tm1) tm1) 

440 
 None => None)) 

441 

442 
and rew2 (tm1 $ tm2) = (case tm1 of 

443 
Abs (_, _, body) => 

444 
let val tm' = subst_bound (tm2, body) 

445 
in Some (if_none (rew2 tm') tm') end 

446 
 _ => (case rew1 tm1 of 

447 
Some tm1' => (case rew1 tm2 of 

448 
Some tm2' => Some (tm1' $ tm2') 

449 
 None => Some (tm1' $ tm2)) 

450 
 None => (case rew1 tm2 of 

451 
Some tm2' => Some (tm1 $ tm2') 

452 
 None => None))) 

12797  453 
 rew2 (Abs (x, T, tm)) = 
454 
let val (abs, tm') = variant_absfree (x, T, tm) in 

455 
(case rew1 tm' of 

456 
Some tm'' => Some (abs tm'') 

457 
 None => None) 

458 
end 

12784  459 
 rew2 _ = None 
460 

12797  461 
in if_none (timeap_msg "FIXME: rewrite_term" rew1 tm) tm end; 
12784  462 

0  463 
end; 