author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 4820  8f6dbbd8d497 
child 6539  2e7d2fba9f6c 
permissions  rwrr 
1460  1 
(* Title: pattern 
0  2 
ID: $Id$ 
1460  3 
Author: Tobias Nipkow and Christine Heinzelmann, TU Muenchen 
0  4 
Copyright 1993 TU Muenchen 
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 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

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

26 
> (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

27 
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

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

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

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

31 
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

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

33 
val pattern : term > bool 
0  34 
exception Unif 
35 
exception MATCH 

36 
exception Pattern 

1501  37 
end; 
0  38 

1501  39 
structure Pattern : PATTERN = 
0  40 
struct 
41 

42 
type type_sig = Type.type_sig 

43 
type sg = Sign.sg 

44 
type env = Envir.env 

45 

46 
exception Unif; 

47 
exception Pattern; 

48 

49 
fun occurs(F,t,env) = 

50 
let fun occ(Var(G,_)) = (case Envir.lookup(env,G) of 

51 
Some(t) => occ t 

52 
 None => F=G) 

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

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

55 
 occ _ = false 

56 
in occ t end; 

57 

58 

59 
fun mapbnd f = 

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

61 
 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

62 
 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

63 
 mpb _ atom = atom 
0  64 
in mpb 0 end; 
65 

66 
fun idx [] j = ~10000 

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

68 

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

70 

71 
fun mkabs (binders,is,t) = 

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

73 
in Abs(x,T,mk is) end 

74 
 mk [] = t 

75 
in mk is end; 

76 

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

78 

79 
fun ints_of [] = [] 

80 
 ints_of (Bound i ::bs) = 

81 
let val is = ints_of bs 

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

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

85 

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

87 
 app (s,[]) = s; 

88 

89 
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

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

91 
 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

92 

0  93 

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

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

96 
 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

97 
 split_type _ = error("split_type"); 
0  98 

99 
fun type_of_G (T,n,is) = 

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

101 

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

103 

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

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

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

107 

108 

109 
fun devar env t = case strip_comb t of 

110 
(Var(F,_),ys) => 

111 
(case Envir.lookup(env,F) of 

112 
Some(t) => devar env (red t (ints_of ys) []) 

113 
 None => t) 

114 
 _ => t; 

115 

116 

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

118 
fun mk_proj_list is = 

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

120 
 mk([],_) = [] 

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

122 

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

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

125 
fun pr(s,env,d,binders) = (case devar env s of 

126 
Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders)) 

127 
in (Abs(a,T,t'),env') end 

128 
 t => (case strip_comb t of 

129 
(c as Const _,ts) => 

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

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

132 
 (f as Free _,ts) => 

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

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

135 
 (Bound(i),ts) => 

136 
let val j = trans d i 

137 
in if j < 0 then raise Unif 

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

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

140 
end 

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

142 
let val js = ints_of ts; 

143 
val js' = map (trans d) js; 

144 
val ks = mk_proj_list js'; 

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

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

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

148 
val env'' = 

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

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

151 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

159 
end; 

160 

161 

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

163 
fun mk_ff_list(is,js) = 

164 
let fun mk([],[],_) = [] 

165 
 mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k1) 

166 
else mk(is,js,k1) 

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

167 
 mk _ = error"mk_ff_list" 
0  168 
in mk(is,js,length is1) end; 
169 

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

171 
if is=js then env 

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

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

174 

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

176 
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

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

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

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

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

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

185 
end; 

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

187 

188 
val tsgr = ref(Type.tsig0); 

189 

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

191 
if T=U then env 

1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1029
diff
changeset

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

193 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
0  194 
handle Type.TUNIFY => raise Unif; 
195 

196 
fun unif binders (env,(s,t)) = case (devar env s,devar env t) of 

197 
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => 

198 
let val name = if ns = "" then nt else ns 

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

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

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

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

203 

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

205 
((Var(F,Fty),ss),(Var(G,Gty),ts)) => 

206 
if F = G then flexflex1(env,binders,F,Fty,ints_of ss,ints_of ts) 

207 
else flexflex2(env,binders,F,Fty,ints_of ss,G,Gty,ints_of ts) 

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

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

210 
 ((Const c,ss),(Const d,ts)) => rigidrigid(env,binders,c,d,ss,ts) 

211 
 ((Free(f),ss),(Free(g),ts)) => rigidrigid(env,binders,f,g,ss,ts) 

212 
 ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 

213 
 ((Abs(_),_),_) => raise Pattern 

214 
 (_,(Abs(_),_)) => raise Pattern 

215 
 _ => raise Unif 

216 

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

218 
if a<>b then raise Unif 

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

220 

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

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

223 

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

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

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

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

228 

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

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

231 

232 

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

233 
(*Etacontract a term (fully)*) 
2792  234 

235 
(* copying: *) 

0  236 
fun eta_contract (Abs(a,T,body)) = 
2616  237 
(case eta_contract body of 
238 
body' as (f $ Bound 0) => 

2792  239 
if loose_bvar1(f,0) then Abs(a,T,body') 
2616  240 
else incr_boundvars ~1 f 
0  241 
 body' => Abs(a,T,body')) 
242 
 eta_contract(f$t) = eta_contract f $ eta_contract t 

243 
 eta_contract t = t; 

244 

245 

2792  246 
(* sharing: 
247 
local 

248 

249 
fun eta(Abs(x,T,t)) = 

250 
(case eta t of 

251 
None => (case t of 

252 
f $ Bound 0 => if loose_bvar1(f,0) 

253 
then None 

254 
else Some(incr_boundvars ~1 f) 

255 
 _ => None) 

256 
 Some(t') => (case t' of 

257 
f $ Bound 0 => if loose_bvar1(f,0) 

258 
then Some(Abs(x,T,t')) 

259 
else Some(incr_boundvars ~1 f) 

260 
 _ => Some(Abs(x,T,t')))) 

261 
 eta(s$t) = (case (eta s,eta t) of 

262 
(None, None) => None 

263 
 (None, Some t') => Some(s $ t') 

264 
 (Some s',None) => Some(s' $ t) 

265 
 (Some s',Some t') => Some(s' $ t')) 

266 
 eta _ = None 

267 

268 
in 

269 

270 
fun eta_contract t = case eta t of None => t  Some(t') => t'; 

271 

272 
end; *) 

273 

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

274 
(*Etacontract a term from outside: just enough to reduce it to an atom*) 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

276 
(case eta_contract2 body of 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

277 
body' as (f $ Bound 0) => 
2792  278 
if loose_bvar1(f,0) then Abs(a,T,body') 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

279 
else eta_contract_atom (incr_boundvars ~1 f) 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

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

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

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

284 

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

285 

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

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

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

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

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

292 
 aconv_aux (Bound i, Bound j) = i=j 

293 
 aconv_aux (Abs(_,T,t), Abs(_,U,u)) = (t aeconv u) andalso T=U 

294 
 aconv_aux (f$t, g$u) = (f aeconv g) andalso (t aeconv u) 

295 
 aconv_aux _ = false; 

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

296 

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

297 

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

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

299 

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

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

301 

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

302 
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

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

304 

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

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

306 
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

307 
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

308 
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

309 
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

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

311 
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

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

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

314 
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

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

316 
if loose_bvar(t,0) then raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

318 
None => (typ_match tsig (tyinsts, (T, fastype_of t)), 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

319 
(ixn,t)::insts) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

320 
 Some u => if t aeconv u then instsp else raise MATCH) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

321 
 (Free (a,T), Free (b,U)) => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

323 
 (Const (a,T), Const (b,U)) => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

325 
 (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

326 
 (Abs(_,T,t), Abs(_,U,u)) => 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

327 
mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

328 
 (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

329 
 (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

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

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

332 

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

333 
fun first_order_match tsig = fomatch tsig ([],[]); 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

334 

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

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

336 

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

337 
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

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

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

340 
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

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

342 
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

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

344 
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

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

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

347 

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

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

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

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

351 
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

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

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

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

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

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

357 
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

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

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

360 
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

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

362 

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

363 
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

364 
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

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

366 
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

367 
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

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

369 
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

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

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

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

373 
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

374 
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

375 
 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

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

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

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

379 
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

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

381 
(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

382 
 (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

383 
 (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

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

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

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

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

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

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

390 

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

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

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

393 
val iTs = typ_match tsg ([],(pT,oT)) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

395 

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

396 
in mtch [] (insts2, po) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

398 
end; 
0  399 

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

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

401 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  402 

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

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

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

405 
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

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

407 
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

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

409 
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

410 
 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

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

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

413 

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

414 
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

415 
 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

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

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

418 

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

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

420 
 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

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

422 
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

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

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

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

426 

0  427 
end; 