Fix unparsing built-ins (#2540)

* [WIP]: Use futu for externalizing builtins

* implemented new externalization functions

* moved externalization code to the test library

* Materialize Nix expressions

* update kore.cabal

* merged master and synched externalisation with unparsing

* reverted last two commits

* Run fourmolu

* addressed PR comments

* Format with fourmolu

* removed unused import

Co-authored-by: MirceaS <[email protected]>
Co-authored-by: MirceaS <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 4 people

kore/kore.cabal

@@ -261,7 +261,6 @@ library
     Kore.Builtin.Endianness.Endianness
     Kore.Builtin.EqTerm
     Kore.Builtin.Error
-    Kore.Builtin.External
     Kore.Builtin.Inj
     Kore.Builtin.Int
     Kore.Builtin.Int.Int
@@ -651,6 +650,7 @@ test-suite kore-test
     Test.Kore.Builtin.Definition
     Test.Kore.Builtin.Encoding
     Test.Kore.Builtin.Endianness
+    Test.Kore.Builtin.External
     Test.Kore.Builtin.Inj
     Test.Kore.Builtin.Int
     Test.Kore.Builtin.InternalBytes

kore/src/Kore/Builtin.hs

@@ -28,7 +28,6 @@ module Kore.Builtin (
     koreVerifiers,
     koreEvaluators,
     evaluators,
-    externalize,
     internalize,
 ) where
 
@@ -50,7 +49,6 @@ import qualified Kore.Attribute.Symbol as Attribute
 import qualified Kore.Builtin.Bool as Bool
 import qualified Kore.Builtin.Builtin as Builtin
 import qualified Kore.Builtin.Endianness as Endianness
-import Kore.Builtin.External
 import qualified Kore.Builtin.Inj as Inj
 import qualified Kore.Builtin.Int as Int
 import qualified Kore.Builtin.InternalBytes as InternalBytes

kore/src/Kore/Builtin/AssocComm/AssocComm.hs

@@ -5,23 +5,19 @@ Copyright   : (c) Runtime Verification, 2019
 License     : NCSA
 -}
 module Kore.Builtin.AssocComm.AssocComm (
-    asTermLike,
     UnitSymbol (..),
     ConcatSymbol (..),
     ConcreteElements (..),
     VariableElements (..),
     Opaque (..),
 ) where
 
-import qualified Data.List as List
 import Kore.Internal.Symbol (
     Symbol,
  )
 import Kore.Internal.TermLike (
     Concrete,
-    InternalVariable,
     TermLike,
-    mkApplySymbol,
  )
 import Prelude.Kore
 
