1(* Title: Pure/more_unify.ML 2 Author: Makarius 3 4Add-ons to Higher-Order Unification, outside the inference kernel. 5*) 6 7signature UNIFY = 8sig 9 include UNIFY 10 val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq 11 val matches_list: Context.generic -> term list -> term list -> bool 12end; 13 14structure Unify: UNIFY = 15struct 16 17(*Pattern matching*) 18fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) = 19 let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) 20 in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end 21 handle Pattern.MATCH => Seq.empty; 22 23(*General matching -- keep variables disjoint*) 24fun matchers _ [] = Seq.single Envir.init 25 | matchers context pairs = 26 let 27 val thy = Context.theory_of context; 28 29 val maxidx = fold (Term.maxidx_term o #2) pairs ~1; 30 val offset = maxidx + 1; 31 val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs; 32 val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; 33 34 val pat_tvars = fold (Term.add_tvars o #1) pairs' []; 35 val pat_vars = fold (Term.add_vars o #1) pairs' []; 36 37 val decr_indexesT = 38 Term.map_atyps (fn T as TVar ((x, i), S) => 39 if i > maxidx then TVar ((x, i - offset), S) else T | T => T); 40 val decr_indexes = 41 Term.map_types decr_indexesT #> 42 Term.map_aterms (fn t as Var ((x, i), T) => 43 if i > maxidx then Var ((x, i - offset), T) else t | t => t); 44 45 fun norm_tvar env ((x, i), S) = 46 let 47 val tyenv = Envir.type_env env; 48 val T' = Envir.norm_type tyenv (TVar ((x, i), S)); 49 in 50 if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE 51 else SOME ((x, i - offset), (S, decr_indexesT T')) 52 end; 53 54 fun norm_var env ((x, i), T) = 55 let 56 val tyenv = Envir.type_env env; 57 val T' = Envir.norm_type tyenv T; 58 val t' = Envir.norm_term env (Var ((x, i), T')); 59 in 60 if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE 61 else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t')) 62 end; 63 64 fun result env = 65 if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) 66 SOME (Envir.Envir {maxidx = maxidx, 67 tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars), 68 tenv = Vartab.make (map_filter (norm_var env) pat_vars)}) 69 else NONE; 70 71 val empty = Envir.empty maxidx'; 72 in 73 Seq.append 74 (Seq.map_filter result (Unify.smash_unifiers context pairs' empty)) 75 (first_order_matchers thy pairs empty) 76 end; 77 78fun matches_list context ps os = 79 length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os))); 80 81 82open Unify; 83 84end; 85 86