1(* Title: Pure/pattern.ML 2 Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen 3 4Unification of Higher-Order Patterns. 5 6See also: 7Tobias Nipkow. Functional Unification of Higher-Order Patterns. 8In Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993. 9 10TODO: optimize red by special-casing it 11*) 12 13signature PATTERN = 14sig 15 exception Unif 16 exception Pattern 17 val unify_trace_failure: bool Config.T 18 val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env 19 val unify: Context.generic -> term * term -> Envir.env -> Envir.env 20 exception MATCH 21 val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv 22 val first_order_match: theory -> term * term 23 -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv 24 val pattern: term -> bool 25end; 26 27structure Pattern: PATTERN = 28struct 29 30exception Unif; 31exception Pattern; 32 33val unify_trace_failure = Config.declare_bool ("unify_trace_failure", \<^here>) (K false); 34 35fun string_of_term ctxt env binders t = 36 Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t))); 37 38fun bname binders i = fst (nth binders i); 39fun bnames binders is = space_implode " " (map (bname binders) is); 40 41fun typ_clash context (tye,T,U) = 42 if Config.get_generic context unify_trace_failure then 43 let 44 val ctxt = Context.proof_of context; 45 val t = Syntax.string_of_typ ctxt (Envir.norm_type tye T); 46 val u = Syntax.string_of_typ ctxt (Envir.norm_type tye U); 47 in tracing ("The following types do not unify:\n" ^ t ^ "\n" ^ u) end 48 else (); 49 50fun clash context a b = 51 if Config.get_generic context unify_trace_failure 52 then tracing ("Clash: " ^ a ^ " =/= " ^ b) else (); 53 54fun boundVar binders i = 55 "bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")"; 56 57fun clashBB context binders i j = 58 if Config.get_generic context unify_trace_failure 59 then clash context (boundVar binders i) (boundVar binders j) else (); 60 61fun clashB context binders i s = 62 if Config.get_generic context unify_trace_failure 63 then clash context (boundVar binders i) s else (); 64 65fun proj_fail context (env,binders,F,_,is,t) = 66 if Config.get_generic context unify_trace_failure then 67 let 68 val ctxt = Context.proof_of context 69 val f = Term.string_of_vname F 70 val xs = bnames binders is 71 val u = string_of_term ctxt env binders t 72 val ys = bnames binders (subtract (op =) is (loose_bnos t)) 73 in 74 tracing ("Cannot unify variable " ^ f ^ 75 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^ 76 "\nTerm contains additional bound variable(s) " ^ ys) 77 end 78 else (); 79 80fun ocheck_fail context (F,t,binders,env) = 81 if Config.get_generic context unify_trace_failure then 82 let 83 val ctxt = Context.proof_of context 84 val f = Term.string_of_vname F 85 val u = string_of_term ctxt env binders t 86 in tracing ("Variable " ^ f ^ " occurs in term\n" ^ u ^ "\nCannot unify!\n") end 87 else (); 88 89fun occurs(F,t,env) = 90 let fun occ(Var (G, T)) = (case Envir.lookup env (G, T) of 91 SOME(t) => occ t 92 | NONE => F=G) 93 | occ(t1$t2) = occ t1 orelse occ t2 94 | occ(Abs(_,_,t)) = occ t 95 | occ _ = false 96 in occ t end; 97 98 99fun mapbnd f = 100 let fun mpb d (Bound(i)) = if i < d then Bound(i) else Bound(f(i-d)+d) 101 | mpb d (Abs(s,T,t)) = Abs(s,T,mpb(d+1) t) 102 | mpb d ((u1 $ u2)) = (mpb d u1)$(mpb d u2) 103 | mpb _ atom = atom 104 in mpb 0 end; 105 106fun idx [] j = raise Unif 107 | idx(i::is) j = if (i:int) =j then length is else idx is j; 108 109fun mkabs (binders,is,t) = 110 let fun mk(i::is) = let val (x,T) = nth binders i 111 in Abs(x,T,mk is) end 112 | mk [] = t 113 in mk is end; 114 115val incr = mapbnd (fn i => i+1); 116 117fun ints_of [] = [] 118 | ints_of (Bound i ::bs) = 119 let val is = ints_of bs 120 in if member (op =) is i then raise Pattern else i::is end 121 | ints_of _ = raise Pattern; 122 123fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); 124 125 126fun app (s,(i::is)) = app (s$Bound(i),is) 127 | app (s,[]) = s; 128 129fun red (Abs(_,_,s)) (i::is) js = red s is (i::js) 130 | red t [] [] = t 131 | red t is jn = app (mapbnd (nth jn) t,is); 132 133 134(* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *) 135fun split_type (T,0,Ts) = (Ts,T) 136 | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) 137 | split_type _ = raise Fail "split_type"; 138 139fun type_of_G env (T, n, is) = 140 let 141 val tyenv = Envir.type_env env; 142 val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []); 143 in map (nth Ts) is ---> U end; 144 145fun mk_hnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); 146 147fun mk_new_hnf(env,binders,is,F as (a,_),T,js) = 148 let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js)) 149 in Envir.update ((F, T), mk_hnf (binders, is, G, js)) env' end; 150 151 152(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*) 153fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1) 154 | downto0 ([], n) = n = ~1; 155 156(*mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ]*) 157fun mk_proj_list is = 158 let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1) 159 | mk([],_) = [] 160 in mk(is,length is - 1) end; 161 162fun proj(s,env,binders,is) = 163 let fun trans d i = if i<d then i else (idx is (i-d))+d; 164 fun pr(s,env,d,binders) = (case Envir.head_norm env s of 165 Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders)) 166 in (Abs(a,T,t'),env') end 167 | t => (case strip_comb t of 168 (c as Const _,ts) => 169 let val (ts',env') = prs(ts,env,d,binders) 170 in (list_comb(c,ts'),env') end 171 | (f as Free _,ts) => 172 let val (ts',env') = prs(ts,env,d,binders) 173 in (list_comb(f,ts'),env') end 174 | (Bound(i),ts) => 175 let val j = trans d i 176 val (ts',env') = prs(ts,env,d,binders) 177 in (list_comb(Bound j,ts'),env') end 178 | (Var(F as (a,_),Fty),ts) => 179 let val js = ints_of' env ts; 180 val js' = map (try (trans d)) js; 181 val ks = mk_proj_list js'; 182 val ls = map_filter I js' 183 val Hty = type_of_G env (Fty,length js,ks) 184 val (env',H) = Envir.genvar a (env,Hty) 185 val env'' = 186 Envir.update ((F, Fty), mk_hnf (binders, js, H, ks)) env' 187 in (app(H,ls),env'') end 188 | _ => raise Pattern)) 189 and prs(s::ss,env,d,binders) = 190 let val (s',env1) = pr(s,env,d,binders) 191 val (ss',env2) = prs(ss,env1,d,binders) 192 in (s'::ss',env2) end 193 | prs([],env,_,_) = ([],env) 194 in if downto0(is,length binders - 1) then (s,env) 195 else pr(s,env,0,binders) 196 end; 197 198 199(* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *) 200fun mk_ff_list(is,js) = 201 let fun mk([],[],_) = [] 202 | mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1) 203 else mk(is,js,k-1) 204 | mk _ = raise Fail "mk_ff_list" 205 in mk(is,js,length is-1) end; 206 207fun flexflex1(env,binders,F,Fty,is,js) = 208 if is=js then env 209 else let val ks = mk_ff_list(is,js) 210 in mk_new_hnf(env,binders,is,F,Fty,ks) end; 211 212fun flexflex2(env,binders,F,Fty,is,G,Gty,js) = 213 let fun ff(F,Fty,is,G as (a,_),Gty,js) = 214 if subset (op =) (js, is) 215 then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js)) 216 in Envir.update ((F, Fty), t) env end 217 else let val ks = inter (op =) js is 218 val Hty = type_of_G env (Fty,length is,map (idx is) ks) 219 val (env',H) = Envir.genvar a (env,Hty) 220 fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); 221 in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env') 222 end; 223 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 224 225fun unify_types context (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = 226 if T = U then env 227 else 228 let 229 val thy = Context.theory_of context 230 val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) 231 in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end 232 handle Type.TUNIFY => (typ_clash context (tyenv, T, U); raise Unif); 233 234fun unif context binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of 235 (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => 236 let val name = if ns = "" then nt else ns 237 in unif context ((name,Ts)::binders) (ts,tt) (unify_types context (Ts, Tt) env) end 238 | (Abs(ns,Ts,ts),t) => unif context ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env 239 | (t,Abs(nt,Tt,tt)) => unif context ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env 240 | p => cases context (binders,env,p) 241 242and cases context (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of 243 ((Var(F,Fty),ss),(Var(G,Gty),ts)) => 244 if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) 245 else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) 246 | ((Var(F,Fty),ss),_) => flexrigid context (env,binders,F,Fty,ints_of' env ss,t) 247 | (_,(Var(F,Fty),ts)) => flexrigid context (env,binders,F,Fty,ints_of' env ts,s) 248 | ((Const c,ss),(Const d,ts)) => rigidrigid context (env,binders,c,d,ss,ts) 249 | ((Free(f),ss),(Free(g),ts)) => rigidrigid context (env,binders,f,g,ss,ts) 250 | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB context (env,binders,i,j,ss,ts) 251 | ((Abs(_),_),_) => raise Pattern 252 | (_,(Abs(_),_)) => raise Pattern 253 | ((Const(c,_),_),(Free(f,_),_)) => (clash context c f; raise Unif) 254 | ((Const(c,_),_),(Bound i,_)) => (clashB context binders i c; raise Unif) 255 | ((Free(f,_),_),(Const(c,_),_)) => (clash context f c; raise Unif) 256 | ((Free(f,_),_),(Bound i,_)) => (clashB context binders i f; raise Unif) 257 | ((Bound i,_),(Const(c,_),_)) => (clashB context binders i c; raise Unif) 258 | ((Bound i,_),(Free(f,_),_)) => (clashB context binders i f; raise Unif) 259 260 261and rigidrigid context (env,binders,(a,Ta),(b,Tb),ss,ts) = 262 if a<>b then (clash context a b; raise Unif) 263 else env |> unify_types context (Ta,Tb) |> fold (unif context binders) (ss~~ts) 264 265and rigidrigidB context (env,binders,i,j,ss,ts) = 266 if i <> j then (clashBB context binders i j; raise Unif) 267 else fold (unif context binders) (ss~~ts) env 268 269and flexrigid context (params as (env,binders,F,Fty,is,t)) = 270 if occurs(F,t,env) then (ocheck_fail context (F,t,binders,env); raise Unif) 271 else (let val (u,env') = proj(t,env,binders,is) 272 in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end 273 handle Unif => (proj_fail context params; raise Unif)); 274 275fun unify context = unif context []; 276 277 278 279(*** Matching ***) 280 281exception MATCH; 282 283fun typ_match thy TU tyenv = Sign.typ_match thy TU tyenv 284 handle Type.TYPE_MATCH => raise MATCH; 285 286(*First-order matching; 287 The pattern and object may have variables in common. 288 Instantiation does not affect the object, so matching ?a with ?a+1 works. 289 Object is eta-contracted on the fly (by eta-expanding the pattern). 290 Precondition: the pattern is already eta-contracted! 291 Types are matched on the fly. 292 The parameter inAbs is an optimization to avoid calling is_open; 293 it has the funny consequence that outside abstractions 294 ?x matches terms containing loose Bounds. 295*) 296fun first_order_match thy = 297 let 298 fun mtch inAbs (instsp as (tyinsts,insts)) = fn 299 (Var(ixn,T), t) => 300 if inAbs andalso Term.is_open t then raise MATCH 301 else (case Envir.lookup1 insts (ixn, T) of 302 NONE => (typ_match thy (T, fastype_of t) tyinsts, 303 Vartab.update_new (ixn, (T, t)) insts) 304 | SOME u => if Envir.aeconv (t, u) then instsp else raise MATCH) 305 | (Free (a,T), Free (b,U)) => 306 if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH 307 | (Const (a,T), Const (b,U)) => 308 if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH 309 | (Bound i, Bound j) => if i=j then instsp else raise MATCH 310 | (Abs(_,T,t), Abs(_,U,u)) => 311 mtch true (typ_match thy (T,U) tyinsts, insts) (t,u) 312 | (f$t, g$u) => mtch inAbs (mtch inAbs instsp (f,g)) (t, u) 313 | (t, Abs(_,U,u)) => mtch true instsp ((incr t)$(Bound 0), u) 314 | _ => raise MATCH 315 in fn tu => fn env => mtch false env tu end; 316 317 318(* Matching of higher-order patterns *) 319 320fun match_bind(itms,binders,ixn,T,is,t) = 321 let val js = loose_bnos t 322 in if null is 323 then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH 324 else if subset (op =) (js, is) 325 then let val t' = if downto0(is,length binders - 1) then t 326 else mapbnd (idx is) t 327 in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end 328 else raise MATCH 329 end; 330 331fun match thy (po as (pat,obj)) envir = 332let 333 (* Pre: pat and obj have same type *) 334 fun mtch binders (pat,obj) (env as (iTs,itms)) = 335 case pat of 336 Abs(ns,Ts,ts) => 337 (case obj of 338 Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env 339 | _ => let val Tt = Envir.subst_type iTs Ts 340 in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end) 341 | _ => (case obj of 342 Abs(nt,Tt,tt) => 343 mtch((nt,Tt)::binders) ((incr pat)$Bound(0),tt) env 344 | _ => cases(binders,env,pat,obj)) 345 346 and cases(binders,env as (iTs,itms),pat,obj) = 347 let val (ph,pargs) = strip_comb pat 348 fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms) 349 handle ListPair.UnequalLengths => raise MATCH 350 fun rigrig2((a:string,Ta),(b,Tb),oargs) = 351 if a <> b then raise MATCH 352 else rigrig1(typ_match thy (Ta,Tb) iTs, oargs) 353 in case ph of 354 Var(ixn,T) => 355 let val is = ints_of pargs 356 in case Envir.lookup1 itms (ixn, T) of 357 NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj)) 358 | SOME u => if Envir.aeconv (obj, red u is []) then env 359 else raise MATCH 360 end 361 | _ => 362 let val (oh,oargs) = strip_comb obj 363 in case (ph,oh) of 364 (Const c,Const d) => rigrig2(c,d,oargs) 365 | (Free f,Free g) => rigrig2(f,g,oargs) 366 | (Bound i,Bound j) => if i<>j then raise MATCH 367 else rigrig1(iTs,oargs) 368 | (Abs _, _) => raise Pattern 369 | (_, Abs _) => raise Pattern 370 | _ => raise MATCH 371 end 372 end; 373 374 val pT = fastype_of pat 375 and oT = fastype_of obj 376 val envir' = apfst (typ_match thy (pT, oT)) envir; 377in mtch [] po envir' handle Pattern => first_order_match thy po envir' end; 378 379 380fun pattern (Abs (_, _, t)) = pattern t 381 | pattern t = 382 let val (head, args) = strip_comb t in 383 if is_Var head then 384 forall is_Bound args andalso not (has_duplicates (op aconv) args) 385 else forall pattern args 386 end; 387end; 388