Add HasCallStack constraints (#506)

* Kore.AST.Valid: Add HasCallStack constraints * freeEpVariables: Avoid calling toMLPattern
runtimeverification · Mar 14, 2019 · b132659 · b132659
1 parent 425e5ea
commit b132659
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 10 deletions.
diff --git a/kore/src/Kore/AST/Valid.hs b/kore/src/Kore/AST/Valid.hs
@@ -103,6 +103,8 @@ import qualified Data.Set as Set
 import           Data.Text
                  ( Text )
 import           Data.These
+import           GHC.Stack
+                 ( HasCallStack )
 
 import           Kore.Annotation.Valid as Valid
 import           Kore.AST.Lens
@@ -125,6 +127,7 @@ getSort (extract -> Valid { patternSort }) = patternSort
 forceSort
     ::  ( Traversable domain
         , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
         )
@@ -226,9 +229,10 @@ same sort.
  -}
 makeSortsAgree
     ::  ( Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
-        , Unparse pattern'
         )
     => (pattern' -> pattern' -> Sort level -> a)
     -> pattern'
@@ -262,9 +266,10 @@ getRigidSort pattern' =
 mkAnd
     ::  ( Ord (variable level)
         , Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
-        , Unparse pattern'
         )
     => pattern'
     -> pattern'
@@ -345,6 +350,7 @@ applyAlias
     ::  ( Traversable domain
         , Ord (variable level)
         , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
         )
@@ -713,9 +719,10 @@ mkForall forallVariable forallChild =
 mkIff
     ::  ( Ord (variable level)
         , Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
-        , Unparse pattern'
         )
     => pattern'
     -> pattern'
@@ -738,9 +745,10 @@ mkIff = makeSortsAgree mkIffWorker
 mkImplies
     ::  ( Ord (variable level)
         , Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
-        , Unparse pattern'
         )
     => pattern'
     -> pattern'
@@ -766,9 +774,10 @@ See also: 'mkIn_'
 mkIn
     ::  ( Ord (variable level)
         , Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
-        , Unparse pattern'
         )
     => Sort level
     -> pattern'
@@ -850,9 +859,10 @@ mkNot notChild =
 mkOr
     ::  ( Ord (variable level)
         , Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable level) level
         , pattern' ~ PurePattern level domain variable valid
-        , Unparse pattern'
         )
     => pattern'
     -> pattern'
@@ -875,9 +885,10 @@ mkOr = makeSortsAgree mkOrWorker
 mkRewrites
     ::  ( Ord (variable Object)
         , Traversable domain
+        , Unparse pattern'
+        , HasCallStack
         , valid ~ Valid (variable Object) Object
         , pattern' ~ PurePattern Object domain variable valid
-        , Unparse pattern'
         )
     => pattern'
     -> pattern'

diff --git a/kore/src/Kore/Predicate/Predicate.hs b/kore/src/Kore/Predicate/Predicate.hs
@@ -54,6 +54,8 @@ import           Data.Set
                  ( Set )
 import           GHC.Generics
                  ( Generic )
+import           GHC.Stack
+                 ( HasCallStack )
 
 import           Kore.AST.Pure
 import           Kore.AST.Valid
@@ -141,7 +143,9 @@ the resulting pattern into a particular sort.
 
  -}
 fromPredicate
-    :: Unparse (variable level)
+    :: ( Unparse (variable level)
+       , HasCallStack
+       )
     => Sort level  -- ^ Sort of resulting pattern
     -> Predicate level variable
     -> StepPattern level variable

diff --git a/kore/src/Kore/Step/Representation/ExpandedPattern.hs b/kore/src/Kore/Step/Representation/ExpandedPattern.hs
@@ -48,6 +48,8 @@ import qualified Data.Set as Set
 import qualified Data.Text.Prettyprint.Doc as Pretty
 import           GHC.Generics
                  ( Generic )
+import           GHC.Stack
+                 ( HasCallStack )
 
 import           Kore.Annotation.Valid
 import           Kore.AST.Pure
@@ -241,8 +243,9 @@ freeEpVariables
        )
     => ExpandedPattern level variable
     -> Set.Set (variable level)
-freeEpVariables =
-    freePureVariables . toMLPattern
+freeEpVariables ep@Predicated { term } =
+    freePureVariables term
+    <> Kore.Step.Representation.ExpandedPattern.freeVariables ep { term = () }
 
 -- | Erase the @Predicated@ 'term' to yield a 'PredicateSubstitution'.
 erasePredicatedTerm
@@ -259,6 +262,7 @@ toMLPattern
         , Ord (variable level)
         , Show (variable level)
         , Unparse (variable level)
+        , HasCallStack
         )
     => ExpandedPattern level variable -> StepPattern level variable
 toMLPattern