author  berghofe 
Fri, 31 May 2002 18:47:11 +0200  
changeset 13195  98975cc13d28 
parent 12980  8f717cbd4e44 
child 13642  a3d97348ceb6 
permissions  rwrr 
12784  1 
(* Title: Pure/pattern.ML 
0  2 
ID: $Id$ 
12784  3 
Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

0  5 

6 
Unification of HigherOrder Patterns. 

7 

8 
See also: 

9 
Tobias Nipkow. Functional Unification of HigherOrder Patterns. 

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

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

11 

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

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

2751  15 
infix aeconv; 
16 

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

21 
type env 

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

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

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

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

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

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

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

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

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

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

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

34 
val pattern : term > bool 
13195  35 
val rewrite_term : type_sig > (term * term) list > (term > term option) list 
36 
> term > term 

0  37 
exception Unif 
38 
exception MATCH 

39 
exception Pattern 

1501  40 
end; 
0  41 

1501  42 
structure Pattern : PATTERN = 
0  43 
struct 
44 

45 
type type_sig = Type.type_sig 

46 
type sg = Sign.sg 

47 
type env = Envir.env 

48 

49 
exception Unif; 

50 
exception Pattern; 

51 

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

55 
 None => F=G) 

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

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

58 
 occ _ = false 

59 
in occ t end; 

60 

61 

62 
fun mapbnd f = 

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

64 
 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

65 
 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

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

69 
fun idx [] j = ~10000 

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

71 

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

73 

74 
fun mkabs (binders,is,t) = 

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

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

79 

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

81 

82 
fun ints_of [] = [] 

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

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

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

0  90 

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

92 
 app (s,[]) = s; 

93 

94 
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

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

96 
 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

97 

0  98 

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

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

101 
 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

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

104 
fun type_of_G (T,n,is) = 

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

106 

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

108 

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

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

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

112 

113 

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

115 
fun mk_proj_list is = 

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

117 
 mk([],_) = [] 

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

119 

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

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

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

125 
 t => (case strip_comb t of 

126 
(c as Const _,ts) => 

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

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

129 
 (f as Free _,ts) => 

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

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

132 
 (Bound(i),ts) => 

133 
let val j = trans d i 

134 
in if j < 0 then raise Unif 

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

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

137 
end 

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

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

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

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

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

145 
val env'' = 

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

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

148 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

156 
end; 

157 

158 

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

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

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

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

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

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

168 
if is=js then env 

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

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

171 

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

173 
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

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

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

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

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

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

182 
end; 

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

184 

185 
val tsgr = ref(Type.tsig0); 

186 

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

188 
if T=U then env 

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

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

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

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

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

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

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

200 

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

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

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

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

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

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

212 
 _ => raise Unif 

213 

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

215 
if a<>b then raise Unif 

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

217 

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

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

220 

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

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

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

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

225 

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

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

228 

229 

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

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

12797  232 
fun eta_contract t = 
233 
let 

234 
exception SAME; 

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

236 
((case eta body of 

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

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

239 
else incr_boundvars ~1 f 

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

241 
(case body of 

242 
(f $ Bound 0) => 

243 
if loose_bvar1 (f, 0) then raise SAME 

244 
else incr_boundvars ~1 f 

245 
 _ => raise SAME)) 

246 
 eta (f $ t) = 

247 
(let val f' = eta f 

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

249 
 eta _ = raise SAME 

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

251 
in etah t end; 

0  252 

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

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

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

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

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

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

262 
else eta_contract_atom (incr_boundvars ~1 f) 

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

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

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

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

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

267 

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

268 

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

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

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

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

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

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

279 

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

280 

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

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

282 

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

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

284 

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

285 
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

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

287 

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

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

289 
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

290 
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

291 
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

292 
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

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

294 
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

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

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

297 
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

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

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

302 
(ixn,t)::insts) 

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

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

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

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

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

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

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

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

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

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

315 

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

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

317 

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

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

319 

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

320 
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

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

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

323 
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

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

325 
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

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

327 
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

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

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

330 

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

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

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

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

334 
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

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

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

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

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

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

340 
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

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

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

343 
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

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

345 

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

346 
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

347 
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

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

349 
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

350 
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

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

352 
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

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

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

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

356 
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

357 
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

358 
 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

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

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

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

362 
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

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

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

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

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

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

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

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

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

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

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

373 

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

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

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

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

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

378 

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

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

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

381 
end; 
0  382 

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

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

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

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

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

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

388 
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

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

390 
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

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

392 
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

393 
 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

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

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

396 

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

397 
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

398 
 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

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

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

401 

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

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

403 
 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

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

405 
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

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

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

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

409 

12784  410 

411 
(* rewriting  simple but fast *) 

412 

13195  413 
fun rewrite_term tsig rules procs tm = 
12784  414 
let 
13195  415 
val skel0 = Bound 0; 
416 

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

13195  419 

12797  420 
fun variant_absfree (x, T, t) = 
421 
let 

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

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

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

425 

12784  426 
fun match_rew tm (tm1, tm2) = 
13195  427 
let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 
428 
in Some (subst_vars (match tsig (tm1, tm)) rtm, rtm) 

429 
handle MATCH => None 

430 
end; 

12784  431 

13195  432 
fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body), skel0) 
433 
 rew tm = (case get_first (match_rew tm) rules of 

434 
None => apsome (rpair skel0) (get_first (fn p => p tm) procs) 

435 
 x => x); 

436 

437 
fun rew1 (Var _) _ = None 

438 
 rew1 skel tm = (case rew2 skel tm of 

12817
fcbb6ad5c790
rewrite_term: removed rew0, so no onthefly etacontraction;
wenzelm
parents:
12797
diff
changeset

439 
Some tm1 => (case rew tm1 of 
13195  440 
Some (tm2, skel') => Some (if_none (rew1 skel' tm2) tm2) 
12784  441 
 None => Some tm1) 
12817
fcbb6ad5c790
rewrite_term: removed rew0, so no onthefly etacontraction;
wenzelm
parents:
12797
diff
changeset

442 
 None => (case rew tm of 
13195  443 
Some (tm1, skel') => Some (if_none (rew1 skel' tm1) tm1) 
12784  444 
 None => None)) 
445 

13195  446 
and rew2 skel (tm1 $ tm2) = (case tm1 of 
12784  447 
Abs (_, _, body) => 
448 
let val tm' = subst_bound (tm2, body) 

13195  449 
in Some (if_none (rew2 skel0 tm') tm') end 
450 
 _ => 

451 
let val (skel1, skel2) = (case skel of 

452 
skel1 $ skel2 => (skel1, skel2) 

453 
 _ => (skel0, skel0)) 

454 
in case rew1 skel1 tm1 of 

455 
Some tm1' => (case rew1 skel2 tm2 of 

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

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

458 
 None => (case rew1 skel2 tm2 of 

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

460 
 None => None) 

461 
end) 

462 
 rew2 skel (Abs (x, T, tm)) = 

463 
let 

464 
val (abs, tm') = variant_absfree (x, T, tm); 

465 
val skel' = (case skel of Abs (_, _, skel') => skel'  _ => skel0) 

466 
in case rew1 skel' tm' of 

12797  467 
Some tm'' => Some (abs tm'') 
13195  468 
 None => None 
12797  469 
end 
13195  470 
 rew2 _ _ = None 
12784  471 

13195  472 
in if_none (rew1 skel0 tm) tm end; 
12784  473 

0  474 
end; 