author  wenzelm 
Sat, 05 Jun 2004 13:07:49 +0200  
changeset 14875  c48d086264c4 
parent 14861  ca5cae7fb65a 
child 14981  e73f8140af78 
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 = 
14787  18 
sig 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

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

24 
val eta_contract_atom : term > term 
14787  25 
val match : Type.tsig > term * term 
2725
9453616d4b80
Declares eta_contract_atom; fixed comment; some tidying
paulson
parents:
2616
diff
changeset

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

28 
> (indexname*typ)list * (indexname*term)list 
14787  29 
val matches : Type.tsig > term * term > bool 
30 
val matches_subterm : Type.tsig > term * term > bool 

31 
val unify : Sign.sg * Envir.env * (term * term)list > Envir.env 

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

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

33 
val pattern : term > bool 
14787  34 
val rewrite_term : Type.tsig > (term * term) list > (term > term option) list 
13195  35 
> term > term 
0  36 
exception Unif 
37 
exception MATCH 

38 
exception Pattern 

14787  39 
end; 
0  40 

1501  41 
structure Pattern : PATTERN = 
0  42 
struct 
43 

44 
exception Unif; 

45 
exception Pattern; 

46 

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

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

48 

14875  49 
fun string_of_term sg env binders t = Sign.string_of_term sg 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

51 

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

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

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

54 

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

56 
if !trace_unify_fail 
14875  57 
then let val t = Sign.string_of_typ sg (Envir.norm_type tye T) 
58 
and u = Sign.string_of_typ sg (Envir.norm_type tye U) 

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

59 
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

60 
else () 
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 clash a b = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

63 
if !trace_unify_fail then tracing("Clash: " ^ a ^ " =/= " ^ b) else () 
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 boundVar binders i = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

67 

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

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

69 
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

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 clashB binders i s = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

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

75 

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

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

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

79 
val xs = bnames binders is 
14875  80 
val u = string_of_term sg env binders t 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

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

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

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

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

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

87 

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

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

90 
then let val f = Syntax.string_of_vname F 
14875  91 
val u = string_of_term sg env binders t 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

93 
"\nCannot unify!\n") 
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 

12784  97 
fun occurs(F,t,env) = 
0  98 
let fun occ(Var(G,_)) = (case Envir.lookup(env,G) of 
99 
Some(t) => occ t 

100 
 None => F=G) 

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

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

103 
 occ _ = false 

104 
in occ t end; 

105 

106 

107 
fun mapbnd f = 

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

109 
 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

110 
 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

111 
 mpb _ atom = atom 
0  112 
in mpb 0 end; 
113 

14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset

114 
fun idx [] j = raise Unif 
0  115 
 idx(i::is) j = if i=j then length is else idx is j; 
116 

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

118 

119 
fun mkabs (binders,is,t) = 

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

12784  121 
in Abs(x,T,mk is) end 
0  122 
 mk [] = t 
123 
in mk is end; 

124 

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

126 

127 
fun ints_of [] = [] 

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

130 
in if i mem_int is then raise Pattern else i::is end 
0  131 
 ints_of _ = raise Pattern; 
132 

12232  133 
fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); 
134 

0  135 

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

137 
 app (s,[]) = s; 

138 

139 
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

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

141 
 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

142 

0  143 

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

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

146 
 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

147 
 split_type _ = error("split_type"); 
0  148 

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

149 
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

150 
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

151 
in map (at Ts) is > U end; 
0  152 

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

154 

155 
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

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

159 

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

161 
fun mk_proj_list is = 

14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset

162 
let fun mk(i::is,j) = if is_some i then j :: mk(is,j1) else mk(is,j1) 
0  163 
 mk([],_) = [] 
164 
in mk(is,length is  1) end; 

165 

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

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

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

171 
 t => (case strip_comb t of 

172 
(c as Const _,ts) => 

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

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

175 
 (f as Free _,ts) => 

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

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

178 
 (Bound(i),ts) => 

179 
let val j = trans d i 

14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset

180 
val (ts',env') = prs(ts,env,d,binders) 
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset

181 
in (list_comb(Bound j,ts'),env') end 
0  182 
 (Var(F as (a,_),Fty),ts) => 
12232  183 
let val js = ints_of' env ts; 
14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset

184 
val js' = map (try (trans d)) js; 
0  185 
val ks = mk_proj_list js'; 
14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset

186 
val ls = mapfilter I js' 
13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

187 
val Hty = type_of_G env (Fty,length js,ks) 
0  188 
val (env',H) = Envir.genvar a (env,Hty) 
189 
val env'' = 

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

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

192 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

200 
end; 

201 

202 

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

12784  204 
fun mk_ff_list(is,js) = 
205 
let fun mk([],[],_) = [] 

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

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

208 
 mk _ = error"mk_ff_list" 
0  209 
in mk(is,js,length is1) end; 
210 

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

212 
if is=js then env 

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

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

215 

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

217 
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

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

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

221 
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

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

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

226 
end; 

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

228 

14875  229 
fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) = 
0  230 
if T=U then env 
14875  231 
else let val (iTs',maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (U, T) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1029
diff
changeset

232 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
14875  233 
handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif); 
0  234 

14875  235 
fun unif sg binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of 
0  236 
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => 
237 
let val name = if ns = "" then nt else ns 

14875  238 
in unif sg ((name,Ts)::binders) (env,(ts,tt)) end 
239 
 (Abs(ns,Ts,ts),t) => unif sg ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0))) 

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

