{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Hyper.Unify.Binding
( UVar (..)
, _UVar
, Binding (..)
, _Binding
, emptyBinding
, bindingDict
) where
import Control.Lens (ALens')
import qualified Control.Lens as Lens
import Control.Monad.State (MonadState (..))
import Data.Sequence (Seq)
import Hyper.Class.Unify (BindingDict (..))
import Hyper.Type (AHyperType, type (#))
import Hyper.Unify.Term
import Hyper.Internal.Prelude
newtype UVar (t :: AHyperType) = UVar Int
deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: AHyperType) x. Rep (UVar t) x -> UVar t
forall (t :: AHyperType) x. UVar t -> Rep (UVar t) x
$cto :: forall (t :: AHyperType) x. Rep (UVar t) x -> UVar t
$cfrom :: forall (t :: AHyperType) x. UVar t -> Rep (UVar t) x
Generic, Int -> UVar t -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: AHyperType). Int -> UVar t -> ShowS
forall (t :: AHyperType). [UVar t] -> ShowS
forall (t :: AHyperType). UVar t -> String
showList :: [UVar t] -> ShowS
$cshowList :: forall (t :: AHyperType). [UVar t] -> ShowS
show :: UVar t -> String
$cshow :: forall (t :: AHyperType). UVar t -> String
showsPrec :: Int -> UVar t -> ShowS
$cshowsPrec :: forall (t :: AHyperType). Int -> UVar t -> ShowS
Show)
deriving newtype (UVar t -> UVar t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: AHyperType). UVar t -> UVar t -> Bool
/= :: UVar t -> UVar t -> Bool
$c/= :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
== :: UVar t -> UVar t -> Bool
$c== :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
Eq, UVar t -> UVar t -> Bool
UVar t -> UVar t -> Ordering
UVar t -> UVar t -> UVar t
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (t :: AHyperType). Eq (UVar t)
forall (t :: AHyperType). UVar t -> UVar t -> Bool
forall (t :: AHyperType). UVar t -> UVar t -> Ordering
forall (t :: AHyperType). UVar t -> UVar t -> UVar t
min :: UVar t -> UVar t -> UVar t
$cmin :: forall (t :: AHyperType). UVar t -> UVar t -> UVar t
max :: UVar t -> UVar t -> UVar t
$cmax :: forall (t :: AHyperType). UVar t -> UVar t -> UVar t
>= :: UVar t -> UVar t -> Bool
$c>= :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
> :: UVar t -> UVar t -> Bool
$c> :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
<= :: UVar t -> UVar t -> Bool
$c<= :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
< :: UVar t -> UVar t -> Bool
$c< :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
compare :: UVar t -> UVar t -> Ordering
$ccompare :: forall (t :: AHyperType). UVar t -> UVar t -> Ordering
Ord)
makePrisms ''UVar
newtype Binding t = Binding (Seq (UTerm UVar t))
deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: AHyperType) x. Rep (Binding t) x -> Binding t
forall (t :: AHyperType) x. Binding t -> Rep (Binding t) x
$cto :: forall (t :: AHyperType) x. Rep (Binding t) x -> Binding t
$cfrom :: forall (t :: AHyperType) x. Binding t -> Rep (Binding t) x
Generic)
makePrisms ''Binding
makeCommonInstances [''Binding]
emptyBinding :: Binding t
emptyBinding :: forall (t :: AHyperType). Binding t
emptyBinding = forall (t :: AHyperType). Seq (UTerm UVar t) -> Binding t
Binding forall a. Monoid a => a
mempty
{-# INLINE bindingDict #-}
bindingDict ::
MonadState s m =>
ALens' s (Binding # t) ->
BindingDict UVar m t
bindingDict :: forall s (m :: * -> *) (t :: HyperType).
MonadState s m =>
ALens' s (Binding # t) -> BindingDict UVar m t
bindingDict ALens' s (Binding # t)
l =
BindingDict
{ lookupVar :: (UVar # t) -> m (UTerm UVar ('AHyperType t))
lookupVar =
\(UVar Int
h) ->
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
Lens.use (forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType) (t :: AHyperType).
Iso
(Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
h)
, newVar :: UTerm UVar ('AHyperType t) -> m (UVar # t)
newVar =
\UTerm UVar ('AHyperType t)
x ->
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType) (t :: AHyperType).
Iso
(Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding forall (p :: * -> * -> *) s (m :: * -> *) a b.
(Strong p, MonadState s m) =>
Over p ((,) a) s s a b -> p a b -> m a
<<%= (forall s a. Snoc s s a a => s -> a -> s
Lens.|> UTerm UVar ('AHyperType t)
x)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (t :: AHyperType). Int -> UVar t
UVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length
, bindVar :: (UVar # t) -> UTerm UVar ('AHyperType t) -> m ()
bindVar =
\(UVar Int
h) ->
(forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType) (t :: AHyperType).
Iso
(Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
h forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.=)
}