author  paulson 
Tue, 26 Nov 1996 16:15:50 +0100  
changeset 2227  18e993700540 
parent 1576  af8f43f742a0 
child 2616  704b6c7432cf 
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 

15 
signature PATTERN = 

1501  16 
sig 
0  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 

1501  28 
end; 
0  29 

1501  30 
structure Pattern : PATTERN = 
0  31 
struct 
32 

33 
type type_sig = Type.type_sig 

34 
type sg = Sign.sg 

35 
type env = Envir.env 

36 

37 
exception Unif; 

38 
exception Pattern; 

39 

40 
fun occurs(F,t,env) = 

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

42 
Some(t) => occ t 

43 
 None => F=G) 

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

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

46 
 occ _ = false 

47 
in occ t end; 

48 

49 

50 
fun mapbnd f = 

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

52 
 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

53 
 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

54 
 mpb _ atom = atom 
0  55 
in mpb 0 end; 
56 

57 
fun idx [] j = ~10000 

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

59 

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

61 

62 
fun mkabs (binders,is,t) = 

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

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

65 
 mk [] = t 

66 
in mk is end; 

67 

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

69 

70 
fun ints_of [] = [] 

71 
 ints_of (Bound i ::bs) = 

72 
let val is = ints_of bs 

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

73 
in if i mem_int is then raise Pattern else i::is end 
0  74 
 ints_of _ = raise Pattern; 
75 

76 

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

78 
 app (s,[]) = s; 

79 

80 
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

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

82 
 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

83 

0  84 

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

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

87 
 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

88 
 split_type _ = error("split_type"); 
0  89 

90 
fun type_of_G (T,n,is) = 

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

92 

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

94 

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

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

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

98 

99 

100 
fun devar env t = case strip_comb t of 

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

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

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

104 
 None => t) 

105 
 _ => t; 

106 

107 

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

109 
fun mk_proj_list is = 

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

111 
 mk([],_) = [] 

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

113 

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

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

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

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

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

119 
 t => (case strip_comb t of 

120 
(c as Const _,ts) => 

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

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

123 
 (f as Free _,ts) => 

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

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

126 
 (Bound(i),ts) => 

127 
let val j = trans d i 

128 
in if j < 0 then raise Unif 

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

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

131 
end 

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

133 
let val js = ints_of ts; 

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

135 
val ks = mk_proj_list js'; 

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

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

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

139 
val env'' = 

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

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

142 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

150 
end; 

151 

152 

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

154 
fun mk_ff_list(is,js) = 

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

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

157 
else mk(is,js,k1) 

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

158 
 mk _ = error"mk_ff_list" 
0  159 
in mk(is,js,length is1) end; 
160 

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

162 
if is=js then env 

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

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

165 

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

167 
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

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

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

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

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

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

176 
end; 

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

178 

179 
val tsgr = ref(Type.tsig0); 

180 

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

182 
if T=U then env 

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

183 
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

184 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
0  185 
handle Type.TUNIFY => raise Unif; 
186 

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

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

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

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

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

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

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

194 

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

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

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

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

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

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

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

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

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

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

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

206 
 _ => raise Unif 

207 

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

209 
if a<>b then raise Unif 

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

211 

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

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

214 

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

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

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

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

219 

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

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

222 

223 

224 
(*Perform etacontractions upon a term*) 

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

226 
(case eta_contract body of 

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

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

228 
if i=0 andalso not (0 mem_int loose_bnos f) then incr_boundvars ~1 f 
1460  229 
else Abs(a,T,body') 
0  230 
 body' => Abs(a,T,body')) 
231 
 eta_contract(f$t) = eta_contract f $ eta_contract t 

232 
 eta_contract t = t; 

233 

234 

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

235 
(* Pattern matching *) 
0  236 
exception MATCH; 
237 

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

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

240 
The pattern and object may have variables in common. 

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

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

243 
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

244 
fun fomatch tsig (pat,obj) = 
0  245 
let fun typ_match args = (Type.typ_match tsig args) 
1460  246 
handle Type.TYPE_MATCH => raise MATCH; 
0  247 
fun mtch (tyinsts,insts) = fn 
1460  248 
(Var(ixn,T), t) => 
249 
if loose_bvar(t,0) then raise MATCH 

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

250 
else (case assoc_string_int(insts,ixn) of 
1460  251 
None => (typ_match (tyinsts, (T, fastype_of t)), 
252 
(ixn,t)::insts) 

253 
 Some u => if t aconv u then (tyinsts,insts) else raise MATCH) 

0  254 
 (Free (a,T), Free (b,U)) => 
1460  255 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH 
0  256 
 (Const (a,T), Const (b,U)) => 
1460  257 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH 
0  258 
 (Bound i, Bound j) => 
259 
if i=j then (tyinsts,insts) else raise MATCH 

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

1460  261 
mtch (typ_match (tyinsts,(T,U)),insts) (t,u) 
0  262 
 (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u) 
263 
 _ => raise MATCH 

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

264 
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

265 

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

266 

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

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

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

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

270 
then if null js then (ixn,t)::itms else raise MATCH 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1501
diff
changeset

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

272 
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

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

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

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

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

277 

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

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

279 
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

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

281 
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

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

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

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

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

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

287 
 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

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

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

290 

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

291 

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

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

293 
let 
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 
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

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

297 

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

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

299 
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

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

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

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

303 
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

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

305 
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

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) => 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

308 
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

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

310 

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

311 
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

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

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

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

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

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

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

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

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

320 
let val is = ints_of pargs 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1501
diff
changeset

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

322 
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

323 
 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

338 

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

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

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

341 
val iTs = typ_match ([],(pT,oT)) 
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 
in mtch [] ((iTs,[]), po) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

345 
end; 
0  346 

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

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

348 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  349 

350 
end; 