author  wenzelm 
Fri, 24 May 2013 14:31:44 +0200  
changeset 52127  a40dfe02dd83 
parent 51700  c8f2bad67dbb 
child 52129  3fd0fe916097 
permissions  rwrr 
12784  1 
(* Title: Pure/pattern.ML 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28348
diff
changeset

2 
Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen 
0  3 

4 
Unification of HigherOrder Patterns. 

5 

6 
See also: 

7 
Tobias Nipkow. Functional Unification of HigherOrder Patterns. 

8 
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

9 

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

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

2751  13 
infix aeconv; 
14 

0  15 
signature PATTERN = 
14787  16 
sig 
32738  17 
val trace_unify_fail: bool Unsynchronized.ref 
17203  18 
val aeconv: term * term > bool 
19 
val eta_long: typ list > term > term 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

20 
val match: theory > term * term > Type.tyenv * Envir.tenv > Type.tyenv * Envir.tenv 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

21 
val first_order_match: theory > term * term 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

22 
> Type.tyenv * Envir.tenv > Type.tyenv * Envir.tenv 
17203  23 
val matches: theory > term * term > bool 
28348  24 
val matchess: theory > term list * term list > bool 
19880  25 
val equiv: theory > term * term > bool 
17203  26 
val matches_subterm: theory > term * term > bool 
52127
a40dfe02dd83
reuse Pattern.unify_types, including its trace_unify_fail option;
wenzelm
parents:
51700
diff
changeset

27 
val unify_types: theory > typ * typ > Envir.env > Envir.env 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

28 
val unify: theory > term * term > Envir.env > Envir.env 
17203  29 
val first_order: term > bool 
30 
val pattern: term > bool 

30565
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

31 
val match_rew: theory > term > term * term > (term * term) option 
17203  32 
val rewrite_term: theory > (term * term) list > (term > term option) list > term > term 
35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

33 
val rewrite_term_top: theory > (term * term) list > (term > term option) list > term > term 
0  34 
exception Unif 
35 
exception MATCH 

36 
exception Pattern 

14787  37 
end; 
0  38 

17203  39 
structure Pattern: PATTERN = 
0  40 
struct 
41 

42 
exception Unif; 

43 
exception Pattern; 

44 

32738  45 
val trace_unify_fail = Unsynchronized.ref false; 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

46 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26831
diff
changeset

47 
fun string_of_term thy env binders t = 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26831
diff
changeset

48 
Syntax.string_of_term_global thy 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26831
diff
changeset

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

50 

18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset

51 
fun bname binders i = fst (nth binders i); 
13642
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 

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

55 
if !trace_unify_fail 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26831
diff
changeset

56 
then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T) 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26831
diff
changeset

57 
and u = Syntax.string_of_typ_global thy (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 

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

76 
if !trace_unify_fail 
22678  77 
then let val f = Term.string_of_vname F 
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

78 
val xs = bnames binders is 
17203  79 
val u = string_of_term thy env binders t 
19300  80 
val ys = bnames binders (subtract (op =) is (loose_bnos t)) 
13642
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 

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

88 
if !trace_unify_fail 
22678  89 
then let val f = Term.string_of_vname F 
17203  90 
val u = string_of_term thy 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) = 
51700  97 
let fun occ(Var (G, T)) = (case Envir.lookup env (G, T) 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 
16668  114 
 idx(i::is) j = if (i:int) =j then length is else idx is j; 
0  115 

116 
fun mkabs (binders,is,t) = 

18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset

117 
let fun mk(i::is) = let val (x,T) = nth binders i 
12784  118 
in Abs(x,T,mk is) end 
0  119 
 mk [] = t 
120 
in mk is end; 

121 

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

123 

124 
fun ints_of [] = [] 

12784  125 
 ints_of (Bound i ::bs) = 
0  126 
let val is = ints_of bs 
20672  127 
in if member (op =) is i then raise Pattern else i::is end 
0  128 
 ints_of _ = raise Pattern; 
129 

12232  130 
fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); 
131 

0  132 

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

134 
 app (s,[]) = s; 

135 

136 
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

137 
 red t [] [] = t 
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset

138 
 red t is jn = app (mapbnd (nth jn) t,is); 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

139 

0  140 

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

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

143 
 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

144 
 split_type _ = error("split_type"); 
0  145 

32032  146 
fun type_of_G env (T, n, is) = 
147 
let 

148 
val tyenv = Envir.type_env env; 

149 
val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []); 

18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset

150 
in map (nth 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)) 
51700  156 
in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end; 
0  157 

