{-# LANGUAGE UndecidableInstances, TemplateHaskell #-}
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 x. UVar t -> Rep (UVar t) x)
-> (forall x. Rep (UVar t) x -> UVar t) -> Generic (UVar t)
forall x. Rep (UVar t) x -> UVar t
forall x. UVar t -> Rep (UVar t) x
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
[UVar t] -> ShowS
UVar t -> String
(Int -> UVar t -> ShowS)
-> (UVar t -> String) -> ([UVar t] -> ShowS) -> Show (UVar t)
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
(UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool) -> Eq (UVar t)
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, Eq (UVar t)
Eq (UVar t)
-> (UVar t -> UVar t -> Ordering)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> UVar t)
-> (UVar t -> UVar t -> UVar t)
-> Ord (UVar t)
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
$cp1Ord :: forall (t :: AHyperType). Eq (UVar t)
Ord)
makePrisms ''UVar
newtype Binding t = Binding (Seq (UTerm UVar t))
deriving stock (forall x. Binding t -> Rep (Binding t) x)
-> (forall x. Rep (Binding t) x -> Binding t)
-> Generic (Binding t)
forall x. Rep (Binding t) x -> Binding t
forall x. Binding t -> Rep (Binding t) x
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 :: Binding t
emptyBinding = Seq (UTerm UVar t) -> Binding t
forall (t :: AHyperType). Seq (UTerm UVar t) -> Binding t
Binding Seq (UTerm UVar t)
forall a. Monoid a => a
mempty
{-# INLINE bindingDict #-}
bindingDict ::
MonadState s m =>
ALens' s (Binding # t) ->
BindingDict UVar m t
bindingDict :: ALens' s (Binding # t) -> BindingDict UVar m t
bindingDict ALens' s (Binding # t)
l =
BindingDict :: forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
((v # t) -> m (UTerm v # t))
-> ((UTerm v # t) -> m (v # t))
-> ((v # t) -> (UTerm v # t) -> m ())
-> BindingDict v m t
BindingDict
{ lookupVar :: (UVar # t) -> m (UTerm UVar # t)
lookupVar =
\(UVar Int
h) ->
Getting (Seq (UTerm UVar # t)) s (Seq (UTerm UVar # t))
-> m (Seq (UTerm UVar # t))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
Lens.use (ALens' s (Binding # t) -> Lens s s (Binding # t) (Binding # t)
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l (((Binding # t) -> Const (Seq (UTerm UVar # t)) (Binding # t))
-> s -> Const (Seq (UTerm UVar # t)) s)
-> ((Seq (UTerm UVar # t)
-> Const (Seq (UTerm UVar # t)) (Seq (UTerm UVar # t)))
-> (Binding # t) -> Const (Seq (UTerm UVar # t)) (Binding # t))
-> Getting (Seq (UTerm UVar # t)) s (Seq (UTerm UVar # t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t)
-> Const (Seq (UTerm UVar # t)) (Seq (UTerm UVar # t)))
-> (Binding # t) -> Const (Seq (UTerm UVar # t)) (Binding # t)
forall (t :: AHyperType) (t :: AHyperType).
Iso
(Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding)
m (Seq (UTerm UVar # t))
-> (Seq (UTerm UVar # t) -> UTerm UVar # t) -> m (UTerm UVar # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Seq (UTerm UVar # t)
-> Getting
(Endo (UTerm UVar # t)) (Seq (UTerm UVar # t)) (UTerm UVar # t)
-> UTerm UVar # t
forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! Index (Seq (UTerm UVar # t))
-> Traversal'
(Seq (UTerm UVar # t)) (IxValue (Seq (UTerm UVar # t)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
Index (Seq (UTerm UVar # t))
h)
, newVar :: (UTerm UVar # t) -> m (UVar # t)
newVar =
\UTerm UVar # t
x ->
ALens' s (Binding # t) -> Lens s s (Binding # t) (Binding # t)
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l (((Binding # t) -> (Seq (UTerm UVar # t), Binding # t))
-> s -> (Seq (UTerm UVar # t), s))
-> ((Seq (UTerm UVar # t)
-> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
-> (Binding # t) -> (Seq (UTerm UVar # t), Binding # t))
-> (Seq (UTerm UVar # t)
-> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
-> s
-> (Seq (UTerm UVar # t), s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t)
-> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
-> (Binding # t) -> (Seq (UTerm UVar # t), Binding # t)
forall (t :: AHyperType) (t :: AHyperType).
Iso
(Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding ((Seq (UTerm UVar # t)
-> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
-> s -> (Seq (UTerm UVar # t), s))
-> (Seq (UTerm UVar # t) -> Seq (UTerm UVar # t))
-> m (Seq (UTerm UVar # t))
forall (p :: * -> * -> *) s (m :: * -> *) a b.
(Strong p, MonadState s m) =>
Over p ((,) a) s s a b -> p a b -> m a
<<%= (Seq (UTerm UVar # t) -> (UTerm UVar # t) -> Seq (UTerm UVar # t)
forall s a. Snoc s s a a => s -> a -> s
Lens.|> UTerm UVar # t
x)
m (Seq (UTerm UVar # t)) -> (Seq (UTerm UVar # t) -> Int) -> m Int
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Seq (UTerm UVar # t) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length m Int -> (Int -> UVar # t) -> m (UVar # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Int -> UVar # t
forall (t :: AHyperType). Int -> UVar t
UVar
, bindVar :: (UVar # t) -> (UTerm UVar # t) -> m ()
bindVar =
\(UVar Int
h) UTerm UVar # t
v ->
ALens' s (Binding # t) -> Lens s s (Binding # t) (Binding # t)
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l (((Binding # t) -> Identity (Binding # t)) -> s -> Identity s)
-> (((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> (Binding # t) -> Identity (Binding # t))
-> ((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> s
-> Identity s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t) -> Identity (Seq (UTerm UVar # t)))
-> (Binding # t) -> Identity (Binding # t)
forall (t :: AHyperType) (t :: AHyperType).
Iso
(Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding ((Seq (UTerm UVar # t) -> Identity (Seq (UTerm UVar # t)))
-> (Binding # t) -> Identity (Binding # t))
-> (((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> Seq (UTerm UVar # t) -> Identity (Seq (UTerm UVar # t)))
-> ((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> (Binding # t)
-> Identity (Binding # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Seq (UTerm UVar # t))
-> Traversal'
(Seq (UTerm UVar # t)) (IxValue (Seq (UTerm UVar # t)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
Index (Seq (UTerm UVar # t))
h (((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> s -> Identity s)
-> (UTerm UVar # t) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= UTerm UVar # t
v
}