@@ -62,44 +58,3 @@ newtype VariableElements variable = VariableElements {getVariableElements :: [Te
 
 -- | Wrapper for giving names to arguments.
 newtype Opaque variable = Opaque {getOpaque :: [TermLike variable]}
-
--- | Externalizes a 'Domain.InternalAc' as a 'TermLike'.
-asTermLike ::
-    forall variable.
-    InternalVariable variable =>
-    UnitSymbol ->
-    ConcatSymbol ->
-    ConcreteElements variable ->
-    VariableElements variable ->
-    Opaque variable ->
-    TermLike variable
-asTermLike
-    (UnitSymbol unitSymbol)
-    (ConcatSymbol concatSymbol)
-    (ConcreteElements concreteElements)
-    (VariableElements variableElements)
-    (Opaque opaque) =
-        case splitLastInit concreteElements of
-            Nothing -> case splitLastInit opaque of
-                Nothing -> case splitLastInit variableElements of
-                    Nothing -> mkApplySymbol unitSymbol []
-                    Just (ves, ve) -> addTerms ves ve
-                Just (opaqs, opaq) ->
-                    addTerms variableElements (addTerms opaqs opaq)
-            Just (concretes, concrete) ->
-                addTerms variableElements $
-                    addTerms opaque $
-                        addTerms concretes concrete
-      where
-        addTerms :: [TermLike variable] -> TermLike variable -> TermLike variable
-        addTerms terms term = List.foldr concat' term terms
-
-        concat' :: TermLike variable -> TermLike variable -> TermLike variable
-        concat' map1 map2 = mkApplySymbol concatSymbol [map1, map2]
-
-splitLastInit :: [a] -> Maybe ([a], a)
-splitLastInit [] = Nothing
-splitLastInit [a] = Just ([], a)
-splitLastInit (a : as) = do
-    (initA, lastA) <- splitLastInit as
-    return (a : initA, lastA)

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -19,7 +19,6 @@ builtin modules.
 module Kore.Builtin.AssociativeCommutative (
     asInternalConcrete,
     asPattern,
-    asTermLike,
     ConcatSymbol (..),
     ConcreteElements (..),
     evalConcatNormalizedOrBottom,
@@ -97,7 +96,6 @@ import Kore.Internal.Symbol (
 import Kore.Internal.TermLike (
     Key,
     TermLike,
-    mkApplySymbol,
     mkElemVar,
     termLikeSort,
     pattern App_,
@@ -1623,44 +1621,3 @@ newtype VariableElements variable = VariableElements {getVariableElements :: [Te
 
 -- | Wrapper for giving names to arguments.
 newtype Opaque variable = Opaque {getOpaque :: [TermLike variable]}
-
--- | Externalizes a 'InternalAc' as a 'TermLike'.
-asTermLike ::
-    forall variable.
-    InternalVariable variable =>
-    UnitSymbol ->
-    ConcatSymbol ->
-    ConcreteElements variable ->
-    VariableElements variable ->
-    Opaque variable ->
-    TermLike variable
-asTermLike
-    (UnitSymbol unitSymbol)
-    (ConcatSymbol concatSymbol)
-    (ConcreteElements concreteElements)
-    (VariableElements variableElements)
-    (Opaque opaque) =
-        case splitLastInit concreteElements of
-            Nothing -> case splitLastInit opaque of
-                Nothing -> case splitLastInit variableElements of
-                    Nothing -> mkApplySymbol unitSymbol []
-                    Just (ves, ve) -> addTerms ves ve
-                Just (opaqs, opaq) ->
-                    addTerms variableElements (addTerms opaqs opaq)
-            Just (concretes, concrete) ->
-                addTerms variableElements $
-                    addTerms opaque $
-                        addTerms concretes concrete
-      where
-        addTerms :: [TermLike variable] -> TermLike variable -> TermLike variable
-        addTerms terms term = List.foldr concat' term terms
-
-        concat' :: TermLike variable -> TermLike variable -> TermLike variable
-        concat' map1 map2 = mkApplySymbol concatSymbol [map1, map2]
-
-splitLastInit :: [a] -> Maybe ([a], a)
-splitLastInit [] = Nothing
-splitLastInit [a] = Just ([], a)
-splitLastInit (a : as) = do
-    (initA, lastA) <- splitLastInit as
-    return (a : initA, lastA)

kore/src/Kore/Builtin/Bool.hs

@@ -8,7 +8,6 @@ module Kore.Builtin.Bool (
     verifiers,
     builtinFunctions,
     asInternal,
-    asTermLike,
     asPattern,
     extractBoolDomainValue,
     parse,

kore/src/Kore/Builtin/Bool/Bool.hs

@@ -6,7 +6,6 @@ module Kore.Builtin.Bool.Bool (
     sort,
     asBuiltin,
     asInternal,
-    asTermLike,
     asPattern,
 
     -- * Keys
@@ -35,18 +34,14 @@ import qualified Kore.Internal.Pattern as Pattern (
     fromTermLike,
  )
 import Kore.Internal.TermLike (
-    DomainValue (DomainValue),
     InternalVariable,
     Sort,
     TermLike,
-    mkDomainValue,
     mkInternalBool,
-    mkStringLiteral,
  )
 import qualified Kore.Internal.TermLike as TermLike (
     markSimplified,
  )
-import qualified Kore.Internal.TermLike as TermLike.DoNotUse
 import Prelude.Kore
 
 -- | Builtin name of the @Bool@ sort.
@@ -79,31 +74,6 @@ asBuiltin ::
     InternalBool
 asBuiltin = InternalBool
 
-{- | Render a 'Bool' as a domain value pattern of the given sort.
-
-  The result sort should be hooked to the builtin @Bool@ sort, but this is not
-  checked.
-
-  See also: 'sort'
--}
-asTermLike ::
-    InternalVariable variable =>
-    -- | builtin value to render
-    InternalBool ->
-    TermLike variable
-asTermLike builtin =
-    mkDomainValue
-        DomainValue
-            { domainValueSort = internalBoolSort
-            , domainValueChild = mkStringLiteral literal
-            }
-  where
-    InternalBool{internalBoolSort} = builtin
-    InternalBool{internalBoolValue = bool} = builtin
-    literal
-        | bool = "true"
-        | otherwise = "false"
-
 asPattern ::
     InternalVariable variable =>
     -- | resulting sort

kore/src/Kore/Builtin/External.hs

@@ -23,7 +23,6 @@ module Kore.Builtin.Int (
     builtinFunctions,
     expectBuiltinInt,
     extractIntDomainValue,
-    asTermLike,
     asInternal,
     asPattern,
     asPartialPattern,