runtimeverification · ttuegel · Feb 18, 2020 · Feb 13, 2020 · Feb 13, 2020 · Feb 9, 2020
diff --git a/kore/src/Debug.hs b/kore/src/Debug.hs
@@ -338,16 +338,18 @@ fromCofreeT (CofreeT x) = SOP (Z (I x :* Nil))
 
 instance (Debug k, Debug a) => Debug (Map.Map k a) where
     debugPrec as precOut =
-        parens (precOut >= 10) ("Data.Map.fromList" <+> debug (Map.toList as))
+        (parens (precOut >= 10) . Pretty.sep)
+        ["Data.Map.fromList", debug (Map.toList as)]
 
 instance Debug a => Debug (Set a) where
     debugPrec as precOut =
-        parens (precOut >= 10) ("Data.Set.fromList" <+> debug (Set.toList as))
+        (parens (precOut >= 10) . Pretty.sep)
+        ["Data.Set.fromList", debug (Set.toList as)]
 
 instance Debug a => Debug (Seq a) where
     debugPrec as precOut =
-        parens (precOut >= 10)
-        $ "Data.Sequence.fromList" <+> debug (Foldable.toList as)
+        (parens (precOut >= 10) . Pretty.sep)
+        ["Data.Sequence.fromList", debug (Foldable.toList as)]
 
 instance Debug a => Debug (Const a b)
 

diff --git a/kore/src/Kore/Builtin/Int/Int.hs b/kore/src/Kore/Builtin/Int/Int.hs
@@ -54,9 +54,6 @@ import qualified Data.Text as Text
 import qualified Kore.Domain.Builtin as Domain
 import Kore.Internal.Pattern as Pattern
 import Kore.Internal.TermLike as TermLike
-import Kore.Variables.Fresh
-    ( FreshVariable
-    )
 
 {- | Builtin name of the @Int@ sort.
  -}
@@ -72,7 +69,7 @@ See also: 'sort'
 
  -}
 asInternal
-    :: FreshVariable variable
+    :: InternalVariable variable
     => Sort  -- ^ resulting sort
     -> Integer  -- ^ builtin value to render
     -> TermLike variable

diff --git a/kore/src/Kore/Builtin/String/String.hs b/kore/src/Kore/Builtin/String/String.hs
@@ -41,9 +41,6 @@ import Kore.Internal.Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.TermLike as TermLike
-import Kore.Variables.Fresh
-    ( FreshVariable
-    )
 
 {- | Builtin name of the @String@ sort.
  -}
@@ -59,7 +56,7 @@ See also: 'sort'
 
  -}
 asInternal
-    :: FreshVariable variable
+    :: InternalVariable variable
     => Sort  -- ^ resulting sort
     -> Text  -- ^ builtin value to render
     -> TermLike variable

diff --git a/kore/src/Kore/Internal/Condition.hs b/kore/src/Kore/Internal/Condition.hs
@@ -64,7 +64,7 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Internal.Variable
 import Kore.Syntax
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 import Kore.Variables.UnifiedVariable
     ( UnifiedVariable
@@ -148,7 +148,7 @@ toPredicate
 toPredicate = from
 
 mapVariables
-    :: (Ord variable1, FreshVariable variable2)
+    :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2)
     => (ElementVariable variable1 -> ElementVariable variable2)
     -> (SetVariable variable1 -> SetVariable variable2)
     -> Condition variable1

diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs
@@ -69,6 +69,7 @@ import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
     ( InternalVariable
     , Sort
+    , SortedVariable
     , TermLike
     , termLikeSort
     )
@@ -78,11 +79,10 @@ import Kore.TopBottom
     )
 import Kore.Unparser
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 import Kore.Variables.UnifiedVariable
-    ( ElementVariable
-    , SetVariable
+    ( MapVariables
     , UnifiedVariable
     )
 import qualified SQL
@@ -413,12 +413,12 @@ isPredicate Conditional {term} = isTop term
 
 -}
 mapVariables
