-- | Basing on the Nix (Hindley–Milner) type system (that provides decidable type inference):
-- gathering assumptions (inference evidence) about polymorphic types.
module Nix.Type.Assumption
  ( Assumption(..)
  , empty
  , lookup
  , remove
  , extend
  , keys
  , merge
  , mergeAssumptions
  , singleton
  )
where

import           Prelude                 hiding ( Type
                                                , empty
                                                )

import           Nix.Type.Type

newtype Assumption = Assumption { Assumption -> [(Name, Type)]
assumptions :: [(Name, Type)] }
  deriving (Assumption -> Assumption -> Bool
(Assumption -> Assumption -> Bool)
-> (Assumption -> Assumption -> Bool) -> Eq Assumption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Assumption -> Assumption -> Bool
$c/= :: Assumption -> Assumption -> Bool
== :: Assumption -> Assumption -> Bool
$c== :: Assumption -> Assumption -> Bool
Eq, Int -> Assumption -> ShowS
[Assumption] -> ShowS
Assumption -> String
(Int -> Assumption -> ShowS)
-> (Assumption -> String)
-> ([Assumption] -> ShowS)
-> Show Assumption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Assumption] -> ShowS
$cshowList :: [Assumption] -> ShowS
show :: Assumption -> String
$cshow :: Assumption -> String
showsPrec :: Int -> Assumption -> ShowS
$cshowsPrec :: Int -> Assumption -> ShowS
Show)

empty :: Assumption
empty :: Assumption
empty = [(Name, Type)] -> Assumption
Assumption [(Name, Type)]
forall a. Monoid a => a
mempty

extend :: Assumption -> (Name, Type) -> Assumption
extend :: Assumption -> (Name, Type) -> Assumption
extend (Assumption [(Name, Type)]
a) (Name
x, Type
s) =
  [(Name, Type)] -> Assumption
Assumption ([(Name, Type)] -> Assumption) -> [(Name, Type)] -> Assumption
forall a b. (a -> b) -> a -> b
$
    (Name
x, Type
s) (Name, Type) -> [(Name, Type)] -> [(Name, Type)]
forall a. a -> [a] -> [a]
: [(Name, Type)]
a

remove :: Assumption -> Name -> Assumption
remove :: Assumption -> Name -> Assumption
remove (Assumption [(Name, Type)]
a) Name
var =
  [(Name, Type)] -> Assumption
Assumption ([(Name, Type)] -> Assumption) -> [(Name, Type)] -> Assumption
forall a b. (a -> b) -> a -> b
$
    ((Name, Type) -> Bool) -> [(Name, Type)] -> [(Name, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (\(Name
n, Type
_) -> Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
var)
      [(Name, Type)]
a

lookup :: Name -> Assumption -> [Type]
lookup :: Name -> Assumption -> [Type]
lookup Name
key (Assumption [(Name, Type)]
a) =
  (Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    ((Name, Type) -> Bool) -> [(Name, Type)] -> [(Name, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (\(Name
n, Type
_) -> Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
key)
      [(Name, Type)]
a

merge :: Assumption -> Assumption -> Assumption
merge :: Assumption -> Assumption -> Assumption
merge (Assumption [(Name, Type)]
a) (Assumption [(Name, Type)]
b) =
  [(Name, Type)] -> Assumption
Assumption ([(Name, Type)] -> Assumption) -> [(Name, Type)] -> Assumption
forall a b. (a -> b) -> a -> b
$ [(Name, Type)]
a [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Name, Type)]
b

mergeAssumptions :: [Assumption] -> Assumption
mergeAssumptions :: [Assumption] -> Assumption
mergeAssumptions = (Assumption -> Assumption -> Assumption)
-> Assumption -> [Assumption] -> Assumption
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Assumption -> Assumption -> Assumption
merge Assumption
empty

singleton :: Name -> Type -> Assumption
singleton :: Name -> Type -> Assumption
singleton Name
x Type
y = [(Name, Type)] -> Assumption
Assumption [(Name
x, Type
y)]

keys :: Assumption -> [Name]
keys :: Assumption -> [Name]
keys (Assumption [(Name, Type)]
a) = (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Name, Type)]
a