241 
 p => cases sg (binders,env,p) 

0  242 

14875  243 
and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of 
12784  244 
((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
12232  245 
if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) 
246 
else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) 

14875  247 
 ((Var(F,_),ss),_) => flexrigid sg (env,binders,F,ints_of' env ss,t) 
248 
 (_,(Var(F,_),ts)) => flexrigid sg (env,binders,F,ints_of' env ts,s) 

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

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

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

0  252 
 ((Abs(_),_),_) => raise Pattern 
253 
 (_,(Abs(_),_)) => raise Pattern 

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

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

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

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

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

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

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

260 

0  261 

14875  262 
and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) = 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

263 
if a<>b then (clash a b; raise Unif) 
14875  264 
else foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts) 
0  265 

14875  266 
and rigidrigidB sg (env,binders,i,j,ss,ts) = 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

267 
if i <> j then (clashBB binders i j; raise Unif) 
14875  268 
else foldl (unif sg binders) (env ,ss~~ts) 
0  269 

14875  270 
and flexrigid sg (params as (env,binders,F,is,t)) = 
271 
if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif) 

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

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

273 
in Envir.update((F,mkabs(binders,is,u)),env') end 
14875  274 
handle Unif => (proj_fail sg params; raise Unif)); 
0  275 

14875  276 
fun unify(sg,env,tus) = foldl (unif sg []) (env,tus); 
0  277 

278 

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

279 
(*Etacontract a term (fully)*) 
2792  280 

12797  281 
fun eta_contract t = 
282 
let 

283 
exception SAME; 

14787  284 
fun eta (Abs (a, T, body)) = 
12797  285 
((case eta body of 
14787  286 
body' as (f $ Bound 0) => 
287 
if loose_bvar1 (f, 0) then Abs(a, T, body') 

288 
else incr_boundvars ~1 f 

12797  289 
 body' => Abs (a, T, body')) handle SAME => 
290 
(case body of 

14787  291 
(f $ Bound 0) => 
292 
if loose_bvar1 (f, 0) then raise SAME 

293 
else incr_boundvars ~1 f 

12797  294 
 _ => raise SAME)) 
295 
 eta (f $ t) = 

296 
(let val f' = eta f 

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

298 
 eta _ = raise SAME 

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

300 
in etah t end; 

0  301 

12781  302 
val beta_eta_contract = eta_contract o Envir.beta_norm; 
303 

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

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

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

306 
*) 
12784  307 
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

308 
(case eta_contract2 body of 
12784  309 
body' as (f $ Bound 0) => 
310 
if loose_bvar1(f,0) then Abs(a,T,body') 

311 
else eta_contract_atom (incr_boundvars ~1 f) 

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

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

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

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

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

316 

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

319 
 eta_long Ts t = (case strip_comb t of 

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

14787  321 
 (u, ts) => 
13998  322 
let 
323 
val Us = binder_types (fastype_of1 (Ts, t)); 

324 
val i = length Us 

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

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

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

328 
end); 

329 

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

330 

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

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

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

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

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

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

341 

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

342 

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

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

344 

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

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

346 

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

347 
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

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

349 

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

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

351 
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

352 
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

353 
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

354 
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

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

356 
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

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

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

359 
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

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

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

364 
(ixn,t)::insts) 

365 
 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

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

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

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

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

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

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

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

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

377 

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

378 
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

379 

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

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

381 

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

382 
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

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

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

385 
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

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

387 
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

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

389 
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

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

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

392 

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

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

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

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

396 
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

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

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

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

400 
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

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

402 
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

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

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

405 
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

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

407 

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

408 
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

409 
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

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

411 
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

412 
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

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

414 
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

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

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

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

418 
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

419 
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

420 
 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

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

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

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

424 
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

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

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

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

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

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

430 
 (Abs _, _) => raise Pattern 
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 
 _ => raise MATCH 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

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

435 

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

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

437 
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

438 
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

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

440 

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

441 
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

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

443 
end; 
0  444 

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

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

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

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

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

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

450 
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

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

452 
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

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

454 
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

455 
 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

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

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

458 

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

459 
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

460 
 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

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

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

463 

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

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

465 
 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

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

467 
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

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

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

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

471 

12784  472 

473 
(* rewriting  simple but fast *) 

474 

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

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

13195  481 

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

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

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

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

487 

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

491 
handle MATCH => None 

492 
end; 

12784  493 

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

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

497 
 x => x); 

498 

499 
fun rew1 (Var _) _ = None 

500 
 rew1 skel tm = (case rew2 skel tm of 

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

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

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

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

13195  511 
in Some (if_none (rew2 skel0 tm') tm') end 
14787  512 
 _ => 
13195  513 
let val (skel1, skel2) = (case skel of 
514 
skel1 $ skel2 => (skel1, skel2) 

515 
 _ => (skel0, skel0)) 

516 
in case rew1 skel1 tm1 of 

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

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

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

520 
 None => (case rew1 skel2 tm2 of 

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

522 
 None => None) 

523 
end) 

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

525 
let 

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

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

528 
in case rew1 skel' tm' of 

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

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

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

537 

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

538 
val trace_unify_fail = Pattern.trace_unify_fail; 