-    :: (Ord variableFrom, FreshVariable variableTo)
-    => ((ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> termFrom -> termTo)
-    -> (ElementVariable variableFrom -> ElementVariable variableTo)
-    -> (SetVariable variableFrom -> SetVariable variableTo)
-    -> Conditional variableFrom termFrom
-    -> Conditional variableTo   termTo
+    ::  Ord variableFrom
+    =>  (FreshPartialOrd variableTo, SortedVariable variableTo)
+    =>  MapVariables variableFrom variableTo termFrom termTo
+    ->  MapVariables variableFrom variableTo
+            (Conditional variableFrom termFrom)
+            (Conditional variableTo   termTo)
 mapVariables
     mapTermVariables
     mapElemVar

diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs
@@ -63,6 +63,7 @@ import Kore.Internal.TermLike
     , InternalVariable
     , SetVariable
     , Sort
+    , SortedVariable
     , TermLike
     , mkAnd
     , mkBottom
@@ -79,7 +80,7 @@ import Kore.TopBottom
     ( TopBottom (..)
     )
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 
 {- | The conjunction of a pattern, predicate, and substitution.
@@ -123,7 +124,7 @@ freeElementVariables =
 in an Pattern.
 -}
 mapVariables
-    :: (Ord variableFrom, FreshVariable variableTo)
+    :: (Ord variableFrom, FreshPartialOrd variableTo, SortedVariable variableTo)
     => (ElementVariable variableFrom -> ElementVariable variableTo)
     -> (SetVariable variableFrom -> SetVariable variableTo)
     -> Pattern variableFrom

diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs
@@ -121,7 +121,7 @@ import Kore.TopBottom
     )
 import Kore.Unparser
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 import Kore.Variables.UnifiedVariable
     ( UnifiedVariable (..)
@@ -706,7 +706,7 @@ isPredicate = Either.isRight . makePredicate
 {- | Replace all variables in a @Predicate@ using the provided mapping.
 -}
 mapVariables
-    :: (Ord from, FreshVariable to)
+    :: (Ord from, FreshPartialOrd to, SortedVariable to)
     => (ElementVariable from -> ElementVariable to)
     -> (SetVariable from -> SetVariable to)
     -> Predicate from

diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs
@@ -86,7 +86,7 @@ import Kore.Unparser
     ( unparseToString
     )
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 import Kore.Variables.UnifiedVariable
 import qualified SQL
@@ -314,24 +314,25 @@ wrap xs = Substitution xs
 -- | Wrap the list of substitutions to a normalized substitution. Do not use
 -- this unless you are sure you need it.
 unsafeWrap
-    :: Ord variable
+    :: HasCallStack
+    => Ord variable
     => [(UnifiedVariable variable, TermLike variable)]
     -> Substitution variable
 unsafeWrap =
     NormalizedSubstitution . List.foldl' insertNormalized Map.empty
   where
     insertNormalized subst (var, termLike) =
+        Map.insert var termLike subst
         -- The variable must not occur in the substitution
-        assert (Map.notMember var subst)
+        & assert (Map.notMember var subst)
         -- or in the right-hand side of this or any other substitution,
-        $ assert (not $ occurs termLike)
-        $ assert (not $ any occurs subst)
+        & assert (not $ occurs termLike)
+        & assert (not $ any occurs subst)
         -- this substitution must not depend on any substitution variable,
-        $ assert (not $ any depends $ Map.keys subst)
+        & assert (not $ any depends $ Map.keys subst)
         -- and if this is an element variable substitution, the substitution
         -- must be defined.
-        $ assert (not $ isElemVar var && isBottom termLike)
-        $ Map.insert var termLike subst
+        & assert (not $ isElemVar var && isBottom termLike)
       where
         occurs = TermLike.hasFreeVariable var
         depends var' = TermLike.hasFreeVariable var' termLike
@@ -350,7 +351,7 @@ modify f = wrap . f . unwrap
 -- with the given function.
 mapVariables
     :: forall variableFrom variableTo
-    .  (Ord variableFrom, FreshVariable variableTo)
+    .  (Ord variableFrom, FreshPartialOrd variableTo, SortedVariable variableTo)
     => (ElementVariable variableFrom -> ElementVariable variableTo)
     -> (SetVariable variableFrom -> SetVariable variableTo)
     -> Substitution variableFrom

diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs
@@ -271,7 +271,8 @@ import Kore.Unparser
 import qualified Kore.Unparser as Unparser
 import Kore.Variables.Binding
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
+    , FreshVariable
     )
 import qualified Kore.Variables.Fresh as Fresh
 import Kore.Variables.UnifiedVariable
@@ -391,7 +392,7 @@ composes with other tree transformations without allocating intermediates.
 
  -}
 fromConcrete
-    :: FreshVariable variable
+    :: (FreshPartialOrd variable, SortedVariable variable)
     => TermLike Concrete
     -> TermLike variable
 fromConcrete = mapVariables (\case {}) (\case {})

diff --git a/kore/src/Kore/Internal/TermLike/Renaming.hs b/kore/src/Kore/Internal/TermLike/Renaming.hs
@@ -56,6 +56,7 @@ renameFreeVariables trElemVar trSetVar =
                 renameSetVariable setVar
                     <$> trSetVar setVar
                     <*> pure renaming
+{-# INLINE renameFreeVariables #-}
 
 askUnifiedVariable
     :: Monad m

diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs
@@ -125,7 +125,7 @@ import Kore.Unparser
 import qualified Kore.Unparser as Unparser
 import Kore.Variables.Binding
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 import qualified Kore.Variables.Fresh as Fresh
 import qualified Pretty
@@ -593,7 +593,7 @@ See also: 'traverseVariables'
  -}
 mapVariables
     :: forall variable1 variable2
-    .  (Ord variable1, FreshVariable variable2)
+    .  (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2)
     => (ElementVariable variable1 -> ElementVariable variable2)
     -> (SetVariable variable1 -> SetVariable variable2)
     -> TermLike variable1