158 

23222  159 
(*predicate: downto0 (is, n) <=> is = [n, n  1, ..., 0]*) 
160 
fun downto0 (i :: is, n) = i = n andalso downto0 (is, n  1) 

161 
 downto0 ([], n) = n = ~1; 

162 

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

0  164 
fun mk_proj_list is = 
19502  165 
let fun mk(i::is,j) = if is_some i then j :: mk(is,j1) else mk(is,j1) 
0  166 
 mk([],_) = [] 
167 
in mk(is,length is  1) end; 

168 

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

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

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

174 
 t => (case strip_comb t of 

175 
(c as Const _,ts) => 

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

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

178 
 (f as Free _,ts) => 

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

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

181 
 (Bound(i),ts) => 

182 
let val j = trans d i 

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

183 
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

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

187 
val js' = map (try (trans d)) js; 
0  188 
val ks = mk_proj_list js'; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19300
diff
changeset

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

190 
val Hty = type_of_G env (Fty,length js,ks) 
0  191 
val (env',H) = Envir.genvar a (env,Hty) 
192 
val env'' = 

51700  193 
Envir.update ((F, Fty), mkhnf (binders, js, H, ks)) env' 
0  194 
in (app(H,ls),env'') end 
195 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

203 
end; 

204 

205 

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

12784  207 
fun mk_ff_list(is,js) = 
208 
let fun mk([],[],_) = [] 

16668  209 
 mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k1) 
0  210 
else mk(is,js,k1) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

211 
 mk _ = error"mk_ff_list" 
0  212 
in mk(is,js,length is1) end; 
213 

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

215 
if is=js then env 

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

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

218 

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

220 
let fun ff(F,Fty,is,G as (a,_),Gty,js) = 

33038  221 
if subset (op =) (js, is) 
0  222 
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js)) 
51700  223 
in Envir.update ((F, Fty), t) env end 
33049
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33038
diff
changeset

224 
else let val ks = inter (op =) js is 
13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset

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

51700  228 
in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env') 
0  229 
end; 
35408  230 
in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end 
0  231 

32032  232 
fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = 
233 
if T = U then env 

234 
else 

235 
let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) 

236 
in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end 

237 
handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif); 

0  238 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

239 
fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of 
0  240 
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => 
241 
let val name = if ns = "" then nt else ns 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

242 
in unif thy ((name,Ts)::binders) (ts,tt) env end 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

243 
 (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

244 
 (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env 
17203  245 
 p => cases thy (binders,env,p) 
0  246 

17203  247 
and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of 
12784  248 
((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
12232  249 
if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) 
250 
else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) 

17203  251 
 ((Var(F,Fty),ss),_) => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t) 
252 
 (_,(Var(F,Fty),ts)) => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s) 

253 
 ((Const c,ss),(Const d,ts)) => rigidrigid thy (env,binders,c,d,ss,ts) 

254 
 ((Free(f),ss),(Free(g),ts)) => rigidrigid thy (env,binders,f,g,ss,ts) 

255 
 ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts) 

0  256 
 ((Abs(_),_),_) => raise Pattern 
257 
 (_,(Abs(_),_)) => raise Pattern 

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

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

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

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

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

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

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

264 

0  265 

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

267 
if a<>b then (clash a b; raise Unif) 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

268 
else env > unify_types thy (Ta,Tb) > fold (unif thy binders) (ss~~ts) 
0  269 

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

271 
if i <> j then (clashBB binders i j; raise Unif) 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

272 
else fold (unif thy binders) (ss~~ts) env 
0  273 

17203  274 
and flexrigid thy (params as (env,binders,F,Fty,is,t)) = 
275 
if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif) 

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

276 
else (let val (u,env') = proj(t,env,binders,is) 
51700  277 
in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end 
17203  278 
handle Unif => (proj_fail thy params; raise Unif)); 
0  279 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

280 
fun unify thy = unif thy []; 
0  281 

282 

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

46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

285 
 eta_long Ts t = 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

286 
(case strip_comb t of 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

287 
(Abs _, _) => eta_long Ts (Envir.beta_norm t) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

288 
 (u, ts) => 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

289 
let 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

290 
val Us = binder_types (fastype_of1 (Ts, t)); 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

291 
val i = length Us; 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

292 
in 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

293 
fold_rev (Term.abs o pair "x") Us 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

294 
(list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts)) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

295 
(map (incr_boundvars i) ts @ map Bound (i  1 downto 0)))) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42083
diff
changeset

296 
end); 
13998  297 

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

