0

1 
(* Title: pattern


2 
ID: $Id$


3 
Author: Tobias Nipkow and Christine Heinzelmann, TU Muenchen


4 
Copyright 1993 TU Muenchen


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.


11 
*)


12 


13 
signature PATTERN =


14 
sig


15 
type type_sig


16 
type sg


17 
type env


18 
val eta_contract: term > term


19 
val match: type_sig > term * term


20 
> (indexname*typ)list * (indexname*term)list


21 
val eta_matches: type_sig > term * term > bool


22 
val unify: sg * env * (term * term)list > env


23 
exception Unif


24 
exception MATCH


25 
exception Pattern


26 
end;


27 


28 
functor PatternFun(structure Sign:SIGN and Envir:ENVIR): PATTERN =


29 
struct


30 


31 
structure Type = Sign.Type;


32 


33 
type type_sig = Type.type_sig


34 
type sg = Sign.sg


35 
type env = Envir.env


36 


37 
exception Unif;


38 
exception Pattern;


39 


40 
fun occurs(F,t,env) =


41 
let fun occ(Var(G,_)) = (case Envir.lookup(env,G) of


42 
Some(t) => occ t


43 
 None => F=G)


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


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


46 
 occ _ = false


47 
in occ t end;


48 


49 
(* Something's wrong *)


50 
fun ill_formed s = error ("Illformed argument in "^s);


51 


52 


53 
fun mapbnd f =


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


55 
 mpb d (Free(c,T)) = Free(c,T)


56 
 mpb d (Const(c,T)) = Const(c,T)


57 
 mpb d (Var(iname,T)) = Var(iname,T)


58 
 mpb d (Abs(s,T,t)) = Abs(s,T,mpb(d+1) t)


59 
 mpb d ((u1 $ u2)) = mpb d (u1)$ mpb d (u2)


60 
in mpb 0 end;


61 


62 
fun idx [] j = ~10000


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


64 


65 
val nth_type = snd o nth_elem;


66 


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


68 


69 
fun mkabs (binders,is,t) =


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


71 
in Abs(x,T,mk is) end


72 
 mk [] = t


73 
in mk is end;


74 


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


76 


77 
(* termlist > intlist *)


78 
fun ints_of [] = []


79 
 ints_of (Bound i ::bs) =


80 
let val is = ints_of bs


81 
in if i mem is then raise Pattern else i::is end


82 
 ints_of _ = raise Pattern;


83 


84 


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


86 
 app (s,[]) = s;


87 


88 
fun red (Abs(_,_,s)) (i::is) js = red s is (i::js)


89 
 red s is jn = app (mapbnd (at jn) s,is);


90 


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


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


93 
 split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n1,T1::Ts)


94 
 split_type _ = ill_formed("split_type");


95 


96 
fun type_of_G (T,n,is) =


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


98 


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


100 


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


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


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


104 


105 


106 
fun devar env t = case strip_comb t of


107 
(Var(F,_),ys) =>


108 
(case Envir.lookup(env,F) of


109 
Some(t) => devar env (red t (ints_of ys) [])


110 
 None => t)


111 
 _ => t;


112 


113 


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


115 
fun mk_proj_list is =


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


117 
 mk([],_) = []


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


119 


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


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


122 
fun pr(s,env,d,binders) = (case devar env s of


123 
Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders))


124 
in (Abs(a,T,t'),env') end


125 
 t => (case strip_comb t of


126 
(c as Const _,ts) =>


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


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


129 
 (f as Free _,ts) =>


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


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


132 
 (Bound(i),ts) =>


133 
let val j = trans d i


134 
in if j < 0 then raise Unif


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


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


137 
end


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


139 
let val js = ints_of ts;


140 
val js' = map (trans d) js;


141 
val ks = mk_proj_list js';


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


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


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


145 
val env'' =


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


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


148 
 _ => raise Pattern))


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


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


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


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


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


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


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


156 
end;


157 


158 


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


160 
fun mk_ff_list(is,js) =


161 
let fun mk([],[],_) = []


162 
 mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k1)


163 
else mk(is,js,k1)


164 
 mk _ = ill_formed"mk_ff_list"


165 
in mk(is,js,length is1) end;


166 


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


168 
if is=js then env


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


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


171 


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


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


174 
if js subset is


175 
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))


176 
in Envir.update((F,t),env) end


177 
else let val ks = is inter js


178 
val Hty = type_of_G(Fty,length is,map (idx is) ks)


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


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


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


182 
end;


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


184 


185 
val tsgr = ref(Type.tsig0);


186 


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


188 
if T=U then env


189 
else let val iTs' = Type.unify (!tsgr) ((U,T),iTs)


190 
in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'} end


191 
handle Type.TUNIFY => raise Unif;


192 


193 
fun unif binders (env,(s,t)) = case (devar env s,devar env t) of


194 
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>


195 
let val name = if ns = "" then nt else ns


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


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


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


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


200 


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


202 
((Var(F,Fty),ss),(Var(G,Gty),ts)) =>


203 
if F = G then flexflex1(env,binders,F,Fty,ints_of ss,ints_of ts)


204 
else flexflex2(env,binders,F,Fty,ints_of ss,G,Gty,ints_of ts)


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


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


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


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


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


210 
 ((Abs(_),_),_) => raise Pattern


211 
 (_,(Abs(_),_)) => raise Pattern


212 
 _ => raise Unif


213 


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


215 
if a<>b then raise Unif


216 
else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts)


217 


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


219 
if i <> j then raise Unif else foldl (unif binders) (env ,ss~~ts)


220 


221 
and flexrigid (env,binders,F,is,t) =


222 
if occurs(F,t,env) then raise Unif


