author  wenzelm 
Thu, 22 Apr 2004 10:52:32 +0200  
changeset 14643  130076a81b84 
parent 13998  75a399c2781f 
child 14787  724ce6e574e3 
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 

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

24 
val eta_contract : term > term 
13998  25 
val eta_long : typ list > term > term 
12781  26 
val beta_eta_contract : term > term 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

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

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

30 
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

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

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

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

34 
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

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

36 
val pattern : term > bool 
13195  37 
val rewrite_term : type_sig > (term * term) list > (term > term option) list 
38 
> term > term 

0  39 
exception Unif 
40 
exception MATCH 

41 
exception Pattern 

1501  42 
end; 
0  43 

1501  44 
structure Pattern : PATTERN = 
0  45 
struct 
46 

47 
type type_sig = Type.type_sig 

48 
type sg = Sign.sg 

49 
type env = Envir.env 

50 

51 
exception Unif; 

52 
exception Pattern; 

53 

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

54 
val trace_unify_fail = ref false; 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

55 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

56 
(* Only for communication between unification and error message printing *) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

57 
val sgr = ref Sign.pre_pure 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

58 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

59 
fun string_of_term env binders t = Sign.string_of_term (!sgr) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

60 
(Envir.norm_term env (subst_bounds(map Free binders,t))); 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

61 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

62 
fun bname binders i = fst(nth_elem(i,binders)); 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

63 
fun bnames binders is = space_implode " " (map (bname binders) is); 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

64 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

65 
fun typ_clash(tye,T,U) = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

66 
if !trace_unify_fail 
13645  67 
then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T) 
68 
and u = Sign.string_of_typ (!sgr) (Envir.norm_type tye U) 

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

69 
in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

70 
else () 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

71 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

72 
fun clash a b = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

73 
if !trace_unify_fail then tracing("Clash: " ^ a ^ " =/= " ^ b) else () 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

74 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

75 
fun boundVar binders i = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

76 
"bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")"; 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

77 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

78 
fun clashBB binders i j = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

79 
if !trace_unify_fail then clash (boundVar binders i) (boundVar binders j) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

80 
else () 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

81 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

82 
fun clashB binders i s = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

83 
if !trace_unify_fail then clash (boundVar binders i) s 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

84 
else () 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

85 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

86 
fun proj_fail(env,binders,F,is,t) = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

87 
if !trace_unify_fail 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

88 
then let val f = Syntax.string_of_vname F 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

89 
val xs = bnames binders is 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

90 
val u = string_of_term env binders t 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

91 
val ys = bnames binders (loose_bnos t \\ is) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

92 
in tracing("Cannot unify variable " ^ f ^ 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

93 
" (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^ 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

94 
"\nTerm contains additional bound variable(s) " ^ ys) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

95 
end 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

96 
else () 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

97 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

98 
fun ocheck_fail(F,t,binders,env) = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

99 
if !trace_unify_fail 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

100 
then let val f = Syntax.string_of_vname F 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

101 
val u = string_of_term env binders t 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

102 
in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^ 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

103 
"\nCannot unify!\n") 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

104 
end 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

105 
else () 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

106 

12784  107 
fun occurs(F,t,env) = 
0  108 
let fun occ(Var(G,_)) = (case Envir.lookup(env,G) of 
109 
Some(t) => occ t 

110 
 None => F=G) 

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

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

113 
 occ _ = false 

114 
in occ t end; 

115 

116 

117 
fun mapbnd f = 

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

119 
 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

120 
 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

121 
 mpb _ atom = atom 
0  122 
in mpb 0 end; 
123 

124 
fun idx [] j = ~10000 

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

126 

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

128 

129 
fun mkabs (binders,is,t) = 

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

12784  131 
in Abs(x,T,mk is) end 
0  132 
 mk [] = t 
133 
in mk is end; 

134 

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

136 

137 
fun ints_of [] = [] 

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

140 
in if i mem_int is then raise Pattern else i::is end 
0  141 
 ints_of _ = raise Pattern; 
142 

12232  143 
fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); 
144 

0  145 

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

147 
 app (s,[]) = s; 

148 

149 
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

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

151 
 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

152 

0  153 

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

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

156 
 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

157 
 split_type _ = error("split_type"); 
0  158 

13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

