author  nipkow 
Thu, 10 Oct 2002 19:02:23 +0200  
changeset 13642  a3d97348ceb6 
parent 13195  98975cc13d28 
child 13645  430310b12c5b 
permissions  rwrr 
12784  1 
(* Title: Pure/pattern.ML 
0  2 
ID: $Id$ 
12784  3 
Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

0  5 

6 
Unification of HigherOrder Patterns. 

7 

8 
See also: 

9 
Tobias Nipkow. Functional Unification of HigherOrder Patterns. 

10 
In Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993. 

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

11 

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

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

2751  15 
infix aeconv; 
16 

0  17 
signature PATTERN = 
1501  18 
sig 
0  19 
type type_sig 
20 
type sg 

21 
type env 

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

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

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

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

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

28 
> (indexname*typ)list * (indexname*term)list 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

29 
val first_order_match : type_sig > term * term 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

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

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

33 
val unify : sg * env * (term * term)list > env 
4820
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

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

0  38 
exception Unif 
39 
exception MATCH 

40 
exception Pattern 

1501  41 
end; 
0  42 

1501  43 
structure Pattern : PATTERN = 
0  44 
struct 
45 

46 
type type_sig = Type.type_sig 

47 
type sg = Sign.sg 

48 
type env = Envir.env 

49 

50 
exception Unif; 

51 
exception Pattern; 

52 

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

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

54 

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

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

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

57 

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

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

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

60 

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

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

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

63 

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

64 
fun norm_typ tye = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

65 
let fun chase(v,s) = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

66 
(case Vartab.lookup (tye, v) of 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

67 
Some U => norm_typ tye U 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

68 
 None => TVar(v,s)) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

69 
in map_type_tvar chase end 
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 typ_clash(tye,T,U) = 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

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

73 
then let val t = Sign.string_of_typ (!sgr) (norm_typ tye T) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

74 
and u = Sign.string_of_typ (!sgr) (norm_typ tye U) 
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset

75 
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

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

77 

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

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

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

80 

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

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

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

83 

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

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

85 
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

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

87 

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

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

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

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

91 

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

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

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

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

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

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

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

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

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

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

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

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

103 

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

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

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

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

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

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

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

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

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

112 

12784  113 
fun occurs(F,t,env) = 
0  114 
let fun occ(Var(G,_)) = (case Envir.lookup(env,G) of 
115 
Some(t) => occ t 

116 
 None => F=G) 

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

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

119 
 occ _ = false 

120 
in occ t end; 

121 

122 

123 
fun mapbnd f = 

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

125 
 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

126 
 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

127 
 mpb _ atom = atom 
0  128 
in mpb 0 end; 
129 

130 
fun idx [] j = ~10000 

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

132 

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

134 

135 
fun mkabs (binders,is,t) = 

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

12784  137 
in Abs(x,T,mk is) end 
0  138 
 mk [] = t 
139 
in mk is end; 

140 

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

142 

143 
fun ints_of [] = [] 

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

146 
in if i mem_int is then raise Pattern else i::is end 
0  147 
 ints_of _ = raise Pattern; 
148 

12232  149 
fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); 
150 

0  151 

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

153 
 app (s,[]) = s; 

154 

155 
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

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

157 
 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

158 

0  159 

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

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

162 
 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

163 
 split_type _ = error("split_type"); 
0  164 

165 
fun type_of_G (T,n,is) = 

166 
let val (Ts,U) = split_type(T,n,[]) in map(at Ts)is > U end; 

167 

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

169 

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

171 
let val (env',G) = Envir.genvar a (env,type_of_G(T,length is,js)) 

172 
in Envir.update((F,mkhnf(binders,is,G,js)),env') end; 

173 

174 

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

176 
fun mk_proj_list is = 

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

178 
 mk([],_) = [] 

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

180 

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

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

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

186 
 t => (case strip_comb t of 

187 
(c as Const _,ts) => 

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

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

190 
 (f as Free _,ts) => 

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

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

193 
 (Bound(i),ts) => 

194 
let val j = trans d i 

195 
in if j < 0 then raise Unif 

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

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

198 
end 

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

12232  200 
let val js = ints_of' env ts; 
0  201 
val js' = map (trans d) js; 
202 
val ks = mk_proj_list js'; 

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

204 
val Hty = type_of_G(Fty,length js,ks) 

205 
val (env',H) = Envir.genvar a (env,Hty) 

206 
val env'' = 

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

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

209 
 _ => raise Pattern)) 

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

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

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

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

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

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

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

217 
end; 

218 

219 

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

12784  221 
fun mk_ff_list(is,js) = 
222 
let fun mk([],[],_) = [] 

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

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

225 
 mk _ = error"mk_ff_list" 
0  226 
in mk(is,js,length is1) end; 
227 

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

229 
if is=js then env 

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

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

232 

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

234 
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

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

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

238 
else let val ks = is inter_int js 
0  239 
val Hty = type_of_G(Fty,length is,map (idx is) ks) 
240 
val (env',H) = Envir.genvar a (env,Hty) 

241 
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); 

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

243 
end; 

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

245 

246 
val tsgr = ref(Type.tsig0); 

247 

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

249 
if T=U then env 

12527  250 
else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1029
diff
changeset

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

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

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

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

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

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

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

261 

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

12784  263 
((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
12232  264 
if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) 
265 
else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) 

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

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

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

12784  270 
 ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
0  271 
 ((Abs(_),_),_) => raise Pattern 
272 
 (_,(Abs(_),_)) => raise Pattern 

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

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

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

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

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

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

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

279 

0  280 

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

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

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

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

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

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

287 
else foldl (unif binders) (env ,ss~~ts) 
0  288 

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

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

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

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

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

293 
handle Unif => (proj_fail params; raise Unif)); 
0  294 

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

295 
fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg); 
0  296 
foldl (unif []) (env,tus)); 
297 