298 

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

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

300 
Note that Consts and Vars may have more than one type.*) 
30555
5925cd6671d5
tuned aeconv: test plain aconv before expensive eta_contract;
wenzelm
parents:
29269
diff
changeset

301 
fun t aeconv u = t aconv u orelse 
5925cd6671d5
tuned aeconv: test plain aconv before expensive eta_contract;
wenzelm
parents:
29269
diff
changeset

302 
Envir.eta_contract t aconv Envir.eta_contract u; 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
63
diff
changeset

303 

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

304 

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

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

306 

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

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

308 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

309 
fun typ_match thy TU tyenv = Sign.typ_match thy TU tyenv 
16939  310 
handle Type.TYPE_MATCH => raise MATCH; 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

311 

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

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

313 
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

314 
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

315 
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

316 
Precondition: the pattern is already etacontracted! 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

317 
Types are matched on the fly*) 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

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

319 
let 
25473
812db0f215b3
first_order_match now only calls loose_bvar when inside an abstraction.
berghofe
parents:
23222
diff
changeset

320 
fun mtch k (instsp as (tyinsts,insts)) = fn 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

321 
(Var(ixn,T), t) => 
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
41067
diff
changeset

322 
if k > 0 andalso Term.is_open t then raise MATCH 
51700  323 
else (case Envir.lookup1 insts (ixn, T) of 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

324 
NONE => (typ_match thy (T, fastype_of t) tyinsts, 
17412  325 
Vartab.update_new (ixn, (T, t)) insts) 
15531  326 
 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

327 
 (Free (a,T), Free (b,U)) => 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

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

329 
 (Const (a,T), Const (b,U)) => 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

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

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

332 
 (Abs(_,T,t), Abs(_,U,u)) => 
25473
812db0f215b3
first_order_match now only calls loose_bvar when inside an abstraction.
berghofe
parents:
23222
diff
changeset

333 
mtch (k + 1) (typ_match thy (T,U) tyinsts, insts) (t,u) 
812db0f215b3
first_order_match now only calls loose_bvar when inside an abstraction.
berghofe
parents:
23222
diff
changeset

334 
 (f$t, g$u) => mtch k (mtch k instsp (f,g)) (t, u) 
812db0f215b3
first_order_match now only calls loose_bvar when inside an abstraction.
berghofe
parents:
23222
diff
changeset

335 
 (t, Abs(_,U,u)) => mtch (k + 1) instsp ((incr t)$(Bound 0), u) 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

336 
 _ => raise MATCH 
25473
812db0f215b3
first_order_match now only calls loose_bvar when inside an abstraction.
berghofe
parents:
23222
diff
changeset

337 
in fn tu => fn env => mtch 0 env tu end; 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

338 

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

339 

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

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

341 

15797  342 
fun match_bind(itms,binders,ixn,T,is,t) = 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

344 
in if null is 
17412  345 
then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH 
33038  346 
else if subset (op =) (js, is) 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

347 
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

348 
else mapbnd (idx is) t 
17412  349 
in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

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

352 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

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

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

355 
(* Pre: pat and obj have same type *) 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

356 
fun mtch binders (pat,obj) (env as (iTs,itms)) = 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

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

359 
(case obj of 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

360 
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env 
32035  361 
 _ => let val Tt = Envir.subst_type iTs Ts 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

362 
in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end) 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

364 
Abs(nt,Tt,tt) => 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

365 
mtch((nt,Tt)::binders) ((incr pat)$Bound(0),tt) env 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

367 

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

368 
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

369 
let val (ph,pargs) = strip_comb pat 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

370 
fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms) 
41067  371 
handle ListPair.UnequalLengths => raise MATCH 
16668  372 
fun rigrig2((a:string,Ta),(b,Tb),oargs) = 
373 
if a <> b then raise MATCH 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

374 
else rigrig1(typ_match thy (Ta,Tb) iTs, oargs) 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

375 
in case ph of 
15797  376 
Var(ixn,T) => 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

377 
let val is = ints_of pargs 
51700  378 
in case Envir.lookup1 itms (ixn, T) of 
15797  379 
NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj)) 
15531  380 
 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

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

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

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

384 
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

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

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

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

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

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

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

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

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

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

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

395 

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

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

397 
and oT = fastype_of obj 
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

398 
val envir' = apfst (typ_match thy (pT, oT)) envir; 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

399 
in mtch [] po envir' handle Pattern => first_order_match thy po envir' end; 
0  400 

18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

401 
fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false; 
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset

402 

