src/Pure/unify.ML
changeset 20020 9e7d3d06c643
parent 19920 8257e52164a1
child 20083 717b1eb434f1
equal deleted inserted replaced
20019:283dfd5bd36b 20020:9e7d3d06c643
   613 fun smash_unifiers thy tus env =
   613 fun smash_unifiers thy tus env =
   614     Seq.map smash_flexflex (unifiers(thy,env,tus));
   614     Seq.map smash_flexflex (unifiers(thy,env,tus));
   615 
   615 
   616 
   616 
   617 (*Pattern matching*)
   617 (*Pattern matching*)
   618 fun pattern_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
   618 fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
   619   let val (tyenv', tenv') = fold (Pattern.match thy) pairs (tyenv, tenv)
   619   let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
   620   in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
   620   in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
   621   handle Pattern.MATCH => Seq.empty;
   621   handle Pattern.MATCH => Seq.empty;
   622 
   622 
   623 (*General matching -- keeps variables disjoint*)
   623 (*General matching -- keeps variables disjoint*)
   624 fun matchers _ [] = Seq.single (Envir.empty ~1)
   624 fun matchers _ [] = Seq.single (Envir.empty ~1)
   657 
   657 
   658         val empty = Envir.empty maxidx';
   658         val empty = Envir.empty maxidx';
   659       in
   659       in
   660         Seq.append
   660         Seq.append
   661           (Seq.map_filter result (smash_unifiers thy pairs' empty))
   661           (Seq.map_filter result (smash_unifiers thy pairs' empty))
   662           (pattern_matchers thy pairs empty)
   662           (first_order_matchers thy pairs empty)
   663       end;
   663       end;
   664 
   664 
   665 fun matches_list thy ps os =
   665 fun matches_list thy ps os =
   666   length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
   666   length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
   667 
   667