search

kframework / matching-logic-prover

15 stars 4 forks source link

Matchig variables - duplicated rule #48

Open h0nzZik opened 4 years ago

h0nzZik commented 4 years ago

In strategies/matching.md, there are two rules for the same case:

// ground variable: mismatched
  rule #matchAssoc( terms:     T, Ts
                  , pattern:   P:Variable, Ps
                  , variables: Vs
                  , subst:     SUBST
                  , rest:      REST
                  )
    => #matchFailure("Variable does not match"), .MatchResults
    requires T =/=K P
     andBool notBool P in Vs

and

// ground variable: non-identical
  rule #matchAssoc( terms:     T, Ts
                  , pattern:   P:Variable, Ps
                  , variables: Vs
                  , subst:     _
                  , rest:      REST
                  )
    => #matchFailure( "No valid substitution" ), .MatchResults
    requires T =/=K P
     andBool notBool P in Vs

. Since syntacticMatch from utils/syntactic-match.md originated as a copy of #matchAssoc, the duplication is also there.