@@ -669,7 +669,7 @@ See also: 'mapVariables'
  -}
 traverseVariables
     :: forall variable1 variable2 m
-    .  (Ord variable1, FreshVariable variable2)
+    .  (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2)
     => Monad m
     => (ElementVariable variable1 -> m (ElementVariable variable2))
     -> (SetVariable variable1 -> m (SetVariable variable2))
@@ -762,7 +762,7 @@ sequenceAdjunct gsequence =
 
 renameElementBinder
     ::  Monad m
-    =>  (Ord variable1, FreshVariable variable2)
+    =>  (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2)
     =>  (ElementVariable variable1 -> m (ElementVariable variable2))
     ->  Set.Set (UnifiedVariable variable2)
     ->  Binder (ElementVariable variable1)
@@ -788,7 +788,7 @@ renameElementBinder trElemVar avoiding binder = do
 
 renameSetBinder
     ::  Monad m
-    =>  (Ord variable1, FreshVariable variable2)
+    =>  (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2)
     =>  (SetVariable variable1 -> m (SetVariable variable2))
     ->  Set.Set (UnifiedVariable variable2)
     ->  Binder (SetVariable variable1)
@@ -888,33 +888,32 @@ externalizeFreshVariables termLike =
     among the set of avoided variables. The externalized form is returned.
 
      -}
-    safeElementVariable
-        :: FreeVariables Variable
-        -> ElementVariable Variable
-        -> ElementVariable Variable
-    safeElementVariable avoiding variable =
-        head  -- 'head' is safe because 'iterate' creates an infinite list
+    safeVariable
+        :: (Functor f, FreshPartialOrd (f Variable))
+        => (f Variable -> UnifiedVariable Variable)
+        -> FreeVariables Variable
+        -> f Variable
+        -> f Variable
+    safeVariable mk avoiding variable =
+        head
         $ dropWhile wouldCapture
         $ externalize
-        <$> iterate nextVariable variable
+        <$> iterate Fresh.nextVariable variable
       where
-        wouldCapture var = isFreeVariable (ElemVar var) avoiding
-        nextVariable = fmap Fresh.nextVariable
+        wouldCapture var = isFreeVariable (mk var) avoiding
         externalize = fmap Variable.externalizeFreshVariable
 
+    safeElementVariable
+        :: FreeVariables Variable
+        -> ElementVariable Variable
+        -> ElementVariable Variable
+    safeElementVariable = safeVariable ElemVar
+
     safeSetVariable
         :: FreeVariables Variable
         -> SetVariable Variable
         -> SetVariable Variable
-    safeSetVariable avoiding variable =
-        head  -- 'head' is safe because 'iterate' creates an infinite list
-        $ dropWhile wouldCapture
-        $ externalize
-        <$> iterate nextVariable variable
-      where
-        wouldCapture var = isFreeVariable (SetVar var) avoiding
-        nextVariable = fmap Fresh.nextVariable
-        externalize = fmap Variable.externalizeFreshVariable
+    safeSetVariable = safeVariable SetVar
 
     underElementBinder freeVariables' variable child = do
         let variable' = safeElementVariable freeVariables' variable

diff --git a/kore/src/Kore/Internal/Variable.hs b/kore/src/Kore/Internal/Variable.hs
@@ -7,6 +7,8 @@ License     : NCSA
 module Kore.Internal.Variable
     ( SubstitutionOrd (..)
     , InternalVariable
+    , FreshVariable
+    , FreshPartialOrd
     , module Kore.Syntax.ElementVariable
     , module Kore.Syntax.SetVariable
     , module Kore.Syntax.Variable
@@ -24,7 +26,8 @@ import Kore.Unparser
     ( Unparse
     )
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
+    , FreshVariable
     )
 
 {- | @SubstitutionOrd@ orders variables for substitution.
@@ -81,5 +84,6 @@ these constraints.
 type InternalVariable variable =
     ( Ord variable, SubstitutionOrd variable
     , Debug variable, Show variable, Unparse variable
-    , VariableName variable, SortedVariable variable, FreshVariable variable
+    , VariableName variable, SortedVariable variable
+    , FreshPartialOrd variable, FreshVariable variable
     )
diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs
@@ -94,7 +94,7 @@ import Kore.Step.Simplification.Simplify
 import qualified Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Variables.Binding
 import Kore.Variables.Fresh
-    ( FreshVariable
+    ( FreshPartialOrd
     )
 import qualified Kore.Variables.Fresh as Variables
 import Kore.Variables.UnifiedVariable
@@ -607,7 +607,7 @@ Returns 'Nothing' if the variable name is already globally-unique.
 
  -}
 liftVariable
-    :: FreshVariable variable
+    :: (FreshPartialOrd variable, SortedVariable variable)
     => MonadState (MatcherState variable) matcher
     => UnifiedVariable variable
     -> matcher (Maybe (UnifiedVariable variable))