298 

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

299 
(*Etacontract a term (fully)*) 
2792  300 

12797  301 
fun eta_contract t = 
302 
let 

303 
exception SAME; 

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

305 
((case eta body of 

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

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

308 
else incr_boundvars ~1 f 

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

310 
(case body of 

311 
(f $ Bound 0) => 

312 
if loose_bvar1 (f, 0) then raise SAME 

313 
else incr_boundvars ~1 f 

314 
 _ => raise SAME)) 

315 
 eta (f $ t) = 

316 
(let val f' = eta f 

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

318 
 eta _ = raise SAME 

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

320 
in etah t end; 

0  321 

12781  322 
val beta_eta_contract = eta_contract o Envir.beta_norm; 
323 

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

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

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

326 
*) 
12784  327 
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

328 
(case eta_contract2 body of 
12784  329 
body' as (f $ Bound 0) => 
330 
if loose_bvar1(f,0) then Abs(a,T,body') 

331 
else eta_contract_atom (incr_boundvars ~1 f) 

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

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

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

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

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

336 

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

337 

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

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

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

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

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

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

348 

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

349 

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

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

351 

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

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

353 

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

354 
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

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

356 

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

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

358 
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

359 
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

360 
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

361 
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

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

363 
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

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

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

366 
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

367 
(Var(ixn,T), t) => 
12784  368 
if loose_bvar(t,0) then raise MATCH 
369 
else (case assoc_string_int(insts,ixn) of 

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

371 
(ixn,t)::insts) 

372 
 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

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

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

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

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

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

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

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

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

384 

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

385 
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

386 

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

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

388 

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

389 
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

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

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

392 
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

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

394 
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

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

396 
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

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

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

399 

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

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

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

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

403 
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

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

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

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

407 
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

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

409 
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

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

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

412 
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

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

414 

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

415 
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

416 
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

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

418 
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

419 
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

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

421 
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

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

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

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

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

426 
None => (iTs,match_bind(itms,binders,ixn,is,obj)) 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

427 
 Some u => if obj aeconv (red u is []) then env 
8f6dbbd8d497
Tried to speed up the rewriter by etacontracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset

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

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

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

431 
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

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

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

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

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

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

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

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

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

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

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

442 

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

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

444 
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

445 
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

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

447 

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

448 
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

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

450 
end; 
0  451 

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

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

453 
fun matches tsig po = (match tsig po; true) handle MATCH => false; 
0  454 

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

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

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

457 
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

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

459 
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

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

461 
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

462 
 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

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

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

465 

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

466 
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

467 
 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

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

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

470 

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

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

472 
 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

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

474 
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

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

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

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

478 

12784  479 

480 
(* rewriting  simple but fast *) 

481 

13195  482 
fun rewrite_term tsig rules procs tm = 
12784  483 
let 
13195  484 
val skel0 = Bound 0; 
485 

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

13195  488 

12797  489 
fun variant_absfree (x, T, t) = 
490 
let 

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

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

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

494 

12784  495 
fun match_rew tm (tm1, tm2) = 
13195  496 
let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 
497 
in Some (subst_vars (match tsig (tm1, tm)) rtm, rtm) 

498 
handle MATCH => None 

499 
end; 

12784  500 

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

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

504 
 x => x); 

505 

506 
fun rew1 (Var _) _ = None 

507 
 rew1 skel tm = (case rew2 skel tm of 

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

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

511 
 None => (case rew tm of 
13195  512 
Some (tm1, skel') => Some (if_none (rew1 skel' tm1) tm1) 
12784  513 
 None => None)) 
514 

13195  515 
and rew2 skel (tm1 $ tm2) = (case tm1 of 
12784  516 
Abs (_, _, body) => 
517 
let val tm' = subst_bound (tm2, body) 

13195  518 
in Some (if_none (rew2 skel0 tm') tm') end 
519 
 _ => 

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

521 
skel1 $ skel2 => (skel1, skel2) 

522 
 _ => (skel0, skel0)) 

523 
in case rew1 skel1 tm1 of 

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

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

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

527 
 None => (case rew1 skel2 tm2 of 

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

529 
 None => None) 

530 
end) 

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

532 
let 

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

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

535 
in case rew1 skel' tm' of 

12797  536 
Some tm'' => Some (abs tm'') 
13195  537 
 None => None 
12797  538 
end 
13195  539 
 rew2 _ _ = None 
12784  540 

13195  541 
in if_none (rew1 skel0 tm) tm end; 
12784  542 

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

544 

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

545 
val trace_unify_fail = Pattern.trace_unify_fail; 