159 
fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) = 
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

160 
let val (Ts, U) = split_type (Envir.norm_type iTs T, n, []) 
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

161 
in map (at Ts) is > U end; 
0  162 

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

164 

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

13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

166 
let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js)) 
0  167 
in Envir.update((F,mkhnf(binders,is,G,js)),env') end; 
168 

169 

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

171 
fun mk_proj_list is = 

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

173 
 mk([],_) = [] 

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

175 

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

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

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

181 
 t => (case strip_comb t of 

182 
(c as Const _,ts) => 

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

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

185 
 (f as Free _,ts) => 

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

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

188 
 (Bound(i),ts) => 

189 
let val j = trans d i 

190 
in if j < 0 then raise Unif 

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

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

193 
end 

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

12232  195 
let val js = ints_of' env ts; 
0  196 
val js' = map (trans d) js; 
197 
val ks = mk_proj_list js'; 

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

13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

199 
val Hty = type_of_G env (Fty,length js,ks) 
0  200 
val (env',H) = Envir.genvar a (env,Hty) 
201 
val env'' = 

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

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

204 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

212 
end; 

213 

214 

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

12784  216 
fun mk_ff_list(is,js) = 
217 
let fun mk([],[],_) = [] 

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

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

220 
 mk _ = error"mk_ff_list" 
0  221 
in mk(is,js,length is1) end; 
222 

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

224 
if is=js then env 

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

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

227 

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

229 
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

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

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

233 
else let val ks = is inter_int js 
13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

234 
val Hty = type_of_G env (Fty,length is,map (idx is) ks) 
0  235 
val (env',H) = Envir.genvar a (env,Hty) 
236 
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); 

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

238 
end; 

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

240 

241 
val tsgr = ref(Type.tsig0); 

242 

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

244 
if T=U then env 

12527  245 
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

246 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

247 
handle Type.TUNIFY => (typ_clash(iTs,T,U); raise Unif); 
0  248 

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

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

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

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

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

256 

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

12784  258 
((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
12232  259 
if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) 
260 
else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) 

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

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

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

12784  265 
 ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
0  266 
 ((Abs(_),_),_) => raise Pattern 
267 
 (_,(Abs(_),_)) => raise Pattern 

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

268 
 ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

269 
 ((Const(c,_),_),(Bound i,_)) => (clashB binders i c; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

270 
 ((Free(f,_),_),(Const(c,_),_)) => (clash f c; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

271 
 ((Free(f,_),_),(Bound i,_)) => (clashB binders i f; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

272 
 ((Bound i,_),(Const(c,_),_)) => (clashB binders i c; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

273 
 ((Bound i,_),(Free(f,_),_)) => (clashB binders i f; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

274 

0  275 

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

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

277 
if a<>b then (clash a b; raise Unif) 
0  278 
else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts) 
279 

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

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

281 
if i <> j then (clashBB binders i j; raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

282 
else foldl (unif binders) (env ,ss~~ts) 
0  283 

13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

284 
and flexrigid (params as (env,binders,F,is,t)) = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

285 
if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

286 
else (let val (u,env') = proj(t,env,binders,is) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

287 
in Envir.update((F,mkabs(binders,is,u)),env') end 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

288 
handle Unif => (proj_fail params; raise Unif)); 
0  289 

14643  290 
fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg; 
0  291 
foldl (unif []) (env,tus)); 
292 

293 

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

294 
(*Etacontract a term (fully)*) 
2792  295 

12797  296 
fun eta_contract t = 
297 
let 

298 
exception SAME; 

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

300 
((case eta body of 

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

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

303 
else incr_boundvars ~1 f 

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

305 
(case body of 

306 
(f $ Bound 0) => 

307 
if loose_bvar1 (f, 0) then raise SAME 

308 
else incr_boundvars ~1 f 

309 
 _ => raise SAME)) 

310 
 eta (f $ t) = 

311 
(let val f' = eta f 

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

313 
 eta _ = raise SAME 

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

315 
in etah t end; 

0  316 

12781  317 
val beta_eta_contract = eta_contract o Envir.beta_norm; 
318 

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

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

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

321 
*) 
12784  322 
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

323 
(case eta_contract2 body of 
12784  324 
body' as (f $ Bound 0) => 
325 
if loose_bvar1(f,0) then Abs(a,T,body') 

326 
else eta_contract_atom (incr_boundvars ~1 f) 

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

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

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

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

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

331 

13998  332 
(* put a term into eta long beta normal form *) 
333 
fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t) 

334 
 eta_long Ts t = (case strip_comb t of 

335 
(Abs _, _) => eta_long Ts (Envir.beta_norm t) 

336 
 (u, ts) => 

337 
let 

338 
val Us = binder_types (fastype_of1 (Ts, t)); 

339 
val i = length Us 

340 
in list_abs (map (pair "x") Us, 

341 
list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts)) 

342 
(map (incr_boundvars i) ts @ map Bound (i  1 downto 0)))) 

343 
end); 

344 

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

345 

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

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

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

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

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

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

356 

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

357 

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

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

359 

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

360 
exception MATCH; 
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 
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

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

364 

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

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

366 
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

367 
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

368 
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

369 
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

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

371 
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

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

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

374 
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

375 
(Var(ixn,T), t) => 
12784  376 
if loose_bvar(t,0) then raise MATCH 
377 
else (case assoc_string_int(insts,ixn) of 

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

379 
(ixn,t)::insts) 

380 
 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

381 
 (Free (a,T), Free (b,U)) => 
12784  382 
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

383 
 (Const (a,T), Const (b,U)) => 
12784  384 
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

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

386 
 (Abs(_,T,t), Abs(_,U,u)) => 
12784  387 
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

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

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

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

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

392 

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

393 
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

394 

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

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

396 

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

397 
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

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

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

400 
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

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

402 
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

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

404 
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

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

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

407 

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

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

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

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

411 
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

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

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

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

415 
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

416 
 _ => 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

417 
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

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

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

420 
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

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

422 

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

423 
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

424 
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

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

426 
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

427 
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

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

429 
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

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

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

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

433 
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

434 
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

435 
 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

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

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

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

439 
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

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

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

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

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

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

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

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

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

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

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

450 

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

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

452 
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

453 
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

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

455 

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

456 
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

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

458 
end; 
0  459 

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

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

461 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  462 

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

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

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

465 
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

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

467 
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

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

469 
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

470 
 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

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

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

473 

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

474 
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

475 
 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

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

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

478 

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

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

480 
 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

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

482 
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

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

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

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

486 

12784  487 

488 
(* rewriting  simple but fast *) 

489 

13195  490 
fun rewrite_term tsig rules procs tm = 
12784  491 
let 
13195  492 
val skel0 = Bound 0; 
493 

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

13195  496 

12797  497 
fun variant_absfree (x, T, t) = 
498 
let 

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

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

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

502 

12784  503 
fun match_rew tm (tm1, tm2) = 
13195  504 
let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 
505 
in Some (subst_vars (match tsig (tm1, tm)) rtm, rtm) 

506 
handle MATCH => None 

507 
end; 

12784  508 

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

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

512 
 x => x); 

513 

514 
fun rew1 (Var _) _ = None 

515 
 rew1 skel tm = (case rew2 skel tm of 

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

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

519 
 None => (case rew tm of 
13195  520 
Some (tm1, skel') => Some (if_none (rew1 skel' tm1) tm1) 
12784  521 
 None => None)) 
522 

13195  523 
and rew2 skel (tm1 $ tm2) = (case tm1 of 
12784  524 
Abs (_, _, body) => 
525 
let val tm' = subst_bound (tm2, body) 

13195  526 
in Some (if_none (rew2 skel0 tm') tm') end 
527 
 _ => 

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

529 
skel1 $ skel2 => (skel1, skel2) 

530 
 _ => (skel0, skel0)) 

531 
in case rew1 skel1 tm1 of 

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

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

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

535 
 None => (case rew1 skel2 tm2 of 

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

537 
 None => None) 

538 
end) 

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

540 
let 

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

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

543 
in case rew1 skel' tm' of 

12797  544 
Some tm'' => Some (abs tm'') 
13195  545 
 None => None 
12797  546 
end 
13195  547 
 rew2 _ _ = None 
12784  548 

13195  549 
in if_none (rew1 skel0 tm) tm end; 
12784  550 

0  551 
end; 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

552 

a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

553 
val trace_unify_fail = Pattern.trace_unify_fail; 