author  paulson 
Fri, 07 Mar 1997 10:23:54 +0100  
changeset 2751  673c4eefd2e1 
parent 2725  9453616d4b80 
child 2792  6c17c5ec3d8b 
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 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

28 
val unify : sg * env * (term * term)list > env 
0  29 
exception Unif 
30 
exception MATCH 

31 
exception Pattern 

1501  32 
end; 
0  33 

1501  34 
structure Pattern : PATTERN = 
0  35 
struct 
36 

37 
type type_sig = Type.type_sig 

38 
type sg = Sign.sg 

39 
type env = Envir.env 

40 

41 
exception Unif; 

42 
exception Pattern; 

43 

44 
fun occurs(F,t,env) = 

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

46 
Some(t) => occ t 

47 
 None => F=G) 

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

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

50 
 occ _ = false 

51 
in occ t end; 

52 

53 

54 
fun mapbnd f = 

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

56 
 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

57 
 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

58 
 mpb _ atom = atom 
0  59 
in mpb 0 end; 
60 

61 
fun idx [] j = ~10000 

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

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 

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

77 
in if i mem_int is then raise Pattern else i::is end 
0  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) = 

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

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

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

175 
else let val ks = is inter_int js 
0  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 

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

187 
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

188 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
0  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 

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

228 
(*Etacontract a term (fully)*) 
0  229 
fun eta_contract (Abs(a,T,body)) = 
2616  230 
(case eta_contract body of 
231 
body' as (f $ Bound 0) => 

232 
if (0 mem_int loose_bnos f) then Abs(a,T,body') 

233 
else incr_boundvars ~1 f 

0  234 
 body' => Abs(a,T,body')) 
235 
 eta_contract(f$t) = eta_contract f $ eta_contract t 

236 
 eta_contract t = t; 

237 

238 

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

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

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

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

242 
body' as (f $ Bound 0) => 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

243 
if (0 mem_int loose_bnos f) then Abs(a,T,body') 
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

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

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

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

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

249 

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

250 

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

251 
(* Pattern matching *) 
0  252 
exception MATCH; 
253 

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

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

256 
The pattern and object may have variables in common. 

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

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

258 
A Const does not match a Free of the same name! *) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

259 
fun fomatch tsig (pat,obj) = 
0  260 
let fun typ_match args = (Type.typ_match tsig args) 
1460  261 
handle Type.TYPE_MATCH => raise MATCH; 
0  262 
fun mtch (tyinsts,insts) = fn 
1460  263 
(Var(ixn,T), t) => 
264 
if loose_bvar(t,0) then raise MATCH 

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

265 
else (case assoc_string_int(insts,ixn) of 
1460  266 
None => (typ_match (tyinsts, (T, fastype_of t)), 
267 
(ixn,t)::insts) 

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

0  269 
 (Free (a,T), Free (b,U)) => 
1460  270 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH 
0  271 
 (Const (a,T), Const (b,U)) => 
1460  272 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH 
0  273 
 (Bound i, Bound j) => 
274 
if i=j then (tyinsts,insts) else raise MATCH 

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

1460  276 
mtch (typ_match (tyinsts,(T,U)),insts) (t,u) 
0  277 
 (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u) 
278 
 _ => raise MATCH 

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

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

280 

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 
fun match_bind(itms,binders,ixn,is,t) = 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

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

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

285 
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

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

287 
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

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

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

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

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

292 

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

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

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

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

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

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

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

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

302 
 aconv_aux _ = false; 

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

303 

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

304 

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

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

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

307 

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

308 
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

309 
handle Type.TYPE_MATCH => raise MATCH; 
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 
(* Pre: pat and obj have same type *) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

312 
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

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

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

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

316 
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

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

318 
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

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

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

321 
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

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

323 

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

324 
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

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

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

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

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

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

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

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

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

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

334 
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

335 
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

336 
 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

351 

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

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

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

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

355 

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

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

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

358 
end; 
0  359 

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

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

361 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  362 

363 
end; 