223 
else let val (u,env') = proj(t,env,binders,is)


224 
in Envir.update((F,mkabs(binders,is,u)),env') end;


225 


226 
fun unify(sg,env,tus) = (tsgr := #tsig(Sign.rep_sg sg);


227 
foldl (unif []) (env,tus));


228 


229 


230 
(*Perform etacontractions upon a term*)


231 
fun eta_contract (Abs(a,T,body)) =


232 
(case eta_contract body of


233 
body' as (f $ Bound i) =>


234 
if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f


235 
else Abs(a,T,body')


236 
 body' => Abs(a,T,body'))


237 
 eta_contract(f$t) = eta_contract f $ eta_contract t


238 
 eta_contract t = t;


239 


240 


241 
(* Pattern matching. Raises MATCH if nonpattern *)


242 
exception MATCH;


243 
(* something wron with types, esp in abstractions


244 
fun typ_match args = Type.typ_match (!tsgr) args


245 
handle Type.TYPE_MATCH => raise MATCH;


246 


247 
fun match_bind(itms,binders,ixn,is,t) =


248 
let val js = loose_bnos t


249 
in if null is


250 
then if null js then (ixn,t)::itms else raise MATCH


251 
else if js subset is


252 
then let val t' = if downto0(is,length binders  1) then t


253 
else mapbnd (idx is) t


254 
in (ixn, eta_contract(mkabs(binders,is,t'))) :: itms end


255 
else raise MATCH


256 
end;


257 


258 
fun match_rr (iTs,(a,Ta),(b,Tb)) =


259 
if a<>b then raise MATCH else typ_match (iTs,(Ta,Tb))


260 


261 
(* Pre: pat and obj have same type *)


262 
fun mtch(binders,env as (iTs,itms),pat,obj) = case pat of


263 
Var(ixn,_) => (case assoc(itms,ixn) of


264 
None => (iTs,match_bind(itms,binders,ixn,[],obj))


265 
 Some u => if obj aconv u then env else raise MATCH)


266 
 Abs(ns,Ts,ts) =>


267 
(case obj of


268 
Abs(nt,Tt,tt) => mtch((nt,Tt)::binders,env,ts,tt)


269 
 _ => let val Tt = typ_subst_TVars iTs Ts


270 
in mtch((ns,Tt)::binders,env,ts,(incr obj)$Bound(0)) end)


271 
 _ => (case obj of


272 
Abs(nt,Tt,tt) =>


273 
mtch((nt,Tt)::binders,env,(incr pat)$Bound(0),tt)


274 
 _ => cases(binders,env,pat,obj))


275 


276 
and cases(binders,env as (iTs,itms),pat,obj) =


277 
let fun structural() = case (pat,obj) of


278 
(Const c,Const d) => (match_rr(iTs,c,d),itms)


279 
 (Free f,Free g) => (match_rr(iTs,f,g),itms)


280 
 (Bound i,Bound j) => if i=j then env else raise MATCH


281 
 (f$t,g$u) => mtch(binders,mtch(binders,env,t,u),f,g)


282 
 _ => raise MATCH


283 
in case strip_comb pat of


284 
(Var(ixn,_),bs) =>


285 
(let val is = ints_of bs


286 
in case assoc(itms,ixn) of


287 
None => (iTs,match_bind(itms,binders,ixn,is,obj))


288 
 Some u => if obj aconv (red u is []) then env else raise MATCH


289 
end (* if ints_of fails: *) handle Pattern => structural())


290 
 _ => structural()


291 
end;


292 


293 
fun match tsg = (tsgr := tsg;


294 
fn (pat,obj) =>

63

295 
let val pT = fastype_of pat


296 
and oT = fastype_of obj


297 
val iTs = typ_match ([],(pT,oT))

0

298 
in mtch([], (iTs,[]), pat, eta_contract obj)


299 
handle Pattern => raise MATCH


300 
end)


301 


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


303 
fun matches tsig args = (match tsig args; true)


304 
handle MATCH => false;


305 
*)


306 


307 
(*Firstorder matching; term_match tsig (pattern, object)


308 
returns a (tyvar,typ)list and (var,term)list.


309 
The pattern and object may have variables in common.


310 
Instantiation does not affect the object, so matching ?a with ?a+1 works.


311 
A Const does not match a Free of the same name!


312 
Does not notice etaequality, thus f does not match %(x)f(x) *)


313 
fun match tsig (pat,obj) =


314 
let fun typ_match args = (Type.typ_match tsig args)


315 
handle Type.TYPE_MATCH => raise MATCH;


316 
fun mtch (tyinsts,insts) = fn


317 
(Var(ixn,T), t) =>


318 
if null (loose_bnos t)


319 
then case assoc(insts,ixn) of

63

320 
None => (typ_match (tyinsts, (T, fastype_of t)),

0

321 
(ixn,t)::insts)


322 
 Some u => if t aconv u then (tyinsts,insts) else raise MATCH


323 
else raise MATCH


324 
 (Free (a,T), Free (b,U)) =>


325 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH


326 
 (Const (a,T), Const (b,U)) =>


327 
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH


328 
 (Bound i, Bound j) =>


329 
if i=j then (tyinsts,insts) else raise MATCH


330 
 (Abs(_,T,t), Abs(_,U,u)) =>


331 
mtch (typ_match (tyinsts,(T,U)),insts) (t,u)


332 
 (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u)


333 
 _ => raise MATCH


334 
in mtch([],[]) (pat,obj) end;


335 


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


337 
fun eta_matches tsig (pat,obj) =


338 
(match tsig (eta_contract pat,eta_contract obj); true)


339 
handle MATCH => false;


340 


341 
end;
