{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | The very core of miniKanren. So core that it basically deals with
-- unification only. For writing relational programs, you will need @"Goal"@ as
-- well.
module Kanren.Core (
  -- * Values and terms
  Logical (..),
  VarId,
  Term (..),
  Atomic (..),

  -- ** Operations on terms
  unify',
  walk',
  occursCheck',
  inject',
  extract',
  Normalizable (..),
  normalize',
  runNormalize,

  -- ** Constraints
  disequality,

  -- * The search state
  State,
  empty,
  makeVariable,
) where

import Control.DeepSeq
import Control.Monad (ap)
import Data.Bifunctor (first)
import Data.Coerce (coerce)
import Data.Foldable (foldrM)
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.Maybe (fromMaybe)
import GHC.Exts (IsList (..))
import GHC.Generics (Generic)
import Unsafe.Coerce (unsafeCoerce)

-- $setup
-- >>> :set -package typedKanren
-- >>> import Kanren.Goal
-- >>> import Kanren.LogicalBase

-- | Types that can enter the relational world.
--
-- Simple types without fields, such as 'Bool' and 'Int', can be used in
-- relational programs as is. Instances for such types are as simple as
--
-- > data Ternary = True | False | Maybe deriving (Eq)
-- > instance Logical Ternary
--
-- >>> run (\x -> x === Value True)
-- [True]
--
-- When a type contains other types, this becomes more tricky. Consider the
-- following type:
--
-- > data Point = Point { x :: Int, y :: Int }
--
-- In the relational world, values may be known only partially. For example, we
-- may find out that some equation is true only for a particular value of @x@,
-- but once that holds, @y@ can be anything. The definition above cannot express
-- this, since @Point@ has to be instantiated with some particular pair of
-- @Int@s.
--
-- To account for this, we'd like to modify the definition slightly, so that
-- each field can possibly contain a variable:
--
-- > data LogicPoint = LogicPoint { logicX :: Term Int, logicY :: Term Int }
--
-- @'Term' a@ here can either be a 'Var' or a 'Value' for type @a@.
--
-- Now we can specify that a @Point@ becomes a @LogicPoint@ in the relational
-- world:
--
-- > instance Logical Point where
-- >   type Logic Point = LogicPoint
--
-- However, we are not finished here yet. When a type has a different
-- representation in the logical world, we need to show how we can go from
-- a @Point@ to a @LogicPoint@ with 'inject' and go back with 'extract':
--
-- > inject (Point x y) = LogicPoint (Value x) (Value y)
-- > extract (LogicPoint (Value x) (Value y)) = Just (Point x y)
-- > extract _ = Nothing
--
-- Note that while we can always transform a @Point@ to a @LogicPoint@, going
-- back to a @Point@ can fail if any field contains a variable.
--
-- We also need to show how @LogicPoint@s can be unified. For simple types,
-- unification of terms works in the following way. If both terms are already
-- known, we just check that they are equal. Otherwise, one of the terms is a
-- variable, and we record that it must be equal to the other term.
--
-- With complex types, a third case is possible: we can refine an existing value
-- if one of its fields is a variable. We can achieve this by unifying each
-- field separately.
--
-- > unify (LogicPoint leftX leftY) (LogicPoint rightX rightY) state =
-- >   unify' leftX rightX state >>= unify' leftY rightY
--
-- 'unify' takes two values being unified and the current state. If unification
-- succeeds, a new state with acquired knowledge is returned. if unification
-- leads to contradiction (the two values cannot be unified), 'unify' returns
-- 'Nothing'. You do not modify the state yourself — this is handled by
-- 'unify'', a version of 'unify' which works on 'Term's instead of logic
-- values.
--
-- When we find out that a variable must have a particular value, we need not
-- only to add a new entry in the state, but also update existing values which
-- might contain that variable. This is the job of 'walk', which takes the value
-- being updated and the current state. Just like with 'unify', the actual job
-- of replacing variables with values is done by 'walk'', and you only need to
-- apply it to each field.
--
-- > walk f (LogicPoint x y) = LogicPoint (walk' f x) (walk' f x)
--
-- You may notice that the logical representation of the type and the 'Logical'
-- instance are suitable for automatic generation. Indeed, the
-- @"GenericLogical"@ module provides generic versions of `Logical`'s methods.
-- The @"TH"@ module goes further and provides 'TH.makeLogic' to generate
-- logical representations for your types.
--
-- Although you'll see instances for @base@ types below, keep in mind that
-- they're only available from the @"LogicalBase"@ module.
class Logical a where
  -- | The logical representation of this type. This defaults to the type
  -- itself, but complex types will usually have a separate logic type.
  --
  -- Note that 'Logic a' is injective, so two different types cannot use the
  -- same type as their logical representation. If you want to provide an
  -- instance for @newtype NT = NT T@, then the logical representation should be
  -- a newtype as well: @newtype LogicNT = LogicNT (Logic T)@.
  type Logic a = r | r -> a

  type Logic a = a

  -- | Perform unification of two values. If unification succeeds, return the
  -- possibly modified state. If unification leads to contradiction, return
  -- 'Nothing'.
  --
  -- The default implementation checks for equality, which works well for simple
  -- types. Complex types will provide their own implmentations which apply
  -- 'unify'' to each field.
  unify :: Logic a -> Logic a -> State -> Maybe State
  default unify :: (Eq (Logic a)) => Logic a -> Logic a -> State -> Maybe State
  unify Logic a
x Logic a
y State
state
    | Logic a
x Logic a -> Logic a -> Bool
forall a. Eq a => a -> a -> Bool
== Logic a
y = State -> Maybe State
forall a. a -> Maybe a
Just State
state
    | Bool
otherwise = Maybe State
forall a. Maybe a
Nothing

  -- | Update the value with acquired knowledge. This method the current state
  -- to substitute variables with their obtained values.
  --
  -- The default implementation works for simple types and returns the value as
  -- is (since there's nothing to substitute inside). Complex types will provide
  -- their own implementations which apply 'walk'' to each field.
  walk :: State -> Logic a -> Logic a
  default walk :: (a ~ Logic a) => State -> Logic a -> Logic a
  walk State
_ = a -> a
Logic a -> Logic a
forall a. a -> a
id

  occursCheck :: VarId b -> Logic a -> State -> Bool
  default occursCheck :: (a ~ Logic a) => VarId b -> Logic a -> State -> Bool
  occursCheck VarId b
_ Logic a
_ State
_ = Bool
False

  -- | Transform a value to its logical representation.
  --
  -- The default implementation works for simple types and returns the value as
  -- is. Complex types will provide their own implementations which apply
  -- 'inject'' to each field. 'inject'' is also the function that you will use
  -- in your relational programs.
  inject :: a -> Logic a
  default inject :: (a ~ Logic a) => a -> Logic a
  inject = a -> a
a -> Logic a
forall a. a -> a
id

  -- | Transform a logical representation of a value back to its normal
  -- representation. Note that this transformation can fail in the general case,
  -- because variables cannot be transformed to values.
  --
  -- The default implementation works for simple types and returns the value as
  -- is. Complex types will provide their own implementations which apply
  -- 'extract'' to each field. 'extract'' is also the function that you will
  -- use in your code.
  extract :: Logic a -> Maybe a
  default extract :: (a ~ Logic a) => Logic a -> Maybe a
  extract = a -> Maybe a
Logic a -> Maybe a
forall a. a -> Maybe a
Just

-- | A variable, which reserves a place for a logical value for type @a@.
newtype VarId a = VarId Int
  deriving newtype (VarId a -> VarId a -> Bool
(VarId a -> VarId a -> Bool)
-> (VarId a -> VarId a -> Bool) -> Eq (VarId a)
forall a. VarId a -> VarId a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. VarId a -> VarId a -> Bool
== :: VarId a -> VarId a -> Bool
$c/= :: forall a. VarId a -> VarId a -> Bool
/= :: VarId a -> VarId a -> Bool
Eq, VarId a -> ()
(VarId a -> ()) -> NFData (VarId a)
forall a. VarId a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. VarId a -> ()
rnf :: VarId a -> ()
NFData)

instance Show (VarId a) where
  show :: VarId a -> String
show (VarId Int
varId) = String
"_." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
varId

-- | A logical value for type @a@, or a variable.
--
-- Note that @a@ must be the “normal” type, not its logical representation,
-- since 'Term' stores @'Logic' a@. For example, @Term (Either String (Tree
-- Int))@ will correctly use @LogicList Char@ and @LogicTree Int@ deep inside.
-- This way, you do not need to know what the logic representation for a type is
-- named, and deriving the logical representation for a type is trivial.
data Term a
  = Var !(VarId a)
  | Value !(Logic a)
  deriving ((forall x. Term a -> Rep (Term a) x)
-> (forall x. Rep (Term a) x -> Term a) -> Generic (Term a)
forall x. Rep (Term a) x -> Term a
forall x. Term a -> Rep (Term a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Term a) x -> Term a
forall a x. Term a -> Rep (Term a) x
$cfrom :: forall a x. Term a -> Rep (Term a) x
from :: forall x. Term a -> Rep (Term a) x
$cto :: forall a x. Rep (Term a) x -> Term a
to :: forall x. Rep (Term a) x -> Term a
Generic)

deriving instance (NFData (Logic a)) => NFData (Term a)

deriving instance (Eq (Logic a)) => Eq (Term a)

-- | This instance doesn't print the 'Var' and 'Value' tags. While this reduces
-- noise in the output, this may also be confusing since fully instantiated
-- terms may look indistinguishable from regular values.
instance (Show (Logic a)) => Show (Term a) where
  showsPrec :: Int -> Term a -> ShowS
showsPrec Int
d (Var VarId a
var) = Int -> VarId a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d VarId a
var
  showsPrec Int
d (Value Logic a
value) = Int -> Logic a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Logic a
value

instance (IsList (Logic a)) => IsList (Term a) where
  type Item (Term a) = Item (Logic a)
  fromList :: [Item (Term a)] -> Term a
fromList = Logic a -> Term a
forall a. Logic a -> Term a
Value (Logic a -> Term a)
-> ([Item (Logic a)] -> Logic a) -> [Item (Logic a)] -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Item (Logic a)] -> Logic a
forall l. IsList l => [Item l] -> l
fromList
  toList :: Term a -> [Item (Term a)]
toList (Value Logic a
xs) = Logic a -> [Item (Logic a)]
forall l. IsList l => l -> [Item l]
toList Logic a
xs
  toList (Var VarId a
x) = String -> [Item (Logic a)]
forall a. HasCallStack => String -> a
error (String
"cannot convert unification variable " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarId a -> String
forall a. Show a => a -> String
show VarId a
x String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" to list")

instance (Num (Logic a)) => Num (Term a) where
  fromInteger :: Integer -> Term a
fromInteger = Logic a -> Term a
forall a. Logic a -> Term a
Value (Logic a -> Term a) -> (Integer -> Logic a) -> Integer -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Logic a
forall a. Num a => Integer -> a
fromInteger
  + :: Term a -> Term a -> Term a
(+) = String
-> (Logic a -> Logic a -> Logic a) -> Term a -> Term a -> Term a
forall a b c.
String
-> (Logic a -> Logic b -> Logic c) -> Term a -> Term b -> Term c
unsafePromoteBinOp String
"(+)" Logic a -> Logic a -> Logic a
forall a. Num a => a -> a -> a
(+)
  (-) = String
-> (Logic a -> Logic a -> Logic a) -> Term a -> Term a -> Term a
forall a b c.
String
-> (Logic a -> Logic b -> Logic c) -> Term a -> Term b -> Term c
unsafePromoteBinOp String
"(-)" (-)
  * :: Term a -> Term a -> Term a
(*) = String
-> (Logic a -> Logic a -> Logic a) -> Term a -> Term a -> Term a
forall a b c.
String
-> (Logic a -> Logic b -> Logic c) -> Term a -> Term b -> Term c
unsafePromoteBinOp String
"(*)" Logic a -> Logic a -> Logic a
forall a. Num a => a -> a -> a
(*)
  abs :: Term a -> Term a
abs = String -> (Logic a -> Logic a) -> Term a -> Term a
forall a b. String -> (Logic a -> Logic b) -> Term a -> Term b
unsafePromoteUnaryOp String
"abs" Logic a -> Logic a
forall a. Num a => a -> a
abs
  signum :: Term a -> Term a
signum = String -> (Logic a -> Logic a) -> Term a -> Term a
forall a b. String -> (Logic a -> Logic b) -> Term a -> Term b
unsafePromoteUnaryOp String
"signum" Logic a -> Logic a
forall a. Num a => a -> a
signum
  negate :: Term a -> Term a
negate = String -> (Logic a -> Logic a) -> Term a -> Term a
forall a b. String -> (Logic a -> Logic b) -> Term a -> Term b
unsafePromoteUnaryOp String
"negate" Logic a -> Logic a
forall a. Num a => a -> a
negate

unsafePromoteUnaryOp :: String -> (Logic a -> Logic b) -> Term a -> Term b
unsafePromoteUnaryOp :: forall a b. String -> (Logic a -> Logic b) -> Term a -> Term b
unsafePromoteUnaryOp String
_name Logic a -> Logic b
f (Value Logic a
x) = Logic b -> Term b
forall a. Logic a -> Term a
Value (Logic a -> Logic b
f Logic a
x)
unsafePromoteUnaryOp String
name Logic a -> Logic b
_f (Var VarId a
x) = String -> Term b
forall a. HasCallStack => String -> a
error (String
"cannot apply " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
name String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" to the unification variable " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarId a -> String
forall a. Show a => a -> String
show VarId a
x)

unsafePromoteBinOp :: String -> (Logic a -> Logic b -> Logic c) -> Term a -> Term b -> Term c
unsafePromoteBinOp :: forall a b c.
String
-> (Logic a -> Logic b -> Logic c) -> Term a -> Term b -> Term c
unsafePromoteBinOp String
_name Logic a -> Logic b -> Logic c
f (Value Logic a
x) (Value Logic b
y) = Logic c -> Term c
forall a. Logic a -> Term a
Value (Logic a -> Logic b -> Logic c
f Logic a
x Logic b
y)
unsafePromoteBinOp String
name Logic a -> Logic b -> Logic c
_f (Var VarId a
x) Term b
_ = String -> Term c
forall a. HasCallStack => String -> a
error (String
"cannot apply " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
name String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" to the unification variable " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarId a -> String
forall a. Show a => a -> String
show VarId a
x)
unsafePromoteBinOp String
name Logic a -> Logic b -> Logic c
_f Term a
_ (Var VarId b
x) = String -> Term c
forall a. HasCallStack => String -> a
error (String
"cannot apply " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
name String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" to the unification variable " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarId b -> String
forall a. Show a => a -> String
show VarId b
x)

-- | Treat a type as atomic, i.e. containing no variables inside. This requires
-- @a@ only to have an 'Eq' instance, thus ignoring its logical representation
-- if it exists. Useful when you really don't want to look inside something.
--
-- > type Symbol = Atomic String
newtype Atomic a = Atomic a
  deriving newtype (Atomic a -> Atomic a -> Bool
(Atomic a -> Atomic a -> Bool)
-> (Atomic a -> Atomic a -> Bool) -> Eq (Atomic a)
forall a. Eq a => Atomic a -> Atomic a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Atomic a -> Atomic a -> Bool
== :: Atomic a -> Atomic a -> Bool
$c/= :: forall a. Eq a => Atomic a -> Atomic a -> Bool
/= :: Atomic a -> Atomic a -> Bool
Eq, Atomic a -> ()
(Atomic a -> ()) -> NFData (Atomic a)
forall a. NFData a => Atomic a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => Atomic a -> ()
rnf :: Atomic a -> ()
NFData)

instance (Eq a) => Logical (Atomic a)
instance (Show a) => Show (Atomic a) where
  show :: Atomic a -> String
show (Atomic a
x) = a -> String
forall a. Show a => a -> String
show a
x
instance (Eq a) => Normalizable (Atomic a)

-- | 'unify', but on 'Term's instead of 'Logic' values. If new knowledge is
-- obtained during unification, it is obtained here.
unify' :: (Logical a) => Term a -> Term a -> State -> Maybe State
unify' :: forall a. Logical a => Term a -> Term a -> State -> Maybe State
unify' Term a
l Term a
r State
state =
  case (State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
shallowWalk State
state Term a
l, State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
shallowWalk State
state Term a
r) of
    (Var VarId a
x, Var VarId a
y)
      | VarId a
x VarId a -> VarId a -> Bool
forall a. Eq a => a -> a -> Bool
== VarId a
y -> State -> Maybe State
forall a. a -> Maybe a
Just State
state
    (Var VarId a
x, Term a
r')
      | VarId a -> Term a -> State -> Bool
forall a b. Logical a => VarId b -> Term a -> State -> Bool
occursCheck' VarId a
x Term a
r' State
state -> Maybe State
forall a. Maybe a
Nothing
      | Bool
otherwise -> VarId a -> Term a -> State -> Maybe State
forall a. Logical a => VarId a -> Term a -> State -> Maybe State
addSubst VarId a
x Term a
r' State
state
    (Term a
l', Var VarId a
y)
      | VarId a -> Term a -> State -> Bool
forall a b. Logical a => VarId b -> Term a -> State -> Bool
occursCheck' VarId a
y Term a
l' State
state -> Maybe State
forall a. Maybe a
Nothing
      | Bool
otherwise -> VarId a -> Term a -> State -> Maybe State
forall a. Logical a => VarId a -> Term a -> State -> Maybe State
addSubst VarId a
y Term a
l' State
state
    (Value Logic a
l', Value Logic a
r') -> Logic a -> Logic a -> State -> Maybe State
forall a. Logical a => Logic a -> Logic a -> State -> Maybe State
unify Logic a
l' Logic a
r' State
state

occursCheck' :: (Logical a) => VarId b -> Term a -> State -> Bool
occursCheck' :: forall a b. Logical a => VarId b -> Term a -> State -> Bool
occursCheck' VarId b
x Term a
t State
state =
  case State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
shallowWalk State
state Term a
t of
    Var VarId a
y -> VarId b -> VarId a
forall a b. Coercible a b => a -> b
coerce VarId b
x VarId a -> VarId a -> Bool
forall a. Eq a => a -> a -> Bool
== VarId a
y
    Value Logic a
v -> VarId b -> Logic a -> State -> Bool
forall b. VarId b -> Logic a -> State -> Bool
forall a b. Logical a => VarId b -> Logic a -> State -> Bool
occursCheck VarId b
x Logic a
v State
state

-- | 'walk', but on 'Term's instead of 'Logic' values. The actual substitution
-- of variables with values happens here.
walk' :: (Logical a) => State -> Term a -> Term a
walk' :: forall a. Logical a => State -> Term a -> Term a
walk' State
state Term a
x = case State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
shallowWalk State
state Term a
x of
  Var VarId a
i -> VarId a -> Term a
forall a. VarId a -> Term a
Var VarId a
i
  Value Logic a
v -> Logic a -> Term a
forall a. Logic a -> Term a
Value (State -> Logic a -> Logic a
forall a. Logical a => State -> Logic a -> Logic a
walk State
state Logic a
v)

-- | 'inject', but to a 'Term' instead of a 'Logic' value. You will use this
-- function in your relational programs to inject normal values.
--
-- > run (\x -> x === inject' [1, 2, 3])
inject' :: (Logical a) => a -> Term a
inject' :: forall a. Logical a => a -> Term a
inject' = Logic a -> Term a
forall a. Logic a -> Term a
Value (Logic a -> Term a) -> (a -> Logic a) -> a -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Logic a
forall a. Logical a => a -> Logic a
inject

-- | 'extract', but from a 'Term' instead of a 'Logic' value. Note that this
-- transformation can fail in the general case, because variables cannot be
-- transformed to values.
--
-- You will use this function to transform solutions of a program back to their
-- normal representation.
--
-- >>> extract' <$> run (\x -> x === inject' (Left 42 :: Either Int Bool))
-- [Just (Left 42)]
extract' :: (Logical a) => Term a -> Maybe a
extract' :: forall a. Logical a => Term a -> Maybe a
extract' Var{} = Maybe a
forall a. Maybe a
Nothing
extract' (Value Logic a
x) = Logic a -> Maybe a
forall a. Logical a => Logic a -> Maybe a
extract Logic a
x

data Normalization = Normalization (IntMap Int) Int
newtype Normalizer a = Normalizer (Normalization -> (Normalization, a)) deriving ((forall a b. (a -> b) -> Normalizer a -> Normalizer b)
-> (forall a b. a -> Normalizer b -> Normalizer a)
-> Functor Normalizer
forall a b. a -> Normalizer b -> Normalizer a
forall a b. (a -> b) -> Normalizer a -> Normalizer b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Normalizer a -> Normalizer b
fmap :: forall a b. (a -> b) -> Normalizer a -> Normalizer b
$c<$ :: forall a b. a -> Normalizer b -> Normalizer a
<$ :: forall a b. a -> Normalizer b -> Normalizer a
Functor)

instance Applicative Normalizer where
  pure :: forall a. a -> Normalizer a
pure a
x = (Normalization -> (Normalization, a)) -> Normalizer a
forall a. (Normalization -> (Normalization, a)) -> Normalizer a
Normalizer (,a
x)
  <*> :: forall a b. Normalizer (a -> b) -> Normalizer a -> Normalizer b
(<*>) = Normalizer (a -> b) -> Normalizer a -> Normalizer b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Normalizer where
  return :: forall a. a -> Normalizer a
return = a -> Normalizer a
forall a. a -> Normalizer a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Normalizer Normalization -> (Normalization, a)
f >>= :: forall a b. Normalizer a -> (a -> Normalizer b) -> Normalizer b
>>= a -> Normalizer b
g = (Normalization -> (Normalization, b)) -> Normalizer b
forall a. (Normalization -> (Normalization, a)) -> Normalizer a
Normalizer ((Normalization -> (Normalization, b)) -> Normalizer b)
-> (Normalization -> (Normalization, b)) -> Normalizer b
forall a b. (a -> b) -> a -> b
$ \Normalization
state ->
    let (Normalization
state', a
x) = Normalization -> (Normalization, a)
f Normalization
state
        Normalizer Normalization -> (Normalization, b)
h = a -> Normalizer b
g a
x
     in Normalization -> (Normalization, b)
h Normalization
state'

class (Logical a) => Normalizable a where
  normalize :: (forall i. VarId i -> Normalizer (VarId i)) -> Logic a -> Normalizer (Logic a)
  default normalize :: (a ~ Logic a) => (forall i. VarId i -> Normalizer (VarId i)) -> Logic a -> Normalizer (Logic a)
  normalize forall i. VarId i -> Normalizer (VarId i)
_ = a -> Normalizer a
Logic a -> Normalizer (Logic a)
forall a. a -> Normalizer a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

normalize' :: (Normalizable a) => (forall i. VarId i -> Normalizer (VarId i)) -> Term a -> Normalizer (Term a)
normalize' :: forall a.
Normalizable a =>
(forall i. VarId i -> Normalizer (VarId i))
-> Term a -> Normalizer (Term a)
normalize' forall i. VarId i -> Normalizer (VarId i)
f (Var VarId a
varId) = VarId a -> Term a
forall a. VarId a -> Term a
Var (VarId a -> Term a) -> Normalizer (VarId a) -> Normalizer (Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarId a -> Normalizer (VarId a)
forall i. VarId i -> Normalizer (VarId i)
f VarId a
varId
normalize' forall i. VarId i -> Normalizer (VarId i)
f (Value Logic a
x) = Logic a -> Term a
forall a. Logic a -> Term a
Value (Logic a -> Term a) -> Normalizer (Logic a) -> Normalizer (Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall i. VarId i -> Normalizer (VarId i))
-> Logic a -> Normalizer (Logic a)
forall a.
Normalizable a =>
(forall i. VarId i -> Normalizer (VarId i))
-> Logic a -> Normalizer (Logic a)
normalize VarId i -> Normalizer (VarId i)
forall i. VarId i -> Normalizer (VarId i)
f Logic a
x

runNormalize :: (Normalizable a) => Term a -> Term a
runNormalize :: forall a. Normalizable a => Term a -> Term a
runNormalize Term a
x = Term a
normalized
 where
  Normalizer Normalization -> (Normalization, Term a)
g = (forall i. VarId i -> Normalizer (VarId i))
-> Term a -> Normalizer (Term a)
forall a.
Normalizable a =>
(forall i. VarId i -> Normalizer (VarId i))
-> Term a -> Normalizer (Term a)
normalize' VarId i -> Normalizer (VarId i)
forall i. VarId i -> Normalizer (VarId i)
forall {a} {a}. VarId a -> Normalizer (VarId a)
addVar Term a
x
  (Normalization
_, Term a
normalized) = Normalization -> (Normalization, Term a)
g (IntMap Int -> Int -> Normalization
Normalization IntMap Int
forall a. IntMap a
IntMap.empty Int
0)
  addVar :: VarId a -> Normalizer (VarId a)
addVar (VarId Int
varId) = (Normalization -> (Normalization, VarId a)) -> Normalizer (VarId a)
forall a. (Normalization -> (Normalization, a)) -> Normalizer a
Normalizer ((Normalization -> (Normalization, VarId a))
 -> Normalizer (VarId a))
-> (Normalization -> (Normalization, VarId a))
-> Normalizer (VarId a)
forall a b. (a -> b) -> a -> b
$ \n :: Normalization
n@(Normalization IntMap Int
vars Int
maxId) ->
    case Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
varId IntMap Int
vars of
      Just Int
varId' -> (Normalization
n, Int -> VarId a
forall a. Int -> VarId a
VarId Int
varId')
      Maybe Int
Nothing -> (IntMap Int -> Int -> Normalization
Normalization IntMap Int
vars' Int
maxId', Int -> VarId a
forall a. Int -> VarId a
VarId Int
maxId)
       where
        maxId' :: Int
maxId' = Int
maxId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        vars' :: IntMap Int
vars' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
varId Int
maxId IntMap Int
vars

-- | Add a constraint that two terms must not be equal.
disequality :: (Logical a) => Term a -> Term a -> State -> Maybe State
disequality :: forall a. Logical a => Term a -> Term a -> State -> Maybe State
disequality Term a
left Term a
right State
state = case Term a -> Term a -> State -> Maybe Subst
forall a. Logical a => Term a -> Term a -> State -> Maybe Subst
addedSubst Term a
left Term a
right State
state of
  Maybe Subst
Nothing -> State -> Maybe State
forall a. a -> Maybe a
Just State
state
  Just Subst
added -> Subst -> State -> Maybe State
stateInsertDisequality Subst
added State
state

-- | Since 'Term's are polymorphic, we cannot easily store them in the
-- substitution map. 'ErasedTerm' is the way to erase the type before putting
-- a 'Term' into the map.
data ErasedTerm where
  ErasedTerm :: (Logical a) => Term a -> ErasedTerm

instance Show ErasedTerm where
  show :: ErasedTerm -> String
show (ErasedTerm (Var VarId a
varId)) = String
"Var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId a -> String
forall a. Show a => a -> String
show VarId a
varId
  show (ErasedTerm (Value Logic a
_)) = String
"Value _"

-- | Cast an 'ErasedTerm' back to a 'Term a'. Hopefully, you will cast it to the
-- correct type, or bad things will happen.
unsafeReconstructTerm :: ErasedTerm -> Term a
unsafeReconstructTerm :: forall a. ErasedTerm -> Term a
unsafeReconstructTerm (ErasedTerm Term a
x) = Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
x

-- | Current knowledge of variable values.
newtype Subst = Subst (IntMap ErasedTerm) deriving (Int -> Subst -> ShowS
[Subst] -> ShowS
Subst -> String
(Int -> Subst -> ShowS)
-> (Subst -> String) -> ([Subst] -> ShowS) -> Show Subst
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Subst -> ShowS
showsPrec :: Int -> Subst -> ShowS
$cshow :: Subst -> String
show :: Subst -> String
$cshowList :: [Subst] -> ShowS
showList :: [Subst] -> ShowS
Show)

substEmpty :: Subst
substEmpty :: Subst
substEmpty = IntMap ErasedTerm -> Subst
Subst IntMap ErasedTerm
forall a. IntMap a
IntMap.empty

substNull :: Subst -> Bool
substNull :: Subst -> Bool
substNull (Subst IntMap ErasedTerm
m) = IntMap ErasedTerm -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap ErasedTerm
m

-- | “Arbitrary” in the sense that this function decides which particular entry
-- to look up, but for the caller it's just some entry from the map. This
-- function must agree on this arbitrary entry with 'substExtractArbitrary'.
substLookupArbitraryId :: Subst -> Maybe Int
substLookupArbitraryId :: Subst -> Maybe Int
substLookupArbitraryId (Subst IntMap ErasedTerm
m) = (Int, ErasedTerm) -> Int
forall a b. (a, b) -> a
fst ((Int, ErasedTerm) -> Int) -> Maybe (Int, ErasedTerm) -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap ErasedTerm -> Maybe (Int, ErasedTerm)
forall a. IntMap a -> Maybe (Int, a)
IntMap.lookupMin IntMap ErasedTerm
m

substExtractArbitrary :: Subst -> Maybe ((Int, ErasedTerm), Subst)
substExtractArbitrary :: Subst -> Maybe ((Int, ErasedTerm), Subst)
substExtractArbitrary (Subst IntMap ErasedTerm
m) = (IntMap ErasedTerm -> Subst)
-> ((Int, ErasedTerm), IntMap ErasedTerm)
-> ((Int, ErasedTerm), Subst)
forall a b.
(a -> b) -> ((Int, ErasedTerm), a) -> ((Int, ErasedTerm), b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IntMap ErasedTerm -> Subst
Subst (((Int, ErasedTerm), IntMap ErasedTerm)
 -> ((Int, ErasedTerm), Subst))
-> Maybe ((Int, ErasedTerm), IntMap ErasedTerm)
-> Maybe ((Int, ErasedTerm), Subst)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap ErasedTerm -> Maybe ((Int, ErasedTerm), IntMap ErasedTerm)
forall a. IntMap a -> Maybe ((Int, a), IntMap a)
IntMap.minViewWithKey IntMap ErasedTerm
m

addedSubst :: (Logical a) => Term a -> Term a -> State -> Maybe Subst
addedSubst :: forall a. Logical a => Term a -> Term a -> State -> Maybe Subst
addedSubst Term a
left Term a
right State
state = State -> Subst
knownSubst (State -> Subst) -> Maybe State -> Maybe Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term a -> Term a -> State -> Maybe State
forall a. Logical a => Term a -> Term a -> State -> Maybe State
unify' Term a
left' Term a
right' State
empty
 where
  left' :: Term a
left' = State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
walk' State
state Term a
left
  right' :: Term a
right' = State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
walk' State
state Term a
right

instance Semigroup Subst where
  Subst IntMap ErasedTerm
l <> :: Subst -> Subst -> Subst
<> Subst IntMap ErasedTerm
r = IntMap ErasedTerm -> Subst
Subst (IntMap ErasedTerm
l IntMap ErasedTerm -> IntMap ErasedTerm -> IntMap ErasedTerm
forall a. Semigroup a => a -> a -> a
<> IntMap ErasedTerm
r)

-- | Disequality constraints.
--
-- We try to perform the same optimization as @faster-minikanren@ does. If
-- we meet a constraint @(x, y) =/= (1, 2)@, we can transform it to
-- @x /= 1 || y /= 2@. But note that every disequality must be falsified for the
-- constraint to fail. Hence we do not need to attach this constraint to every
-- variable; we only need to pick one variable and attach the whole constraint
-- to it.
--
-- > x => [(1, y => 2)]
--
-- Together with the disallowed value for @x@, we store a map with the rest of
-- disequalities for this constraint. If we find that @x@ is 1, we merge that
-- map into 'Disequalities'. If that map is empty however, it means that the
-- constraint must fail. If we first learn that @y@ is 2, we don't care until
-- @x /= 1@ is falsified.
--
-- If there are several constraints on @x@, they'll be stored in a list.
--
-- > x => [(1, y => 2), (2, empty)]
--
-- If @x@ turns out to be 1, there are still other disequalities to check,
-- but if @x@ becomes 2, then we fail. If @x@ is anything else, we just drop
-- all constraints attached to it.
newtype Disequalities = Disequalities (IntMap [(ErasedTerm, Subst)])
  deriving (Int -> Disequalities -> ShowS
[Disequalities] -> ShowS
Disequalities -> String
(Int -> Disequalities -> ShowS)
-> (Disequalities -> String)
-> ([Disequalities] -> ShowS)
-> Show Disequalities
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Disequalities -> ShowS
showsPrec :: Int -> Disequalities -> ShowS
$cshow :: Disequalities -> String
show :: Disequalities -> String
$cshowList :: [Disequalities] -> ShowS
showList :: [Disequalities] -> ShowS
Show)

disequalitiesInsert :: Subst -> Disequalities -> Maybe Disequalities
disequalitiesInsert :: Subst -> Disequalities -> Maybe Disequalities
disequalitiesInsert Subst
subst (Disequalities IntMap [(ErasedTerm, Subst)]
d) = do
  ((Int
varId, ErasedTerm
value), Subst
subst') <- Subst -> Maybe ((Int, ErasedTerm), Subst)
substExtractArbitrary Subst
subst
  let entry' :: [(ErasedTerm, Subst)]
entry' = (ErasedTerm
value, Subst
subst') (ErasedTerm, Subst)
-> [(ErasedTerm, Subst)] -> [(ErasedTerm, Subst)]
forall a. a -> [a] -> [a]
: [(ErasedTerm, Subst)]
-> Maybe [(ErasedTerm, Subst)] -> [(ErasedTerm, Subst)]
forall a. a -> Maybe a -> a
fromMaybe [] (Int -> IntMap [(ErasedTerm, Subst)] -> Maybe [(ErasedTerm, Subst)]
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
varId IntMap [(ErasedTerm, Subst)]
d)
  Disequalities -> Maybe Disequalities
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap [(ErasedTerm, Subst)] -> Disequalities
Disequalities (Int
-> [(ErasedTerm, Subst)]
-> IntMap [(ErasedTerm, Subst)]
-> IntMap [(ErasedTerm, Subst)]
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
varId [(ErasedTerm, Subst)]
entry' IntMap [(ErasedTerm, Subst)]
d))

disequalitiesExtract
  :: VarId a
  -> Disequalities
  -> Maybe ([(Term a, Subst)], Disequalities)
disequalitiesExtract :: forall a.
VarId a
-> Disequalities -> Maybe ([(Term a, Subst)], Disequalities)
disequalitiesExtract (VarId Int
varId) (Disequalities IntMap [(ErasedTerm, Subst)]
d) = do
  [(ErasedTerm, Subst)]
entry <- Int -> IntMap [(ErasedTerm, Subst)] -> Maybe [(ErasedTerm, Subst)]
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
varId IntMap [(ErasedTerm, Subst)]
d
  let entry' :: [(Term a, Subst)]
entry' = ((ErasedTerm, Subst) -> (Term a, Subst))
-> [(ErasedTerm, Subst)] -> [(Term a, Subst)]
forall a b. (a -> b) -> [a] -> [b]
map ((ErasedTerm -> Term a) -> (ErasedTerm, Subst) -> (Term a, Subst)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ErasedTerm -> Term a
forall a. ErasedTerm -> Term a
unsafeReconstructTerm) [(ErasedTerm, Subst)]
entry

  let withoutEntry :: Disequalities
withoutEntry = IntMap [(ErasedTerm, Subst)] -> Disequalities
Disequalities (Int -> IntMap [(ErasedTerm, Subst)] -> IntMap [(ErasedTerm, Subst)]
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
varId IntMap [(ErasedTerm, Subst)]
d)
  ([(Term a, Subst)], Disequalities)
-> Maybe ([(Term a, Subst)], Disequalities)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Term a, Subst)]
entry', Disequalities
withoutEntry)

disequalitiesUpdate
  :: (Logical a)
  => State
  -> VarId a
  -> Term a
  -> Disequalities
  -> Maybe Disequalities
disequalitiesUpdate :: forall a.
Logical a =>
State -> VarId a -> Term a -> Disequalities -> Maybe Disequalities
disequalitiesUpdate State
state VarId a
varId Term a
value Disequalities
d =
  case VarId a
-> Disequalities -> Maybe ([(Term a, Subst)], Disequalities)
forall a.
VarId a
-> Disequalities -> Maybe ([(Term a, Subst)], Disequalities)
disequalitiesExtract VarId a
varId Disequalities
d of
    Maybe ([(Term a, Subst)], Disequalities)
Nothing -> Disequalities -> Maybe Disequalities
forall a. a -> Maybe a
Just Disequalities
d
    Just ([(Term a, Subst)]
varDisequalities, Disequalities
d') ->
      ((Term a, Subst) -> Disequalities -> Maybe Disequalities)
-> Disequalities -> [(Term a, Subst)] -> Maybe Disequalities
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (Term a, Subst) -> Disequalities -> Maybe Disequalities
updateDisequality Disequalities
d' [(Term a, Subst)]
varDisequalities
 where
  value' :: Term a
value' = State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
walk' State
state Term a
value
  updateDisequality :: (Term a, Subst) -> Disequalities -> Maybe Disequalities
updateDisequality (Term a
disallowedValue, Subst
subst) Disequalities
d' =
    case Term a -> Term a -> State -> Maybe Subst
forall a. Logical a => Term a -> Term a -> State -> Maybe Subst
addedSubst Term a
value' Term a
disallowedValue State
state of
      Maybe Subst
Nothing -> Disequalities -> Maybe Disequalities
forall a. a -> Maybe a
Just Disequalities
d'
      Just Subst
added
        | Subst -> Bool
substNull Subst
subst' -> Maybe Disequalities
forall a. Maybe a
Nothing
        | Bool
otherwise -> Subst -> Disequalities -> Maybe Disequalities
disequalitiesInsert Subst
subst' Disequalities
d'
       where
        subst' :: Subst
subst' = State -> Subst -> Subst
updateComponents State
state (Subst
subst Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
added)

updateComponents :: State -> Subst -> Subst
updateComponents :: State -> Subst -> Subst
updateComponents State
state Subst
subst = case Subst -> Maybe ((Int, ErasedTerm), Subst)
substExtractArbitrary Subst
subst of
  Maybe ((Int, ErasedTerm), Subst)
Nothing -> Subst
subst
  Just ((Int
varId, ErasedTerm Term a
value), Subst
subst') ->
    case Subst -> Maybe Int
substLookupArbitraryId Subst
subst'' of
      Just Int
varId' | Int
varId Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
varId' -> Subst
subst''
      Maybe Int
_ -> State -> Subst -> Subst
updateComponents State
state Subst
subst''
   where
    added :: Subst
added = Subst -> Maybe Subst -> Subst
forall a. a -> Maybe a -> a
fromMaybe Subst
substEmpty (Term a -> Term a -> State -> Maybe Subst
forall a. Logical a => Term a -> Term a -> State -> Maybe Subst
addedSubst (VarId a -> Term a
forall a. VarId a -> Term a
Var (Int -> VarId a
forall a. Int -> VarId a
VarId Int
varId)) Term a
value State
state)
    subst'' :: Subst
subst'' = Subst
subst' Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
added

-- | One branch in the search tree. Keeps track of known substitutions and
-- variables.
data State = State
  { State -> Subst
knownSubst :: !Subst
  , State -> Disequalities
disequalities :: !Disequalities
  , State -> Int
maxVarId :: !Int
  }
  deriving (Int -> State -> ShowS
[State] -> ShowS
State -> String
(Int -> State -> ShowS)
-> (State -> String) -> ([State] -> ShowS) -> Show State
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> State -> ShowS
showsPrec :: Int -> State -> ShowS
$cshow :: State -> String
show :: State -> String
$cshowList :: [State] -> ShowS
showList :: [State] -> ShowS
Show)

-- | The initial state without any knowledge and variables.
empty :: State
empty :: State
empty =
  State
    { knownSubst :: Subst
knownSubst = Subst
substEmpty
    , disequalities :: Disequalities
disequalities = IntMap [(ErasedTerm, Subst)] -> Disequalities
Disequalities IntMap [(ErasedTerm, Subst)]
forall a. IntMap a
IntMap.empty
    , maxVarId :: Int
maxVarId = Int
0
    }

-- | Create a variable in the given state.
makeVariable :: State -> (State, Term a)
makeVariable :: forall a. State -> (State, Term a)
makeVariable State{Int
maxVarId :: State -> Int
maxVarId :: Int
maxVarId, Disequalities
Subst
knownSubst :: State -> Subst
disequalities :: State -> Disequalities
knownSubst :: Subst
disequalities :: Disequalities
..} = (State
state', Term a
var)
 where
  var :: Term a
var = VarId a -> Term a
forall a. VarId a -> Term a
Var (Int -> VarId a
forall a. Int -> VarId a
VarId Int
maxVarId)
  state' :: State
state' = State{maxVarId :: Int
maxVarId = Int
maxVarId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Disequalities
Subst
knownSubst :: Subst
disequalities :: Disequalities
knownSubst :: Subst
disequalities :: Disequalities
..}

shallowWalk :: (Logical a) => State -> Term a -> Term a
shallowWalk :: forall a. Logical a => State -> Term a -> Term a
shallowWalk State
_ (Value Logic a
v) = Logic a -> Term a
forall a. Logic a -> Term a
Value Logic a
v
shallowWalk state :: State
state@State{knownSubst :: State -> Subst
knownSubst = Subst IntMap ErasedTerm
m} (Var (VarId Int
i)) =
  case Int -> IntMap ErasedTerm -> Maybe ErasedTerm
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap ErasedTerm
m of
    Maybe ErasedTerm
Nothing -> VarId a -> Term a
forall a. VarId a -> Term a
Var (Int -> VarId a
forall a. Int -> VarId a
VarId Int
i)
    Just ErasedTerm
v -> State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
shallowWalk State
state (ErasedTerm -> Term a
forall a. ErasedTerm -> Term a
unsafeReconstructTerm ErasedTerm
v)

addSubst :: (Logical a) => VarId a -> Term a -> State -> Maybe State
addSubst :: forall a. Logical a => VarId a -> Term a -> State -> Maybe State
addSubst (VarId Int
i) Term a
value State{knownSubst :: State -> Subst
knownSubst = Subst IntMap ErasedTerm
m, Int
Disequalities
disequalities :: State -> Disequalities
maxVarId :: State -> Int
disequalities :: Disequalities
maxVarId :: Int
..} =
  VarId a -> Term a -> State -> Maybe State
forall a. Logical a => VarId a -> Term a -> State -> Maybe State
stateUpdateDisequalities (Int -> VarId a
forall a. Int -> VarId a
VarId Int
i) Term a
value (State -> Maybe State) -> State -> Maybe State
forall a b. (a -> b) -> a -> b
$
    State
      { knownSubst :: Subst
knownSubst = IntMap ErasedTerm -> Subst
Subst (IntMap ErasedTerm -> Subst) -> IntMap ErasedTerm -> Subst
forall a b. (a -> b) -> a -> b
$ Int -> ErasedTerm -> IntMap ErasedTerm -> IntMap ErasedTerm
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Term a -> ErasedTerm
forall a. Logical a => Term a -> ErasedTerm
ErasedTerm Term a
value) IntMap ErasedTerm
m
      , Int
Disequalities
disequalities :: Disequalities
maxVarId :: Int
disequalities :: Disequalities
maxVarId :: Int
..
      }

stateInsertDisequality :: Subst -> State -> Maybe State
stateInsertDisequality :: Subst -> State -> Maybe State
stateInsertDisequality Subst
subst state :: State
state@State{Disequalities
disequalities :: State -> Disequalities
disequalities :: Disequalities
disequalities} = do
  Disequalities
disequalities' <- Subst -> Disequalities -> Maybe Disequalities
disequalitiesInsert Subst
subst Disequalities
disequalities
  State -> Maybe State
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return State
state{disequalities = disequalities'}

stateUpdateDisequalities
  :: (Logical a)
  => VarId a
  -> Term a
  -> State
  -> Maybe State
stateUpdateDisequalities :: forall a. Logical a => VarId a -> Term a -> State -> Maybe State
stateUpdateDisequalities VarId a
varId Term a
value state :: State
state@State{Disequalities
disequalities :: State -> Disequalities
disequalities :: Disequalities
disequalities} = do
  Disequalities
disequalities' <- State -> VarId a -> Term a -> Disequalities -> Maybe Disequalities
forall a.
Logical a =>
State -> VarId a -> Term a -> Disequalities -> Maybe Disequalities
disequalitiesUpdate State
state VarId a
varId Term a
value Disequalities
disequalities
  State -> Maybe State
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (State
state{disequalities = disequalities'})