Hotfix check/adjust subsorting for substitutions based on ==K terms (#4076)

When a constraint of shape `VAR:VarSort ~> .K ==K term:TermSort ~> .K`
is externalised, the prior code just rendered a `VAR:VarSort #Equals
term:TermSort`. This is wrong when `TermSort /= VarSort`, however
`TermSort` will be a subsort of `VarSort`, otherwise the rule that
introduced this `==K` term is ill-sorted.

* Externalisation code now inserts the missing injection into the
`#Equals` expression.
* A test was added which demonstrates the use case and behaviour (failed
before, succeeds now).
* A pretty-printer option was added to show the injections in the
printed terms (off by default).

---------

Co-authored-by: Petar Maksimović <[email protected]>

Author: jberthold

booster/library/Booster/CLOptions.hs

@@ -184,7 +184,7 @@ parseLogOptions =
             ( metavar "PRETTY_PRINT"
                 <> value [Decoded, Truncated]
                 <> long "pretty-print"
-                <> help "Prety print options for kore terms: decode, infix, truncated"
+                <> help "Pretty print options for kore terms: decoded, infix, truncated, with-injections"
                 <> showDefault
             )
   where
@@ -210,7 +210,8 @@ parseLogOptions =
         "truncated" -> Right Truncated
         "infix" -> Right Infix
         "decoded" -> Right Decoded
-        other -> Left $ other <> ": Unsupported prettry printer option"
+        "with-injections" -> Right WithInjections
+        other -> Left $ other <> ": Unsupported pretty printer option"
 
     readTimeStampFormat :: String -> Either String TimestampFormat
     readTimeStampFormat = \case

booster/library/Booster/Pattern/Pretty.hs

@@ -23,18 +23,21 @@ import Data.Data (Proxy (..))
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 
-data ModifierT = Truncated | Infix | Decoded deriving (Show)
+data ModifierT = WithInjections | Truncated | Infix | Decoded deriving (Show)
 
 data Modifiers = Modifiers
-    { isTruncated, isInfix, isDecoded :: Bool
+    { isWithInjections, isTruncated, isInfix, isDecoded :: Bool
     }
 
 defaultModifiers :: Modifiers
-defaultModifiers = Modifiers False False False
+defaultModifiers = Modifiers False False False False
 
 class FromModifierT (m :: ModifierT) where
     modifiers' :: Modifiers -> Modifiers
 
+instance FromModifierT 'WithInjections where
+    modifiers' m = m{isWithInjections = True}
+
 instance FromModifierT 'Truncated where
     modifiers' m = m{isTruncated = True}
 
@@ -60,6 +63,7 @@ toModifiersRep = go (ModifiersRep @'[] Proxy)
   where
     go rep@(ModifiersRep (Proxy :: Proxy mods)) = \case
         [] -> rep
+        (WithInjections : xs) -> go (ModifiersRep @('WithInjections ': mods) Proxy) xs
         (Truncated : xs) -> go (ModifiersRep @('Truncated ': mods) Proxy) xs
         (Infix : xs) -> go (ModifiersRep @('Infix ': mods) Proxy) xs
         (Decoded : xs) -> go (ModifiersRep @('Decoded ': mods) Proxy) xs
@@ -89,7 +93,13 @@ instance Pretty (PrettyWithModifiers mods Term) where
         DotDotDot -> "..."
         DomainValue _sort bs -> pretty . show . Text.decodeLatin1 . shortenBS $ bs
         Var var -> pretty' @mods var
-        Injection _source _target t' -> pretty' @mods t'
+        Injection source target t'
+            | isWithInjections ->
+                "inj"
+                    <> Pretty.braces
+                        (Pretty.hsep $ Pretty.punctuate Pretty.comma [pretty' @mods source, pretty' @mods target])
+                    <> KPretty.arguments' [pretty' @mods t']
+            | otherwise -> pretty' @mods t'
         KMap _attrs keyVals rest ->
             Pretty.braces . Pretty.hsep . Pretty.punctuate Pretty.comma $
                 [pretty' @mods k <+> "->" <+> pretty' @mods v | (k, v) <- keyVals]
@@ -110,7 +120,8 @@ instance Pretty (PrettyWithModifiers mods Term) where
                 Pretty.<+> maybe mempty ((" ++ " <>) . pretty' @mods) rest
       where
         Modifiers
-            { isTruncated
+            { isWithInjections
+            , isTruncated
             , isInfix
             , isDecoded
             } = modifiers @mods defaultModifiers

booster/library/Booster/Syntax/Json/Externalise.hs

@@ -99,7 +99,7 @@ externaliseExistTerm vars t = exist vars
 externalisePredicate :: Syntax.Sort -> Internal.Predicate -> Syntax.KorePattern
 externalisePredicate sort (Internal.Predicate t) =
     Syntax.KJEquals
-        { argSort = externaliseSort $ sortOfTerm t
+        { argSort = externaliseSort $ sortOfTerm t -- must actually be SortBool
         , sort
         , first = externaliseTerm Internal.TrueBool
         , second = externaliseTerm t
@@ -116,11 +116,20 @@ externaliseCeil sort (Internal.Ceil term) =
 externaliseSubstitution :: Syntax.Sort -> Internal.Variable -> Internal.Term -> Syntax.KorePattern
 externaliseSubstitution sort Internal.Variable{variableSort = iSort, variableName = iName} t =
     Syntax.KJEquals
-        { argSort = externaliseSort $ sortOfTerm t
+        { argSort = extISort
         , sort
-        , first = Syntax.KJEVar (varNameToId iName) (externaliseSort iSort)
-        , second = externaliseTerm t
+        , first = Syntax.KJEVar (varNameToId iName) extISort
+        , second = target
         }
+  where
+    extISort = externaliseSort iSort
+    -- The sort of the term not be iSort but must be a subsort of it.
+    -- We assume termSort < iSort but cannot check it.
+    termSort = sortOfTerm t
+    target
+        | termSort == iSort = externaliseTerm t
+        | otherwise =
+            externaliseTerm $ Internal.Injection termSort iSort t
 
 varNameToId :: Internal.VarName -> Syntax.Id
 varNameToId = Syntax.Id . Text.decodeLatin1

booster/test/rpc-integration/resources/subk.k

@@ -2,9 +2,9 @@ module SUBK
   imports BOOL
   imports K-EQUAL
 
-  syntax State ::= "ping" [token]
-                 | "pong" [token]
-                 | "peng" [token]
+  syntax State ::= "ping" [symbol("ping")]
+                 | "pong" [symbol("pong")]
+                 | "peng" [symbol("peng")]
 
   configuration <k> $PGM:State ~> .K </k>
                 <x> .K </x>
@@ -27,4 +27,12 @@ module SUBK
                <x> X </x>
     requires notBool (X ==K inK(pong))
 
+  syntax State ::= Substate
+
+  syntax Substate ::= "bong" [symbol("bong")]
+
+  syntax Bool ::= isBong ( State ) [function, total, symbol("isBong")]
+
+  rule isBong(S) => S ==K bong
+
 endmodule