Kevin Kappelmann (Aug 26 2021 at 13:53): Kevin Kappelmann (Aug 26 2021 at 13:53):I am confused about the behaviour of Unify.unifiers in the following situation:
ML‹
val t =
Var (("v", 0), TFree ("'a", []) --> TFree ("'b", [])) $
Var (("w", 0), TFree ("'a", []))
val s =
Var (("x", 0), TFree ("'a", []) --> TFree ("'b", [])) $
Var (("y", 0), TFree ("'a", []))
(*returns empty environment and no unification error (unifying (t, s))*)
val env =
Unify.unifiers ((Context.the_generic_context ()), Envir.init, [(t,s)]) |> Seq.hd |> fst
(*returns correct unifier for (t, s')*)
val s' = (Var (("x", 0), TFree ("'b", [])))
val env' =
Unify.unifiers ((Context.the_generic_context ()), Envir.init, [(t, s')]) |> Seq.hd |> fst
›
how come that in the first case, an empty environment is returned?
Kevin Kappelmann (Sep 01 2021 at 13:11):Nevermind - I misinterpreted the way unifiersworks. I thought it returns a sequence of environments including instantiations for flex-flex pairs, but indeed it returns a sequence of environments including instantiations only for non-flex-flex cases and all remaining flex-flex instances in a separate list.
Last updated: Dec 30 2024 at 16:22 UTC