{-# language TypeFamilies #-}

-- | 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
  , singleton
  )
where

import           Nix.Prelude             hiding ( Type
                                                , empty
                                                )

import           Nix.Expr.Types
import           Nix.Type.Type

newtype Assumption = Assumption [(VarName, 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)

-- We pretend that Assumptions can be inconsistent (nonunique keys),
-- (just like people in real life).
-- The consistency between assumptions is the inference responcibility.
instance Semigroup Assumption where
  <> :: Assumption -> Assumption -> Assumption
(<>) = Assumption -> Assumption -> Assumption
merge

instance Monoid Assumption where
  mempty :: Assumption
mempty = Assumption
empty

instance One Assumption where
  type OneItem Assumption = (VarName, Type)
  one :: OneItem Assumption -> Assumption
one OneItem Assumption
vt = [(VarName, Type)] -> Assumption
Assumption ([(VarName, Type)] -> Assumption)
-> [(VarName, Type)] -> Assumption
forall a b. (a -> b) -> a -> b
$ OneItem [(VarName, Type)] -> [(VarName, Type)]
forall x. One x => OneItem x -> x
one OneItem [(VarName, Type)]
OneItem Assumption
vt

--  2022-01-12: NOTE: `empty` implies Alternative. Either have Alternative or use `mempty`
empty :: Assumption
empty :: Assumption
empty = [(VarName, Type)] -> Assumption
Assumption [(VarName, Type)]
forall a. Monoid a => a
mempty

extend :: Assumption -> (VarName, Type) -> Assumption
extend :: Assumption -> (VarName, Type) -> Assumption
extend Assumption
a (VarName, Type)
vt =
  OneItem Assumption -> Assumption
forall x. One x => OneItem x -> x
one ((VarName, Type) -> (VarName, Type)
coerce (VarName, Type)
vt) Assumption -> Assumption -> Assumption
forall a. Semigroup a => a -> a -> a
<> Assumption
a

remove :: Assumption -> VarName -> Assumption
remove :: Assumption -> VarName -> Assumption
remove Assumption
a VarName
var =
  ([(VarName, Type)] -> [(VarName, Type)])
-> Assumption -> Assumption
coerce
    [(VarName, Type)] -> [(VarName, Type)]
rmVar
    Assumption
a
 where
  rmVar :: [(VarName, Type)] -> [(VarName, Type)]
  rmVar :: [(VarName, Type)] -> [(VarName, Type)]
rmVar =
    ((VarName, Type) -> Bool) -> [(VarName, Type)] -> [(VarName, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (VarName -> VarName -> Bool
forall a. Eq a => a -> a -> Bool
(/=) VarName
var (VarName -> Bool)
-> ((VarName, Type) -> VarName) -> (VarName, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarName, Type) -> VarName
forall a b. (a, b) -> a
fst)

lookup :: VarName -> Assumption -> [Type]
lookup :: VarName -> Assumption -> [Type]
lookup VarName
key Assumption
a =
  (VarName, Type) -> Type
forall a b. (a, b) -> b
snd ((VarName, Type) -> Type) -> [(VarName, Type)] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    ((VarName, Type) -> Bool) -> [(VarName, Type)] -> [(VarName, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (VarName -> VarName -> Bool
forall a. Eq a => a -> a -> Bool
(==) VarName
key (VarName -> Bool)
-> ((VarName, Type) -> VarName) -> (VarName, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarName, Type) -> VarName
forall a b. (a, b) -> a
fst)
      (Assumption -> [(VarName, Type)]
coerce Assumption
a)

merge :: Assumption -> Assumption -> Assumption
merge :: Assumption -> Assumption -> Assumption
merge =
  ([(VarName, Type)] -> [(VarName, Type)] -> [(VarName, Type)])
-> Assumption -> Assumption -> Assumption
coerce (Semigroup [(VarName, Type)] =>
[(VarName, Type)] -> [(VarName, Type)] -> [(VarName, Type)]
forall a. Semigroup a => a -> a -> a
(<>) @[(VarName, Type)])

singleton :: VarName -> Type -> Assumption
singleton :: VarName -> Type -> Assumption
singleton = ((VarName, Type) -> Assumption) -> VarName -> Type -> Assumption
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (VarName, Type) -> Assumption
forall x. One x => OneItem x -> x
one

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