46857  403 
fun matchess thy (ps, os) = 
404 
length ps = length os andalso 

405 
((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false); 

28348  406 

19880  407 
fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t); 
408 

0  409 

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

410 
(* Does pat match a subterm of obj? *) 
22255  411 
fun matches_subterm thy (pat, obj) = 
412 
let 

413 
fun msub bounds obj = matches thy (pat, obj) orelse 

414 
(case obj of 

415 
Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t))) 

416 
 t $ u => msub bounds t orelse msub bounds u 

417 
 _ => false) 

418 
in msub 0 obj end; 

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

419 

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

420 
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

421 
 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

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

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

424 

20672  425 
fun pattern (Abs (_, _, t)) = pattern t 
426 
 pattern t = 

427 
let val (head, args) = strip_comb t in 

428 
if is_Var head then 

429 
forall is_Bound args andalso not (has_duplicates (op aconv) args) 

430 
else forall pattern args 

431 
end; 

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

432 

12784  433 

434 
(* rewriting  simple but fast *) 

435 

30565
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

436 
fun match_rew thy tm (tm1, tm2) = 
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

437 
let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in 
32035  438 
SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm) 
30565
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

439 
handle MATCH => NONE 
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

440 
end; 
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

441 

35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

442 
fun gen_rewrite_term bot thy rules procs tm = 
12784  443 
let 
13195  444 
val skel0 = Bound 0; 
445 

16939  446 
fun variant_absfree bounds (x, T, t) = 
12797  447 
let 
20079
ec5c8584487c
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19880
diff
changeset

448 
val (x', t') = Term.dest_abs (Name.bound bounds, T, t); 
16939  449 
fun abs u = Abs (x, T, abstract_over (Free (x', T), u)); 
450 
in (abs, t') end; 

12797  451 

15531  452 
fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0) 
30565
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

453 
 rew tm = 
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

454 
(case get_first (match_rew thy tm) rules of 
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

455 
NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs) 
784be11cb70e
export match_rew  useful for implementing "procs" for rewrite_term;
wenzelm
parents:
30555
diff
changeset

456 
 x => x); 
13195  457 

35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

458 
fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of 
12784  459 
Abs (_, _, body) => 
460 
let val tm' = subst_bound (tm2, body) 

35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

461 
in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end 
14787  462 
 _ => 
13195  463 
let val (skel1, skel2) = (case skel of 
464 
skel1 $ skel2 => (skel1, skel2) 

465 
 _ => (skel0, skel0)) 

35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

466 
in case r bounds skel1 tm1 of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

467 
SOME tm1' => (case r bounds skel2 tm2 of 
15531  468 
SOME tm2' => SOME (tm1' $ tm2') 
469 
 NONE => SOME (tm1' $ tm2)) 

35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

470 
 NONE => (case r bounds skel2 tm2 of 
15531  471 
SOME tm2' => SOME (tm1 $ tm2') 
472 
 NONE => NONE) 

13195  473 
end) 
35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

474 
 rew_sub r bounds skel (Abs body) = 
13195  475 
let 
16939  476 
val (abs, tm') = variant_absfree bounds body; 
13195  477 
val skel' = (case skel of Abs (_, _, skel') => skel'  _ => skel0) 
35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

478 
in case r (bounds + 1) skel' tm' of 
15531  479 
SOME tm'' => SOME (abs tm'') 
480 
 NONE => NONE 

12797  481 
end 
35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

482 
 rew_sub _ _ _ _ = NONE; 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

483 

6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

484 
fun rew_bot bounds (Var _) _ = NONE 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

485 
 rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

486 
SOME tm1 => (case rew tm1 of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

487 
SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2)) 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

488 
 NONE => SOME tm1) 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

489 
 NONE => (case rew tm of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

490 
SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1)) 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

491 
 NONE => NONE)); 
12784  492 

35210
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

493 
fun rew_top bounds _ tm = (case rew tm of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

494 
SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

495 
SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2)) 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

496 
 NONE => SOME tm1) 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

497 
 NONE => (case rew_sub rew_top bounds skel0 tm of 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

498 
SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1)) 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

499 
 NONE => NONE)); 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

500 

6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

501 
in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end; 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

502 

6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

503 
val rewrite_term = gen_rewrite_term true; 
6e45e4c94751
Added function rewrite_term_top for topdown rewriting.
berghofe
parents:
33049
diff
changeset

504 
val rewrite_term_top = gen_rewrite_term false; 
12784  505 

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

507 

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

508 
val trace_unify_fail = Pattern.trace_unify_fail; 