{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
-- Description: This module defines an effect signature for
-- computations that support doing unification.  The intention is for
-- code needing unification to use the operations defined in this
-- module, and then import 'Swarm.Effect.Unify.Fast' to dispatch the
-- 'Unification' effects.
module Swarm.Effect.Unify where

import Control.Algebra
import Data.Kind (Type)
import Data.Set (Set)
import Prettyprinter
import Swarm.Language.Types hiding (Type)
import Swarm.Pretty (PrettyPrec (..), ppr, reportBug)

-- | Data type representing available unification operations.
data Unification (m :: Type -> Type) k where
  Unify :: UType -> UType -> Unification m (Either UnificationError UType)
  ApplyBindings :: UType -> Unification m UType
  FreshIntVar :: Unification m IntVar
  FreeUVars :: UType -> Unification m (Set IntVar)

-- | Unify two types, returning a type equal to both, or a 'UnificationError' if
--   the types definitely do not unify.
(=:=) :: Has Unification sig m => UType -> UType -> m (Either UnificationError UType)
UType
t1 =:= :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> UType -> m (Either UnificationError UType)
=:= UType
t2 = Unification m (Either UnificationError UType)
-> m (Either UnificationError UType)
forall (eff :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member eff sig, Algebra sig m) =>
eff m a -> m a
send (UType -> UType -> Unification m (Either UnificationError UType)
forall (m :: * -> *).
UType -> UType -> Unification m (Either UnificationError UType)
Unify UType
t1 UType
t2)

-- | Substitute for all the unification variables that are currently
--   bound.  It is guaranteed that any unification variables remaining
--   in the result are not currently bound, /i.e./ we have learned no
--   information about them.
applyBindings :: Has Unification sig m => UType -> m UType
applyBindings :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings = Unification m UType -> m UType
forall (eff :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member eff sig, Algebra sig m) =>
eff m a -> m a
send (Unification m UType -> m UType)
-> (UType -> Unification m UType) -> UType -> m UType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UType -> Unification m UType
forall (m :: * -> *). UType -> Unification m UType
ApplyBindings

-- | Compute the set of free unification variables of a type (after
--   substituting away any which are already bound).
freeUVars :: Has Unification sig m => UType -> m (Set IntVar)
freeUVars :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m (Set IntVar)
freeUVars = Unification m (Set IntVar) -> m (Set IntVar)
forall (eff :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member eff sig, Algebra sig m) =>
eff m a -> m a
send (Unification m (Set IntVar) -> m (Set IntVar))
-> (UType -> Unification m (Set IntVar)) -> UType -> m (Set IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UType -> Unification m (Set IntVar)
forall (m :: * -> *). UType -> Unification m (Set IntVar)
FreeUVars

-- | Generate a fresh unification variable.
freshIntVar :: Has Unification sig m => m IntVar
freshIntVar :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m IntVar
freshIntVar = Unification m IntVar -> m IntVar
forall (eff :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member eff sig, Algebra sig m) =>
eff m a -> m a
send Unification m IntVar
forall (m :: * -> *). Unification m IntVar
FreshIntVar

-- | An error that occurred while running the unifier.
data UnificationError where
  -- | Occurs check failure, i.e. the solution to some unification
  --   equations was an infinite term.
  Infinite :: IntVar -> UType -> UnificationError
  -- | Mismatch error between the given terms.
  UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
  -- | Encountered an undefined/unknown type constructor.
  UndefinedUserType :: UType -> UnificationError
  -- | Encountered an unexpanded recursive type in unifyF.  This
  --   should never happen.
  UnexpandedRecTy :: TypeF UType -> UnificationError
  deriving (Int -> UnificationError -> ShowS
[UnificationError] -> ShowS
UnificationError -> String
(Int -> UnificationError -> ShowS)
-> (UnificationError -> String)
-> ([UnificationError] -> ShowS)
-> Show UnificationError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnificationError -> ShowS
showsPrec :: Int -> UnificationError -> ShowS
$cshow :: UnificationError -> String
show :: UnificationError -> String
$cshowList :: [UnificationError] -> ShowS
showList :: [UnificationError] -> ShowS
Show)

instance PrettyPrec UnificationError where
  prettyPrec :: forall ann. Int -> UnificationError -> Doc ann
prettyPrec Int
_ = \case
    Infinite IntVar
x UType
uty ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
        [ Doc ann
"Encountered infinite type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IntVar -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr IntVar
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
uty Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
        , Doc ann
"Swarm will not infer recursive types; if you want a recursive type, add an explicit type annotation."
        ]
    UnifyErr TypeF UType
ty1 TypeF UType
ty2 ->
      Doc ann
"Can't unify" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeF UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TypeF UType
ty1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"and" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeF UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TypeF UType
ty2
    UndefinedUserType UType
ty ->
      Doc ann
"Undefined user type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
ty
    UnexpandedRecTy TypeF UType
ty ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
        [ Doc ann
"Unexpanded recursive type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeF UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TypeF UType
ty Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"encountered in unifyF."
        , Doc ann
forall ann. Doc ann
reportBug
        ]