author  berghofe 
Fri, 04 Apr 2003 17:00:25 +0200  
changeset 13891  ae9a2a433388 
parent 13645  430310b12c5b 
child 13998  75a399c2781f 
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 
12781  25 
val beta_eta_contract : term > term 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

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

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

29 
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

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

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

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

33 
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

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

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

0  38 
exception Unif 
39 
exception MATCH 

40 
exception Pattern 

1501  41 
end; 
0  42 

1501  43 
structure Pattern : PATTERN = 
0  44 
struct 
45 

46 
type type_sig = Type.type_sig 

47 
type sg = Sign.sg 

48 
type env = Envir.env 

49 

50 
exception Unif; 

51 
exception Pattern; 

52 

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

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

54 

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

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

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

57 

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

58 
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

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

60 

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

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

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

63 

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

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

65 
if !trace_unify_fail 
13645  66 
then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T) 
67 
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

68 
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

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

70 

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

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

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

73 

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

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

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

76 

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

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

78 
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

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

80 

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

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

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

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

84 

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

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

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

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

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

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

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

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

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

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

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

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

96 

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

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

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

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

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

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

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

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

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

105 

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

109 
 None => F=G) 

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

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

112 
 occ _ = false 

113 
in occ t end; 

114 

115 

116 
fun mapbnd f = 

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

118 
 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

119 
 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

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

123 
fun idx [] j = ~10000 

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

125 

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

127 

128 
fun mkabs (binders,is,t) = 

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

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

133 

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

135 

136 
fun ints_of [] = [] 

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

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

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

0  144 

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

146 
 app (s,[]) = s; 

147 

148 
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

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

150 
 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

151 

0  152 

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

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

155 
 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

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

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

158 
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

159 
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

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

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

163 

164 
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

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

168 

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

170 
fun mk_proj_list is = 

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

172 
 mk([],_) = [] 

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

174 

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

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

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

180 
 t => (case strip_comb t of 

181 
(c as Const _,ts) => 

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

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

184 
 (f as Free _,ts) => 

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

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

187 
 (Bound(i),ts) => 

188 
let val j = trans d i 

189 
in if j < 0 then raise Unif 

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

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

192 
end 

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

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

197 
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

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

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

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

203 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

211 
end; 

212 

213 

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

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

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

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

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

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

223 
if is=js then env 

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

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

226 

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

228 
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

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

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

232 
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

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

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

237 
end; 

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

239 

240 
val tsgr = ref(Type.tsig0); 

241 

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

243 
if T=U then env 

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

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

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

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

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

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

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

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

255 

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

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

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

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

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

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

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

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

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

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

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

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

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

273 

0  274 

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

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

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

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

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

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

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

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

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

284 
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

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

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

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

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

289 
fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg); 
0  290 
foldl (unif []) (env,tus)); 
291 

292 

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

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

12797  295 
fun eta_contract t = 
296 
let 

297 
exception SAME; 

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

299 
((case eta body of 

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

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

302 
else incr_boundvars ~1 f 

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

304 
(case body of 

305 
(f $ Bound 0) => 

306 
if loose_bvar1 (f, 0) then raise SAME 

307 
else incr_boundvars ~1 f 

308 
 _ => raise SAME)) 

309 
 eta (f $ t) = 

310 
(let val f' = eta f 

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

312 
 eta _ = raise SAME 

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

314 
in etah t end; 

0  315 

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

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

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

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

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

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

325 
else eta_contract_atom (incr_boundvars ~1 f) 

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

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

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

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

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

330 

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

331 

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

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

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

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

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

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

342 

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

343 

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

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

345 

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

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

347 

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

348 
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

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

350 

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

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

352 
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

353 
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

354 
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

355 
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

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

357 
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

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

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

360 
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

361 
(Var(ixn,T), t) => 
12784  362 
if loose_bvar(t,0) then raise MATCH 
363 
else (case assoc_string_int(insts,ixn) of 

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

365 
(ixn,t)::insts) 

366 
 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

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

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

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

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

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

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

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

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

378 

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

379 
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

380 

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

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

382 

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

383 
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

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

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

386 
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

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

388 
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

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

390 
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

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

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

393 

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

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

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

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

397 
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

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

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

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

401 
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

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

403 
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

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

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

406 
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

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

408 

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

409 
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

410 
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

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

412 
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

413 
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

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

415 
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

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

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

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

419 
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

420 
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

421 
 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

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

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

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

425 
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

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

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

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

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

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

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

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

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

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

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

436 

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

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

438 
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

439 
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

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

441 

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

442 
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

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

444 
end; 
0  445 

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

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

447 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  448 

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

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

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

451 
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

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

453 
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

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

455 
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

456 
 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

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

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

459 

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

460 
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

461 
 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

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

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

464 

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

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

466 
 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

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

468 
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

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

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

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

472 

12784  473 

474 
(* rewriting  simple but fast *) 

475 

13195  476 
fun rewrite_term tsig rules procs tm = 
12784  477 
let 
13195  478 
val skel0 = Bound 0; 
479 

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

13195  482 

12797  483 
fun variant_absfree (x, T, t) = 
484 
let 

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

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

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

488 

12784  489 
fun match_rew tm (tm1, tm2) = 
13195  490 
let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 
491 
in Some (subst_vars (match tsig (tm1, tm)) rtm, rtm) 

492 
handle MATCH => None 

493 
end; 

12784  494 

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

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

498 
 x => x); 

499 

500 
fun rew1 (Var _) _ = None 

501 
 rew1 skel tm = (case rew2 skel tm of 

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

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

505 
 None => (case rew tm of 
13195  506 
Some (tm1, skel') => Some (if_none (rew1 skel' tm1) tm1) 
12784  507 
 None => None)) 
508 

13195  509 
and rew2 skel (tm1 $ tm2) = (case tm1 of 
12784  510 
Abs (_, _, body) => 
511 
let val tm' = subst_bound (tm2, body) 

13195  512 
in Some (if_none (rew2 skel0 tm') tm') end 
513 
 _ => 

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

515 
skel1 $ skel2 => (skel1, skel2) 

516 
 _ => (skel0, skel0)) 

517 
in case rew1 skel1 tm1 of 

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

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

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

521 
 None => (case rew1 skel2 tm2 of 

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

523 
 None => None) 

524 
end) 

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

526 
let 

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

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

529 
in case rew1 skel' tm' of 

12797  530 
Some tm'' => Some (abs tm'') 
13195  531 
 None => None 
12797  532 
end 
13195  533 
 rew2 _ _ = None 
12784  534 

13195  535 
in if_none (rew1 skel0 tm) tm end; 
12784  536 

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

538 

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

539 
val trace_unify_fail = Pattern.trace_unify_fail; 