author  skalberg 
Sun, 13 Feb 2005 17:15:14 +0100  
changeset 15531  08c8dad8e399 
parent 14981  e73f8140af78 
child 15570  8d8c70b41bab 
permissions  rwrr 
12784  1 
(* Title: Pure/pattern.ML 
0  2 
ID: $Id$ 
12784  3 
Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer 
0  4 

5 
Unification of HigherOrder Patterns. 

6 

7 
See also: 

8 
Tobias Nipkow. Functional Unification of HigherOrder Patterns. 

9 
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

10 

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

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

2751  14 
infix aeconv; 
15 

0  16 
signature PATTERN = 
14787  17 
sig 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

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

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

25 
> (indexname*typ)list * (indexname*term)list 
14787  26 
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

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

30 
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

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

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

37 
exception Pattern 

14787  38 
end; 
0  39 

1501  40 
structure Pattern : PATTERN = 
0  41 
struct 
42 

43 
exception Unif; 

44 
exception Pattern; 

45 

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

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

47 

14875  48 
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

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

50 

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

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

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

53 

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

55 
if !trace_unify_fail 
14875  56 
then let val t = Sign.string_of_typ sg (Envir.norm_type tye T) 
57 
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

58 
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

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

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

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

66 

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

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

68 
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

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

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

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

74 

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

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

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

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

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

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

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

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

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

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

86 

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

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

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

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

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

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

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

95 

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

0  100 
 occ(t1$t2) = occ t1 orelse occ t2 
101 
 occ(Abs(_,_,t)) = occ t 

102 
 occ _ = false 

103 
in occ t end; 

104 

105 

106 
fun mapbnd f = 

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

108 
 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

109 
 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

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

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

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

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

117 

118 
fun mkabs (binders,is,t) = 

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

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

123 

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

125 

126 
fun ints_of [] = [] 

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

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

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

0  134 

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

136 
 app (s,[]) = s; 

137 

138 
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

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

140 
 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

141 

0  142 

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

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

145 
 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

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

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

148 
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

149 
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

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

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

153 

154 
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

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

158 

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

160 
fun mk_proj_list is = 

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

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

164 

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

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

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

170 
 t => (case strip_comb t of 

171 
(c as Const _,ts) => 

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

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

174 
 (f as Free _,ts) => 

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

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

177 
 (Bound(i),ts) => 

178 
let val j = trans d i 

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

179 
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

180 
in (list_comb(Bound j,ts'),env') end 
0  181 
 (Var(F as (a,_),Fty),ts) => 
12232  182 
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

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

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

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

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

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

191 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

199 
end; 

200 

201 

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

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

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

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

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

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

211 
if is=js then env 

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

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

214 

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

216 
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

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

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

220 
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

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

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

225 
end; 

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

227 

14875  228 
fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) = 
0  229 
if T=U then env 
14875  230 
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

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

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

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

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

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

0  241 

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

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

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

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

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

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

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

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

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

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

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

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

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

259 

0  260 

14875  261 
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

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

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

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

14875  269 
and flexrigid sg (params as (env,binders,F,is,t)) = 
270 
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

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

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

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

277 

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

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

12797  280 
fun eta_contract t = 
281 
let 

282 
exception SAME; 

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

287 
else incr_boundvars ~1 f 

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

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

292 
else incr_boundvars ~1 f 

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

295 
(let val f' = eta f 

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

297 
 eta _ = raise SAME 

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

299 
in etah t end; 

0  300 

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

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

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

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

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

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

310 
else eta_contract_atom (incr_boundvars ~1 f) 

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

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

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

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

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

315 

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

318 
 eta_long Ts t = (case strip_comb t of 

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

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

323 
val i = length Us 

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

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

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

327 
end); 

328 

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

329 

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

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

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

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

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

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

340 

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

341 

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

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

343 

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

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

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

348 

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

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

350 
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

351 
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

352 
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

353 
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

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

355 
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

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

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

358 
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

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

15531  362 
NONE => (typ_match tsig (tyinsts, (T, fastype_of t)), 
12784  363 
(ixn,t)::insts) 
15531  364 
 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

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

367 
 (Const (a,T), Const (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 
 (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

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

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

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

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

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

376 

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

377 
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

378 

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

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

380 

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

381 
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

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

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

384 
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

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

386 
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

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

388 
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

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

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

391 

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

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

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

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

395 
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

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

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

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

399 
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

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

401 
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

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

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

404 
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

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

406 

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

407 
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

408 
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

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

410 
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

411 
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

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

413 
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

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

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

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

417 
in case assoc_string_int(itms,ixn) of 
15531  418 
NONE => (iTs,match_bind(itms,binders,ixn,is,obj)) 
419 
 SOME u => if obj aeconv (red u is []) then env 

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

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

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

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

423 
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

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

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

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

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

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

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

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

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

434 

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

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

436 
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

437 
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

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

439 

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

440 
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

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

442 
end; 
0  443 

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

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

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

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

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

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

449 
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

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

451 
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

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

453 
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

454 
 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

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

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

457 

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

458 
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

459 
 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

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

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

462 

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

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

464 
 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

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

466 
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

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

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

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

470 

12784  471 

472 
(* rewriting  simple but fast *) 

473 

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

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

13195  480 

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

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

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

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

486 

12784  487 
fun match_rew tm (tm1, tm2) = 
13195  488 
let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 
15531  489 
in SOME (subst_vars (match tsig (tm1, tm)) rtm, rtm) 
490 
handle MATCH => NONE 

13195  491 
end; 
12784  492 

15531  493 
fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0) 
13195  494 
 rew tm = (case get_first (match_rew tm) rules of 
15531  495 
NONE => apsome (rpair skel0) (get_first (fn p => p tm) procs) 
13195  496 
 x => x); 
497 

15531  498 
fun rew1 (Var _) _ = NONE 
13195  499 
 rew1 skel tm = (case rew2 skel tm of 
15531  500 
SOME tm1 => (case rew tm1 of 
501 
SOME (tm2, skel') => SOME (if_none (rew1 skel' tm2) tm2) 

502 
 NONE => SOME tm1) 

503 
 NONE => (case rew tm of 

504 
SOME (tm1, skel') => SOME (if_none (rew1 skel' tm1) tm1) 

505 
 NONE => NONE)) 

12784  506 

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

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

514 
 _ => (skel0, skel0)) 

515 
in case rew1 skel1 tm1 of 

15531  516 
SOME tm1' => (case rew1 skel2 tm2 of 
517 
SOME tm2' => SOME (tm1' $ tm2') 

518 
 NONE => SOME (tm1' $ tm2)) 

519 
 NONE => (case rew1 skel2 tm2 of 

520 
SOME tm2' => SOME (tm1 $ tm2') 

521 
 NONE => NONE) 

13195  522 
end) 
523 
 rew2 skel (Abs (x, T, tm)) = 

524 
let 

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

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

527 
in case rew1 skel' tm' of 

15531  528 
SOME tm'' => SOME (abs tm'') 
529 
 NONE => NONE 

12797  530 
end 
15531  531 
 rew2 _ _ = NONE 
12784  532 

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

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

536 

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

537 
val trace_unify_fail = Pattern.trace_unify_fail; 