checkSubstitutionCoverage: check for constructor-like configuration (#2015)

* First attempt

* Check for constructor-like configuration

* Update golden

* Addressed comments

* Add integration test

Author: andreiburdusa

kore/src/Kore/Log/ErrorRewritesInstantiation.hs

@@ -15,8 +15,6 @@ import Control.Exception
     ( Exception (..)
     , throw
     )
-import qualified Data.Foldable as Foldable
-import qualified Data.Map.Strict as Map
 import Data.Set
     ( Set
     )
@@ -40,7 +38,9 @@ import Kore.Internal.Conditional
 import Kore.Internal.Pattern
     ( Pattern
     )
-import qualified Kore.Internal.Substitution as Substitution
+import Kore.Internal.TermLike
+    ( isConstructorLike
+    )
 import Kore.Internal.Variable
     ( SomeVariableName
     )
@@ -158,8 +158,6 @@ checkSubstitutionCoverage configuration solution
     substitutionCoverageError =
         SubstitutionCoverageError { solution, missingVariables }
 
-    Conditional { substitution } = solution
-    substitutionVariables = Map.keysSet (Substitution.toMap substitution)
     missingVariables = wouldNarrowWith solution
     isCoveringSubstitution = Set.null missingVariables
-    isSymbolic = Foldable.any isSomeConfigVariableName substitutionVariables
+    isSymbolic = (not . isConstructorLike) (term configuration)

test/imp/disjunction-in-simplification-spec.k

@@ -0,0 +1 @@
+f()

test/imp/disjunction-in-simplification-spec.k.out.golden

@@ -0,0 +1,3 @@
+<k>
+  I:Int ~> .
+</k>

test/issue-2010/1.test

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

test/issue-2010/1.test.out.golden

@@ -0,0 +1,13 @@
+module TEST
+    imports BOOL
+    imports INT
+
+    syntax MaybeInt ::= "Some" Int
+                      | "None"
+    syntax MaybeInt ::= f() [function, functional, no-evaluators]
+
+    configuration <k> f() </k>
+
+    rule <k> None => true ... </k>
+    rule <k> Some I => I ... </k>
+endmodule