Unify Match/Unify modules #573
Conversation
Kontrol
|
library/Booster/Pattern/Rewrite.hs
Outdated
| | -- | A sort error was detected during unification | ||
| RewriteSortError (RewriteRule k) Term SortError | ||
| | -- | A sort error was detected during unification | ||
| InternalMatchError Text |
| , attributes = | ||
| SymbolAttributes | ||
| { collectionMetadata = Nothing | ||
| , symbolType = TotalFunction | ||
| , symbolType = Function Total | ||
| , isIdem = IsNotIdem | ||
| , isAssoc = IsNotAssoc |
There was a problem hiding this comment.
Maybe better to just re-generate (using the repl, and then slightly edit and auto-format) this definition. It is not up to date any more with the source.
There was a problem hiding this comment.
should re-think this maybe parsing kore via TH? I would leave out of the scope of this PR at any rate...
| | symbol1.name /= symbol2.name = | ||
| failWith | ||
| ( DifferentSymbols (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) | ||
| ) |
There was a problem hiding this comment.
This is a bit intricate... only correct with the invariant that we only call this case (with Rule) for ConsApplications.
Maybe we could merge the Rule and Fun cases for symbol1.name /= symbol2.name to make this more self-contained? (the Rule case shouldn't ever occur with function symbols, and would yield Indeterminate before)
| | -- mirrored case above: left list fully concrete, right one isn't | ||
| Nothing <- rest1 | ||
| , Just _ <- rest2 = | ||
| matchLists def heads2 rest2 heads1 rest1 -- won't loop, will fail later if unification succeeds |
There was a problem hiding this comment.
Not sure about this case...
Since the intent is matching this is probably bound to fail - the idea is that the pattern being fully concrete already means we cannot match a non-concrete list part in the subject but we might have to spell this out more explicitly.
There was a problem hiding this comment.
Yeah this was in the original unification code which appeared bidirectional, but we know this would eventually fail. Definitely should refactor, but maybe in a followup?
| >>= \case | ||
| Just newProblems -> | ||
| enqueueRegularProblems $ (Seq.fromList $ Map.elems commonMap) >< newProblems | ||
| Nothing -> pure () |
There was a problem hiding this comment.
What about the commonMap in this case?
There was a problem hiding this comment.
if we have a Nothing that means we added an indeterminate result, in which case I thought we don't want to continue anyway, unless we want to find more indeterminate cases in the commonMap, tho that just seems like busywork.
There was a problem hiding this comment.
Would there be cases where the commonMap elements still cause an outright failure to match (as opposed to being indeterminate)?
| data MapList | ||
| = ConstructorKey Term Term MapList | ||
| | Rest RestMapList | ||
|
|
||
| pattern SingleConstructorKey :: Term -> Term -> MapList | ||
| pattern SingleConstructorKey k v = ConstructorKey k v (Rest Empty) | ||
|
|
||
| pattern SingleOtherKey :: Term -> Term -> MapList | ||
| pattern SingleOtherKey k v = Rest (OtherKey k v Empty) |
There was a problem hiding this comment.
I would prefer if we didn't bring in a whole new map matching algorithm in the same PR as the refactoring.
It should be possble to port the existing matching/"unification" code without too many adaptations, then we can still rewrite the map-matching algorithm.
There was a problem hiding this comment.
unfortunately I tried a few times to make a frankenstein monster out of the existing two versions but could not get the tests to pass in both instances. I also found one or two tests that are just wrong and others that had to be oriented correctly for matching
There was a problem hiding this comment.
That being said, I have yet to run kevm/kontrol with this change so not too sure of it myself atm
There was a problem hiding this comment.
Hmm perhaps i will just keep the two copies for now and try to introduce this in the followup
| -- Check if term is a variable, prefer target variables. Should | ||
| -- not happen given how we call it in the code above. | ||
| Var var2 | ||
| | mType == Rule | ||
| && var2 `Set.member` targets | ||
| && not (var `Set.member` targets) -> | ||
| bindVariable mType var2 (Var var) |
There was a problem hiding this comment.
An assumption of the prior "unification" code... we should probably remove targets completely from the code and not care whether or not term is a variable.
| @@ -397,10 +399,12 @@ data RewriteFailed k | |||
| RuleConditionUnclear (RewriteRule k) Predicate | |||
| | -- | A rewrite rule does not preserve definedness | |||
| DefinednessUnclear (RewriteRule k) Pattern [NotPreservesDefinednessReason] | |||
| | -- | A unification produced a non-match substitution | |||
| | -- | A matching produced a non-match substitution | |||
| UnificationIsNotMatch (RewriteRule k) Term Substitution | |||
There was a problem hiding this comment.
Probably need to rename the UnificationIsNotMatch constructor to just IsNotMatch.
| match1 _ (AndTerm t1a t1b) t2@FunctionApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 | ||
| match1 Rewrite (AndTerm t1a t1b) t2@Var{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 | ||
| match1 Eval t1@AndTerm{} t2@Var{} = addIndeterminate t1 t2 | ||
| match1 Rewrite t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b |
There was a problem hiding this comment.
I like how this looks! I'd suggest a minor style change: let's add comments separating the groups of clauses for the different Term patterns:
| match1 Rewrite t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b | |
| -- DomainValue | |
| match1 Rewrite t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b |
| match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2 | ||
| match1 Rewrite t1@DomainValue{} (Var var2) = matchVar Rewrite var2 t1 | ||
| match1 Eval t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2 | ||
| match1 Rewrite t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b |
There was a problem hiding this comment.
As suggested above, consider adding spanners like this:
| match1 Rewrite t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b | |
| -- Injection | |
| match1 Rewrite t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b |
| ----- Symbol Applications | ||
| -- two constructors: fail if names differ, recurse | ||
|
|
||
| ----- Symbol Applications |
There was a problem hiding this comment.
| ----- Symbol Applications | |
| -- two constructors: fail if names differ, recurse | |
| ----- Symbol Applications | |
| ----- Symbol Applications |
| [] -> pure () | ||
| (k, _) : _ -> failWith $ DuplicateKeys k m | ||
| checkDuplicateKeys _ = pure () | ||
| matchMaps _ _ _ = undefined |
There was a problem hiding this comment.
This is probably an overlooked case, or should it "never happen"? Either way, probably a good idea to return indeterminate here.
There was a problem hiding this comment.
this is getting a refactor in the followup PR anyway
Fixes #3785 by merging the two versions of our matching algorithm, one used in matching rewrite rules and another matching function/simplification rules. This is a first pass which mostly just merges the two algorithms, prserving most of the divergent behaviour under the `Rewrite`/`Eval` `MatchType` flag. A followup refactor should clean up this code further. This PR is a port of runtimeverification/hs-backend-booster#573 where the development and testing happened. --------- Co-authored-by: github-actions <github-actions@github.com>
Will re-open in the haskell backend, just keeping this for the commit history for now
fixes runtimeverification/haskell-backend#3785