Change the representation of reachability claims, part 1

kore/src/Kore/Internal/Conditional.hs

@@ -32,6 +32,9 @@ import Prelude.Kore
 import Control.DeepSeq
     ( NFData
     )
+import Data.Map.Strict
+    ( Map
+    )
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
@@ -245,6 +248,16 @@ instance
   where
     from = pure
 
+instance
+    InternalVariable variable
+    => From (Map (SomeVariable variable) (TermLike variable)) (Conditional variable ())
+  where
+    from =
+        from @(Substitution variable) @(Conditional variable ())
+        . from
+            @(Map (SomeVariable variable) (TermLike variable))
+            @(Substitution variable)
+
 unparseConditional
     :: Sort
     -> Doc ann    -- ^ term

kore/src/Kore/Internal/OrPattern.hs

@@ -20,6 +20,8 @@ module Kore.Internal.OrPattern
     , toPattern
     , toTermLike
     , targetBinder
+    , substitute
+    , parseFromTermLike
     , MultiOr.flatten
     , MultiOr.filterOr
     , MultiOr.gather
@@ -29,6 +31,9 @@ module Kore.Internal.OrPattern
 import Prelude.Kore
 
 import qualified Data.Foldable as Foldable
+import Data.Map.Strict
+    ( Map
+    )
 
 import Kore.Internal.Condition
     ( Condition
@@ -52,6 +57,7 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
     )
 import Kore.Internal.TermLike
     ( InternalVariable
+    , pattern Or_
     , Sort
     , TermLike
     , mkBottom_
@@ -219,3 +225,19 @@ targetBinder Binder { binderVariable, binderChild } =
          { binderVariable = newVar
          , binderChild = newChild
          }
+
+substitute
+    :: InternalVariable variable
+    => Map (SomeVariableName variable) (TermLike variable)
+    -> OrPattern variable
+    -> OrPattern variable
+substitute subst =
+    fromPatterns . fmap (Pattern.substitute subst) . toPatterns
+
+parseFromTermLike
+    :: InternalVariable variable
+    => TermLike variable
+    -> OrPattern variable
+parseFromTermLike (Or_ _ term1 term2) =
+    parseFromTermLike term1 <> parseFromTermLike term2
+parseFromTermLike term = fromTermLike term

kore/src/Kore/Internal/Pattern.hs

@@ -10,6 +10,7 @@ module Kore.Internal.Pattern
     , patternSort
     , fromCondition
     , fromCondition_
+    , fromTermAndPredicate
     , fromPredicateSorted
     , bottom
     , bottomOf
@@ -96,6 +97,18 @@ program configuration for Kore execution.
  -}
 type Pattern variable = Conditional variable (TermLike variable)
 
+fromTermAndPredicate
+    :: InternalVariable variable
+    => TermLike variable
+    -> Predicate variable
+    -> Pattern variable
+fromTermAndPredicate term predicate =
+    Conditional
+        { term
+        , predicate
+        , substitution = mempty
+        }
+
 fromCondition_
     :: InternalVariable variable
     => Condition variable

kore/src/Kore/Internal/TermLike.hs

@@ -45,6 +45,11 @@ module Kore.Internal.TermLike
     -- * Utility functions for dealing with sorts
     , forceSort
     , fullyOverrideSort
+    -- * Reachability modalities and application
+    , Modality (..)
+    , weakExistsFinally
+    , weakAlwaysFinally
+    , applyModality
     -- * Pure Kore pattern constructors
     , mkAnd
     , mkApplyAlias
@@ -2025,3 +2030,60 @@ refreshSetBinder
     -> Binder (SetVariable variable) (TermLike variable)
     -> Binder (SetVariable variable) (TermLike variable)
 refreshSetBinder = refreshBinder refreshSetVariable
+
+data Modality = WEF | WAF
+
+-- | Weak exists finally modality symbol.
+weakExistsFinally :: Text
+weakExistsFinally = "weakExistsFinally"
+
+-- | Weak always finally modality symbol.
+weakAlwaysFinally :: Text
+weakAlwaysFinally = "weakAlwaysFinally"
+
+-- | 'Alias' construct for weak exist finally.
+wEF :: Sort -> Alias (TermLike VariableName)
+wEF sort = Alias
+    { aliasConstructor = Id
+        { getId = weakExistsFinally
+        , idLocation = AstLocationNone
+        }
+    , aliasParams = [sort]
+    , aliasSorts = ApplicationSorts
+        { applicationSortsOperands = [sort]
+        , applicationSortsResult = sort
+        }
+    , aliasLeft = []
+    , aliasRight = mkTop sort
+    }
+
+-- | 'Alias' construct for weak always finally.
+wAF :: Sort -> Alias (TermLike VariableName)
+wAF sort = Alias
+    { aliasConstructor = Id
+        { getId = weakAlwaysFinally
+        , idLocation = AstLocationNone
+        }
+    , aliasParams = [sort]
+    , aliasSorts = ApplicationSorts
+        { applicationSortsOperands = [sort]
+        , applicationSortsResult = sort
+        }
+    , aliasLeft = []
+    , aliasRight = mkTop sort
+    }
+
+-- | Apply one of the reachability modality aliases
+-- to a term.
+applyModality
+    :: Modality
+    -> TermLike VariableName
+    -> TermLike VariableName
+applyModality modality term =
+    case modality of
+        WEF ->
+            mkApplyAlias (wEF sort) [term]
+        WAF ->
+            mkApplyAlias (wAF sort) [term]
+  where
+    sort = termLikeSort term

kore/src/Kore/Rewriting/RewritingVariable.hs

@@ -6,6 +6,7 @@ License     : NCSA
 
 module Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
+    , RewritingVariable
     , isConfigVariable
     , isRuleVariable
     , isSomeConfigVariable
@@ -26,6 +27,8 @@ module Kore.Rewriting.RewritingVariable
     , getResultPattern
     , getRemainderPredicate
     , getRemainderPattern
+    -- * Exported for reachability rule unparsing
+    , getRewritingVariable
     ) where
 
 import Prelude.Kore
@@ -118,6 +121,8 @@ instance From VariableName RewritingVariableName where
 
 instance FreshName RewritingVariableName
 
+type RewritingVariable = Variable RewritingVariableName
+
 mkElementConfigVariable
     :: ElementVariable VariableName
     -> ElementVariable RewritingVariableName