author  nipkow 
Wed, 12 Apr 1995 13:53:34 +0200  
changeset 1029  27808dabf4af 
parent 678  6151b7f3b606 
child 1435  aefcd255ed4a 
permissions  rwrr 
0  1 
(* Title: pattern 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow and Christine Heinzelmann, TU Muenchen 

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 

15 
signature PATTERN = 

16 
sig 

17 
type type_sig 

18 
type sg 

19 
type env 

20 
val eta_contract: term > term 

21 
val match: type_sig > term * term 

22 
> (indexname*typ)list * (indexname*term)list 

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

23 
val matches: type_sig > term * term > bool 
0  24 
val unify: sg * env * (term * term)list > env 
25 
exception Unif 

26 
exception MATCH 

27 
exception Pattern 

28 
end; 

29 

30 
functor PatternFun(structure Sign:SIGN and Envir:ENVIR): PATTERN = 

31 
struct 

32 

33 
structure Type = Sign.Type; 

34 

35 
type type_sig = Type.type_sig 

36 
type sg = Sign.sg 

37 
type env = Envir.env 

38 

39 
exception Unif; 

40 
exception Pattern; 

41 

42 
fun occurs(F,t,env) = 

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

44 
Some(t) => occ t 

45 
 None => F=G) 

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

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

48 
 occ _ = false 

49 
in occ t end; 

50 

51 

52 
fun mapbnd f = 

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

54 
 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

55 
 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

56 
 mpb _ atom = atom 
0  57 
in mpb 0 end; 
58 

59 
fun idx [] j = ~10000 

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

61 

62 
val nth_type = snd o nth_elem; 

63 

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

65 

66 
fun mkabs (binders,is,t) = 

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

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

69 
 mk [] = t 

70 
in mk is end; 

71 

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

73 

74 
fun ints_of [] = [] 

75 
 ints_of (Bound i ::bs) = 

76 
let val is = ints_of bs 

77 
in if i mem is then raise Pattern else i::is end 

78 
 ints_of _ = raise Pattern; 

79 

80 

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

82 
 app (s,[]) = s; 

83 

84 
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

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

86 
 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

87 

0  88 

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

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

91 
 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

92 
 split_type _ = error("split_type"); 
0  93 

94 
fun type_of_G (T,n,is) = 

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

96 

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

98 

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

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

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

102 

103 

104 
fun devar env t = case strip_comb t of 

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

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

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

108 
 None => t) 

109 
 _ => t; 

110 

111 

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

113 
fun mk_proj_list is = 

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

115 
 mk([],_) = [] 

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

117 

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

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

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

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

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

123 
 t => (case strip_comb t of 

124 
(c as Const _,ts) => 

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

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

127 
 (f as Free _,ts) => 

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

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

130 
 (Bound(i),ts) => 

131 
let val j = trans d i 

132 
in if j < 0 then raise Unif 

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

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

135 
end 

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

137 
let val js = ints_of ts; 

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

139 
val ks = mk_proj_list js'; 

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

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

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

143 
val env'' = 

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

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

146 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

154 
end; 

155 

156 

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

158 
fun mk_ff_list(is,js) = 

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

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

161 
else mk(is,js,k1) 

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

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

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

166 
if is=js then env 

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

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

169 

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

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

172 
if js subset is 

173 
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js)) 

174 
in Envir.update((F,t),env) end 

175 
else let val ks = is inter js 

176 
val Hty = type_of_G(Fty,length is,map (idx is) ks) 

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

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

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

180 
end; 

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

182 

183 
val tsgr = ref(Type.tsig0); 

184 

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

186 
if T=U then env 

187 
else let val iTs' = Type.unify (!tsgr) ((U,T),iTs) 

188 
in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'} end 

189 
handle Type.TUNIFY => raise Unif; 

190 

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

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

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

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

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

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

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

198 

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

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

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

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

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

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

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

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

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

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

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

210 
 _ => raise Unif 

211 

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

213 
if a<>b then raise Unif 

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

215 

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

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

218 

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

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

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

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

223 

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

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

226 

227 

228 
(*Perform etacontractions upon a term*) 

229 
fun eta_contract (Abs(a,T,body)) = 

230 
(case eta_contract body of 

231 
body' as (f $ Bound i) => 

232 
if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f 

233 
else Abs(a,T,body') 

234 
 body' => Abs(a,T,body')) 

235 
 eta_contract(f$t) = eta_contract f $ eta_contract t 

236 
 eta_contract t = t; 

237 

238 

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

239 
(* Pattern matching *) 
0  240 
exception MATCH; 
241 

242 
(*Firstorder matching; term_match tsig (pattern, object) 

243 
returns a (tyvar,typ)list and (var,term)list. 

244 
The pattern and object may have variables in common. 

245 
Instantiation does not affect the object, so matching ?a with ?a+1 works. 

246 
A Const does not match a Free of the same name! 

247 
Does not notice etaequality, thus f does not match %(x)f(x) *) 

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

248 
fun fomatch tsig (pat,obj) = 
0  249 
let fun typ_match args = (Type.typ_match tsig args) 
250 
handle Type.TYPE_MATCH => raise MATCH; 

251 
fun mtch (tyinsts,insts) = fn 

252 
(Var(ixn,T), t) => 

1029
27808dabf4af
term.ML: add_loose_bnos now returns a list w/o duplicates.
nipkow
parents:
678
diff
changeset

253 
if loose_bvar(t,0) then raise MATCH 
27808dabf4af
term.ML: add_loose_bnos now returns a list w/o duplicates.
nipkow
parents:
678
diff
changeset

254 
else (case assoc(insts,ixn) of 
63  255 
None => (typ_match (tyinsts, (T, fastype_of t)), 
0  256 
(ixn,t)::insts) 
1029
27808dabf4af
term.ML: add_loose_bnos now returns a list w/o duplicates.
nipkow
parents:
678
diff
changeset

257 
 Some u => if t aconv u then (tyinsts,insts) else raise MATCH) 
0  258 
 (Free (a,T), Free (b,U)) => 
259 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH 

260 
 (Const (a,T), Const (b,U)) => 

261 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH 

262 
 (Bound i, Bound j) => 

263 
if i=j then (tyinsts,insts) else raise MATCH 

264 
 (Abs(_,T,t), Abs(_,U,u)) => 

265 
mtch (typ_match (tyinsts,(T,U)),insts) (t,u) 

266 
 (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u) 

267 
 _ => raise MATCH 

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

268 
in mtch([],[]) (eta_contract pat,eta_contract obj) end; 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

269 

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

270 

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

271 
fun match_bind(itms,binders,ixn,is,t) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

272 
let val js = loose_bnos t 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

273 
in if null is 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

274 
then if null js then (ixn,t)::itms else raise MATCH 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

275 
else if js subset is 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

276 
then let val t' = if downto0(is,length binders  1) then t 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

277 
else mapbnd (idx is) t 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

278 
in (ixn, mkabs(binders,is,t')) :: itms end 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

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

281 

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

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

283 
Note that Consts and Vars may have more than one type.*) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

285 
fun (Const(a,T)) aeconv (Const(b,U)) = a=b andalso T=U 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

286 
 (Free(a,T)) aeconv (Free(b,U)) = a=b andalso T=U 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

287 
 (Var(v,T)) aeconv (Var(w,U)) = v=w andalso T=U 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

288 
 (Bound i) aeconv (Bound j) = i=j 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

289 
 (Abs(_,T,t)) aeconv (Abs(_,U,u)) = (t aeconv u) andalso T=U 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

290 
 (Abs(_,T,t)) aeconv u = t aeconv ((incr u)$Bound(0)) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

291 
 t aeconv (Abs(_,U,u)) = ((incr t)$Bound(0)) aeconv u 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

292 
 (f$t) aeconv (g$u) = (f aeconv g) andalso (t aeconv u) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

293 
 _ aeconv _ = false; 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

294 

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

295 

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

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

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

298 

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

299 
fun typ_match args = Type.typ_match tsg args 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

300 
handle Type.TYPE_MATCH => raise MATCH; 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

301 

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

302 
(* Pre: pat and obj have same type *) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

303 
fun mtch binders (env as (iTs,itms),(pat,obj)) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

305 
Abs(ns,Ts,ts) => 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

307 
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt)) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

308 
 _ => let val Tt = typ_subst_TVars iTs Ts 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

309 
in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

310 
 _ => (case obj of 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

311 
Abs(nt,Tt,tt) => 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

312 
mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt)) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

314 

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

315 
and cases(binders,env as (iTs,itms),pat,obj) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

316 
let val (ph,pargs) = strip_comb pat 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

317 
fun rigrig1(iTs,oargs) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

318 
foldl (mtch binders) ((iTs,itms), pargs~~oargs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

319 
fun rigrig2((a,Ta),(b,Tb),oargs) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

320 
if a<> b then raise MATCH 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

321 
else rigrig1(typ_match(iTs,(Ta,Tb)), oargs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

323 
Var(ixn,_) => 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

324 
let val is = ints_of pargs 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

325 
in case assoc(itms,ixn) of 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

326 
None => (iTs,match_bind(itms,binders,ixn,is,obj)) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

327 
 Some u => if obj aeconv (red u is []) then env 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

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

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

331 
let val (oh,oargs) = strip_comb obj 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

332 
in case (ph,oh) of 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

333 
(Const c,Const d) => rigrig2(c,d,oargs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

334 
 (Free f,Free g) => rigrig2(f,g,oargs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

335 
 (Bound i,Bound j) => if i<>j then raise MATCH 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

336 
else rigrig1(iTs,oargs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

337 
 (Abs _, _) => raise Pattern 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

338 
 (_, Abs _) => raise Pattern 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

339 
 _ => raise MATCH 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

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

342 

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

343 
val pT = fastype_of pat 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

344 
and oT = fastype_of obj 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

345 
val iTs = typ_match ([],(pT,oT)) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

346 

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

347 
in mtch [] ((iTs,[]), po) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

349 
end; 
0  350 

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

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

352 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  353 

354 
end; 