{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedStrings #-}

module Ty ( TyE
          , tyClosed
          , match
          -- * Substitutions
          , aT, rwArr
          ) where

import           A
import           Control.DeepSeq            (NFData)
import           Control.Exception          (Exception, throw)
import           Control.Monad              (zipWithM)
import           Control.Monad.Except       (liftEither, throwError)
import           Control.Monad.State.Strict (StateT (runStateT), gets, modify, state)
import           Data.Bifunctor             (first, second)
import           Data.Containers.ListUtils  (nubOrd)
import           Data.Foldable              (traverse_)
import           Data.Functor               (void, ($>))
import qualified Data.IntMap                as IM
import qualified Data.IntSet                as IS
import           Data.Maybe                 (catMaybes)
import qualified Data.Text                  as T
import           Data.Typeable              (Typeable)
import           GHC.Generics               (Generic)
import           Nm
import           Nm.IntMap
import           Prettyprinter              (Doc, Pretty (..), hardline, indent, squotes, (<+>))
import           Prettyprinter.Ext
import           Ty.Clone
import           U

data TySt a = TySt { forall a. TySt a -> Int
maxU      :: !Int
                   , forall a. TySt a -> IntMap (T ())
staEnv    :: IM.IntMap (T ())
                   , forall a. TySt a -> IntMap (T ())
polyEnv   :: IM.IntMap (T ())
                   , forall a. TySt a -> IntMap (C, a)
varConstr :: IM.IntMap (C, a)
                   }

data Subst a = Subst { forall a. Subst a -> IntMap (T a)
tySubst :: IM.IntMap (T a)
                     , forall a. Subst a -> IntMap (I a)
iSubst  :: IM.IntMap (I a) -- ^ Index variables
                     , forall a. Subst a -> IntMap (Sh a)
sSubst  :: IM.IntMap (Sh a) -- ^ Shape variables
                     } deriving ((forall a b. (a -> b) -> Subst a -> Subst b)
-> (forall a b. a -> Subst b -> Subst a) -> Functor Subst
forall a b. a -> Subst b -> Subst a
forall a b. (a -> b) -> Subst a -> Subst b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Subst a -> Subst b
fmap :: forall a b. (a -> b) -> Subst a -> Subst b
$c<$ :: forall a b. a -> Subst b -> Subst a
<$ :: forall a b. a -> Subst b -> Subst a
Functor)

data TyE a = IllScoped a (Nm a)
           | UF a (E a) (T a) (T a)
           | UI a (I a) (I a)
           | USh a (Sh a) (Sh a)
           | OT a (T a) (T a)
           | OSh a (Sh a) (Sh a)
           | OI a (I a) (I a)
           | ExistentialArg (T ())
           | MatchFailed (T ()) (T ())
           | MatchShFailed (Sh a) (Sh a)
           | MatchIFailed (I a) (I a)
           | Doesn'tSatisfy a (T a) C
           deriving ((forall x. TyE a -> Rep (TyE a) x)
-> (forall x. Rep (TyE a) x -> TyE a) -> Generic (TyE a)
forall x. Rep (TyE a) x -> TyE a
forall x. TyE a -> Rep (TyE a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (TyE a) x -> TyE a
forall a x. TyE a -> Rep (TyE a) x
$cfrom :: forall a x. TyE a -> Rep (TyE a) x
from :: forall x. TyE a -> Rep (TyE a) x
$cto :: forall a x. Rep (TyE a) x -> TyE a
to :: forall x. Rep (TyE a) x -> TyE a
Generic)

instance Semigroup (Subst a) where
    <> :: Subst a -> Subst a -> Subst a
(<>) (Subst IntMap (T a)
t IntMap (I a)
i IntMap (Sh a)
s) (Subst IntMap (T a)
t0 IntMap (I a)
i0 IntMap (Sh a)
s0) = IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (IntMap (T a)
tIntMap (T a) -> IntMap (T a) -> IntMap (T a)
forall a. Semigroup a => a -> a -> a
<>IntMap (T a)
t0) (IntMap (I a)
iIntMap (I a) -> IntMap (I a) -> IntMap (I a)
forall a. Semigroup a => a -> a -> a
<>IntMap (I a)
i0) (IntMap (Sh a)
sIntMap (Sh a) -> IntMap (Sh a) -> IntMap (Sh a)
forall a. Semigroup a => a -> a -> a
<>IntMap (Sh a)
s0)

instance Monoid (Subst a) where
    mempty :: Subst a
mempty = IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst IntMap (T a)
forall a. IntMap a
IM.empty IntMap (I a)
forall a. IntMap a
IM.empty IntMap (Sh a)
forall a. IntMap a
IM.empty
    mappend :: Subst a -> Subst a -> Subst a
mappend = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>)

instance NFData a => NFData (TyE a) where

instance Pretty a => Pretty (TyE a) where
    pretty :: forall ann. TyE a -> Doc ann
pretty (IllScoped a
l Nm a
n)         = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Nm a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Nm a -> Doc ann
pretty Nm a
n) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not in scope."
    pretty (UF a
l E a
e T a
ty T a
ty')         = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"could not unify" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T a -> Doc ann
pretty T a
ty) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"with" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T a -> Doc ann
pretty T a
ty') Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in expression" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (E a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. E a -> Doc ann
pretty E a
e)
    pretty (USh a
l Sh a
sh Sh a
sh')          = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"could not unify shape" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Sh a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh a -> Doc ann
pretty Sh a
sh) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"with" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Sh a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh a -> Doc ann
pretty Sh a
sh')
    pretty (UI a
l I a
ix I a
ix')           = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"could not unify index" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (I a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. I a -> Doc ann
pretty I a
ix) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"with" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (I a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. I a -> Doc ann
pretty I a
ix')
    pretty (OT a
l T a
ty T a
ty')           = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"occurs check failed when unifying" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T a -> Doc ann
pretty T a
ty) 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
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T a -> Doc ann
pretty T a
ty')
    pretty (OI a
l I a
i I a
j)              = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"occurs check failed when unifying indices" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (I a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. I a -> Doc ann
pretty I a
i) 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
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (I a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. I a -> Doc ann
pretty I a
j)
    pretty (OSh a
l Sh a
s0 Sh a
s1)           = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"occurs check failed when unifying shapes" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Sh a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh a -> Doc ann
pretty Sh a
s0) 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
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Sh a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh a -> Doc ann
pretty Sh a
s1)
    pretty (ExistentialArg T ()
ty)     = Doc ann
"Existential occurs as an argument in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T () -> Doc ann
pretty T ()
ty)
    pretty (MatchFailed T ()
t T ()
t')      = Doc ann
"Failed to match" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T () -> Doc ann
pretty T ()
t) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"against type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T () -> Doc ann
pretty T ()
t')
    pretty (MatchShFailed Sh a
sh Sh a
sh')  = Doc ann
"Failed to match" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Sh a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh a -> Doc ann
pretty Sh a
sh) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"against shape" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Sh a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh a -> Doc ann
pretty Sh a
sh')
    pretty (MatchIFailed I a
i I a
i')     = Doc ann
"Failed to match" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (I a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. I a -> Doc ann
pretty I a
i) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"against index" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (I a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. I a -> Doc ann
pretty I a
i')
    pretty (Doesn'tSatisfy a
l T a
ty C
c) = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T a -> Doc ann
pretty T a
ty) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not a member of class" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> C -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. C -> Doc ann
pretty C
c

instance (Pretty a) => Show (TyE a) where
    show :: TyE a -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> (TyE a -> Doc Any) -> TyE a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyE a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. TyE a -> Doc ann
pretty

instance (Pretty a, Typeable a) => Exception (TyE a) where

instance Pretty (Subst a) where
    pretty :: forall ann. Subst a -> Doc ann
pretty (Subst IntMap (T a)
ty IntMap (I a)
i IntMap (Sh a)
sh) =
        Doc ann
"type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<#*> IntMap (T a) -> Doc ann
forall b a. Pretty b => IntMap b -> Doc a
prettyDumpBinds IntMap (T a)
ty
            Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<#> Doc ann
"index:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<#*> IntMap (I a) -> Doc ann
forall b a. Pretty b => IntMap b -> Doc a
prettyDumpBinds IntMap (I a)
i
            Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<#> Doc ann
"shape:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<#*> IntMap (Sh a) -> Doc ann
forall b a. Pretty b => IntMap b -> Doc a
prettyDumpBinds IntMap (Sh a)
sh

instance Show (Subst a) where show :: Subst a -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> (Subst a -> Doc Any) -> Subst a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Subst a -> Doc ann
pretty

(<#*>) :: Doc a -> Doc a -> Doc a
<#*> :: forall ann. Doc ann -> Doc ann -> Doc ann
(<#*>) Doc a
x Doc a
y = Doc a
x Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
forall ann. Doc ann
hardline Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc a
y

type TyM a = StateT (TySt a) (Either (TyE a))
type UM a = StateT Int (Either (TyE a))

nI :: a -> UM b (I a)
nI :: forall a b. a -> UM b (I a)
nI a
l = (Int -> (I a, Int)) -> StateT Int (Either (TyE b)) (I a)
forall a. (Int -> (a, Int)) -> StateT Int (Either (TyE b)) a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state (\Int
i -> let j :: Int
j=Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 in (a -> Nm a -> I a
forall a. a -> Nm a -> I a
IEVar a
l (Text -> U -> a -> Nm a
forall a. Text -> U -> a -> Nm a
Nm Text
"m" (Int -> U
U Int
j) a
l), Int
j))

liftU :: UM a x -> TyM a x
liftU :: forall a x. UM a x -> TyM a x
liftU UM a x
a = do
    i <- (TySt a -> Int) -> StateT (TySt a) (Either (TyE a)) Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TySt a -> Int
forall a. TySt a -> Int
maxU
    (b, j) <- liftEither$runStateT a i
    modify (setMaxU j) $> b

mI :: Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI :: forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
_ i0 :: I a
i0@(Ix a
_ Int
i) i1 :: I a
i1@(Ix a
_ Int
j) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
                             | Bool
otherwise = TyE a -> Either (TyE a) (Subst a)
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (Subst a))
-> TyE a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ I a -> I a -> TyE a
forall a. I a -> I a -> TyE a
MatchIFailed I a
i0 I a
i1
mI Focus
_ (IVar a
_ (Nm Text
_ (U Int
i) a
_)) I a
ix = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right (Subst a -> Either (TyE a) (Subst a))
-> Subst a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst IntMap (T a)
forall a. IntMap a
IM.empty (Int -> I a -> IntMap (I a)
forall a. Int -> a -> IntMap a
IM.singleton Int
i I a
ix) IntMap (Sh a)
forall a. IntMap a
IM.empty
mI Focus
_ I a
ix (IVar a
_ (Nm Text
_ (U Int
i) a
_)) = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right (Subst a -> Either (TyE a) (Subst a))
-> Subst a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst IntMap (T a)
forall a. IntMap a
IM.empty (Int -> I a -> IntMap (I a)
forall a. Int -> a -> IntMap a
IM.singleton Int
i I a
ix) IntMap (Sh a)
forall a. IntMap a
IM.empty
mI Focus
_ (IEVar a
_ Nm a
n) (IEVar a
_ Nm a
n') | Nm a
n Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
n' = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
mI Focus
RF IEVar{} IEVar{} = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
-- TODO: Ix should match against ∃
mI Focus
_ i0 :: I a
i0@IEVar{} i1 :: I a
i1@IEVar{} = TyE a -> Either (TyE a) (Subst a)
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (Subst a))
-> TyE a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ I a -> I a -> TyE a
forall a. I a -> I a -> TyE a
MatchIFailed I a
i0 I a
i1
mI Focus
f (StaPlus a
_ I a
i (Ix a
_ Int
iϵ)) (Ix a
l Int
j) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
iϵ = Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
i (a -> Int -> I a
forall a. a -> Int -> I a
Ix a
l (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
iϵ))
mI Focus
f (Ix a
l Int
iϵ) (StaPlus a
_ I a
i (Ix a
_ Int
j)) | Int
iϵ Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
j = Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
i (a -> Int -> I a
forall a. a -> Int -> I a
Ix a
l (Int
iϵInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j))
mI Focus
f (StaPlus a
_ I a
i I a
j) (StaPlus a
_ I a
i' I a
j') = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
i I a
i' Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
j I a
j' -- FIXME: too stringent
mI Focus
f (StaMul a
_ I a
i I a
j) (StaMul a
_ I a
i' I a
j') = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
i I a
i' Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
j I a
j' -- FIXME: too stringent

mSh :: Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh :: forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
_ (SVar (Nm Text
_ (U Int
i) a
_)) Sh a
sh      = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right (Subst a -> Either (TyE a) (Subst a))
-> Subst a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst IntMap (T a)
forall a. IntMap a
IM.empty IntMap (I a)
forall a. IntMap a
IM.empty (Int -> Sh a -> IntMap (Sh a)
forall a. Int -> a -> IntMap a
IM.singleton Int
i Sh a
sh)
mSh Focus
_ Sh a
Nil Sh a
Nil                       = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
mSh Focus
f (Cons I a
i Sh a
sh) (Cons I a
i' Sh a
sh')     = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> I a -> I a -> Either (TyE a) (Subst a)
forall a. Focus -> I a -> I a -> Either (TyE a) (Subst a)
mI Focus
f I a
i I a
i' Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
f Sh a
sh Sh a
sh'
mSh Focus
f (Cat Sh a
sh0 Sh a
sh1) (Cat Sh a
sh0' Sh a
sh1') = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
f Sh a
sh0 Sh a
sh0' Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
f Sh a
sh1 Sh a
sh1'
mSh Focus
f (Rev Sh a
sh) (Rev Sh a
sh')            = Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
f Sh a
sh Sh a
sh'
mSh Focus
_ Sh a
sh Sh a
sh'                        = TyE a -> Either (TyE a) (Subst a)
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (Subst a))
-> TyE a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ Sh a -> Sh a -> TyE a
forall a. Sh a -> Sh a -> TyE a
MatchShFailed Sh a
sh Sh a
sh'

match :: (Typeable a, Pretty a) => T a -> T a -> Subst a
match :: forall a. (Typeable a, Pretty a) => T a -> T a -> Subst a
match T a
t T a
t' = (TyE a -> Subst a)
-> (Subst a -> Subst a) -> Either (TyE a) (Subst a) -> Subst a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TyE a -> Subst a
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw Subst a -> Subst a
forall a. a -> a
id (Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
LF T a
t T a
t')

maM :: Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM :: forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
_ T a
I T a
I                           = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
maM Focus
_ T a
F T a
F                           = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
maM Focus
_ T a
B T a
B                           = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
maM Focus
_ (TVar Nm a
n) (TVar Nm a
n') | Nm a
n Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
n'  = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
maM Focus
_ (TVar (Nm Text
_ (U Int
i) a
_)) T a
t     = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right (Subst a -> Either (TyE a) (Subst a))
-> Subst a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (Int -> T a -> IntMap (T a)
forall a. Int -> a -> IntMap a
IM.singleton Int
i T a
t) IntMap (I a)
forall a. IntMap a
IM.empty IntMap (Sh a)
forall a. IntMap a
IM.empty
maM Focus
_ (Arrow T a
t0 T a
t1) (Arrow T a
t0' T a
t1') = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
LF T a
t0 T a
t0' Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
RF T a
t1 T a
t1' -- FIXME: use <\> over <>
maM Focus
f (Arr Sh a
sh T a
t) (Arr Sh a
sh' T a
t')       = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
f Sh a
sh Sh a
sh' Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
f T a
t T a
t'
maM Focus
f (Arr Sh a
sh T a
t) T a
t'                 = Subst a -> Subst a -> Subst a
forall a. Semigroup a => a -> a -> a
(<>) (Subst a -> Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a -> Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Focus
f Sh a
sh Sh a
forall a. Sh a
Nil Either (TyE a) (Subst a -> Subst a)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall a b.
Either (TyE a) (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
f T a
t T a
t'
maM Focus
f (P [T a]
ts) (P [T a]
ts')                = [Subst a] -> Subst a
forall a. Monoid a => [a] -> a
mconcat ([Subst a] -> Subst a)
-> Either (TyE a) [Subst a] -> Either (TyE a) (Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (T a -> T a -> Either (TyE a) (Subst a))
-> [T a] -> [T a] -> Either (TyE a) [Subst a]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
f) [T a]
ts [T a]
ts'
maM Focus
_ (Ρ Nm a
n IntMap (T a)
_) (Ρ Nm a
n' IntMap (T a)
_) | Nm a
n Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
n'    = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
forall a. Monoid a => a
mempty
maM Focus
f (Ρ Nm a
n IntMap (T a)
rs) t :: T a
t@(Ρ Nm a
_ IntMap (T a)
rs') | IntMap (T a) -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet IntMap (T a)
rs' IntSet -> IntSet -> Bool
`IS.isSubsetOf` IntMap (T a) -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet IntMap (T a)
rs = (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
forall {a}. (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
mapTySubst (Nm a -> T a -> IntMap (T a) -> IntMap (T a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n T a
t) (Subst a -> Subst a)
-> ([Subst a] -> Subst a) -> [Subst a] -> Subst a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Subst a] -> Subst a
forall a. Monoid a => [a] -> a
mconcat ([Subst a] -> Subst a)
-> Either (TyE a) [Subst a] -> Either (TyE a) (Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((T a, T a) -> Either (TyE a) (Subst a))
-> [(T a, T a)] -> Either (TyE a) [Subst a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((T a -> T a -> Either (TyE a) (Subst a))
-> (T a, T a) -> Either (TyE a) (Subst a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
f)) (IntMap (T a, T a) -> [(T a, T a)]
forall a. IntMap a -> [a]
IM.elems ((T a -> T a -> (T a, T a))
-> IntMap (T a) -> IntMap (T a) -> IntMap (T a, T a)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IM.intersectionWith (,) IntMap (T a)
rs IntMap (T a)
rs'))
maM Focus
f (Ρ Nm a
n IntMap (T a)
rs) t :: T a
t@(P [T a]
ts) | [T a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T a]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= (Int, T a) -> Int
forall a b. (a, b) -> a
fst (IntMap (T a) -> (Int, T a)
forall a. IntMap a -> (Int, a)
IM.findMax IntMap (T a)
rs) = (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
forall {a}. (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
mapTySubst (Int -> T a -> IntMap (T a) -> IntMap (T a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (U -> Int
unU(U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$Nm a -> U
forall a. Nm a -> U
unique Nm a
n) T a
t) (Subst a -> Subst a)
-> ([Subst a] -> Subst a) -> [Subst a] -> Subst a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Subst a] -> Subst a
forall a. Monoid a => [a] -> a
mconcat ([Subst a] -> Subst a)
-> Either (TyE a) [Subst a] -> Either (TyE a) (Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((T a, T a) -> Either (TyE a) (Subst a))
-> [(T a, T a)] -> Either (TyE a) [Subst a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((T a -> T a -> Either (TyE a) (Subst a))
-> (T a, T a) -> Either (TyE a) (Subst a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Focus -> T a -> T a -> Either (TyE a) (Subst a)
forall a. Focus -> T a -> T a -> Either (TyE a) (Subst a)
maM Focus
f)) [ ([T a]
ts[T a] -> Int -> T a
forall a. (?callStack::CallStack) => [a] -> Int -> a
!!(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1),T a
tϵ) | (Int
i,T a
tϵ) <- IntMap (T a) -> [(Int, T a)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap (T a)
rs ]
maM Focus
_ T a
t T a
t'                          = TyE a -> Either (TyE a) (Subst a)
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (Subst a))
-> TyE a -> Either (TyE a) (Subst a)
forall a b. (a -> b) -> a -> b
$ T () -> T () -> TyE a
forall a. T () -> T () -> TyE a
MatchFailed (T a -> T ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void T a
t) (T a -> T ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void T a
t')

shSubst :: Subst a -> Sh a -> Sh a
shSubst :: forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
_ Sh a
Nil           = Sh a
forall a. Sh a
Nil
shSubst Subst a
s (Cons I a
i Sh a
sh)   = I a -> Sh a -> Sh a
forall a. I a -> Sh a -> Sh a
Cons (Subst a -> IntMap (I a)
forall a. Subst a -> IntMap (I a)
iSubst Subst a
s IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
i) (Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh)
shSubst Subst a
s (Cat Sh a
sh0 Sh a
sh1) = Sh a -> Sh a -> Sh a
forall a. Sh a -> Sh a -> Sh a
Cat (Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh0) (Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh1)
shSubst Subst a
s (Rev Sh a
sh)      = Sh a -> Sh a
forall a. Sh a -> Sh a
Rev (Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh)
shSubst Subst a
s (Π Sh a
sh)        = Sh a -> Sh a
forall a. Sh a -> Sh a
Π (Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh)
shSubst s :: Subst a
s@(Subst IntMap (T a)
ts IntMap (I a)
is IntMap (Sh a)
ss) sh' :: Sh a
sh'@(SVar (Nm Text
_ (U Int
u) a
_)) =
    case Int -> IntMap (Sh a) -> Maybe (Sh a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
u IntMap (Sh a)
ss of
        Just sh'' :: Sh a
sh''@SVar{} -> Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst (IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst IntMap (T a)
ts IntMap (I a)
is (Int -> IntMap (Sh a) -> IntMap (Sh a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
u IntMap (Sh a)
ss)) Sh a
sh''
        Just Sh a
sh          -> Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh
        Maybe (Sh a)
Nothing          -> Sh a
sh'

infixr 4 !>
(!>) :: IM.IntMap (I a) -> I a -> I a
!> :: forall a. IntMap (I a) -> I a -> I a
(!>) IntMap (I a)
ixes ix' :: I a
ix'@(IVar a
_ (Nm Text
_ (U Int
u) a
_)) =
    case Int -> IntMap (I a) -> Maybe (I a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
u IntMap (I a)
ixes of
        Just ix :: I a
ix@IVar{} -> Int -> IntMap (I a) -> IntMap (I a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
u IntMap (I a)
ixes IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
ix
        Just I a
ix        -> IntMap (I a)
ixes IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!>I a
ix
        Maybe (I a)
Nothing        -> I a
ix'
(!>) IntMap (I a)
ixes (StaPlus a
l I a
ix I a
ix') = a -> I a -> I a -> I a
forall a. a -> I a -> I a -> I a
StaPlus a
l (IntMap (I a)
ixes IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
ix) (IntMap (I a)
ixes IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
ix')
(!>) IntMap (I a)
ixes (StaMul a
l I a
ix I a
ix') = a -> I a -> I a -> I a
forall a. a -> I a -> I a -> I a
StaMul a
l (IntMap (I a)
ixes IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
ix) (IntMap (I a)
ixes IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
ix')
(!>) IntMap (I a)
_ ix :: I a
ix@Ix{} = I a
ix
(!>) IntMap (I a)
_ ix :: I a
ix@IEVar{} = I a
ix

aT :: Subst a -> T a -> T a
aT :: forall a. Subst a -> T a -> T a
aT Subst a
s (Arr Sh a
sh T a
ty) = Sh a -> T a -> T a
forall a. Sh a -> T a -> T a
Arr (Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh) (Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
ty)
aT Subst a
s (Arrow T a
t₁ T a
t₂) = T a -> T a -> T a
forall a. T a -> T a -> T a
Arrow (Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
t₁) (Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
t₂)
aT s :: Subst a
s@(Subst IntMap (T a)
ts IntMap (I a)
is IntMap (Sh a)
ss) ty' :: T a
ty'@(TVar Nm a
n) =
    let u :: Int
u = U -> Int
unU (U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$ Nm a -> U
forall a. Nm a -> U
unique Nm a
n in
    case Int -> IntMap (T a) -> Maybe (T a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
u IntMap (T a)
ts of
        Just ty :: T a
ty@TVar{} -> Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT (IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (Int -> IntMap (T a) -> IntMap (T a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
u IntMap (T a)
ts) IntMap (I a)
is IntMap (Sh a)
ss) T a
ty
        Just ty :: T a
ty@Ρ{}    -> Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT (IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (Int -> IntMap (T a) -> IntMap (T a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
u IntMap (T a)
ts) IntMap (I a)
is IntMap (Sh a)
ss) T a
ty
        Just T a
ty        -> Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
ty
        Maybe (T a)
Nothing        -> T a
ty'
aT Subst a
s (P [T a]
ts) = [T a] -> T a
forall a. [T a] -> T a
P (Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s (T a -> T a) -> [T a] -> [T a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [T a]
ts)
aT s :: Subst a
s@(Subst IntMap (T a)
ts IntMap (I a)
is IntMap (Sh a)
ss) (Ρ Nm a
n IntMap (T a)
rs) =
    let u :: Int
u = U -> Int
unU (Nm a -> U
forall a. Nm a -> U
unique Nm a
n) in
    case Int -> IntMap (T a) -> Maybe (T a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
u IntMap (T a)
ts of
        Just ty :: T a
ty@Ρ{}    -> Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT (IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (Int -> IntMap (T a) -> IntMap (T a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
u IntMap (T a)
ts) IntMap (I a)
is IntMap (Sh a)
ss) T a
ty
        Just ty :: T a
ty@TVar{} -> Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT (IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (Int -> IntMap (T a) -> IntMap (T a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
u IntMap (T a)
ts) IntMap (I a)
is IntMap (Sh a)
ss) T a
ty
        Just T a
ty        -> Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
ty
        Maybe (T a)
Nothing        -> Nm a -> IntMap (T a) -> T a
forall a. TyNm a -> IntMap (T a) -> T a
Ρ Nm a
n (Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s(T a -> T a) -> IntMap (T a) -> IntMap (T a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>IntMap (T a)
rs)
aT Subst a
_ T a
ty = T a
ty

runTyM :: Int -> TyM a b -> Either (TyE a) (b, Int)
runTyM :: forall a b. Int -> TyM a b -> Either (TyE a) (b, Int)
runTyM Int
i = ((b, TySt a) -> (b, Int))
-> Either (TyE a) (b, TySt a) -> Either (TyE a) (b, Int)
forall a b. (a -> b) -> Either (TyE a) a -> Either (TyE a) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TySt a -> Int) -> (b, TySt a) -> (b, Int)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second TySt a -> Int
forall a. TySt a -> Int
maxU) (Either (TyE a) (b, TySt a) -> Either (TyE a) (b, Int))
-> (TyM a b -> Either (TyE a) (b, TySt a))
-> TyM a b
-> Either (TyE a) (b, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyM a b -> TySt a -> Either (TyE a) (b, TySt a))
-> TySt a -> TyM a b -> Either (TyE a) (b, TySt a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip TyM a b -> TySt a -> Either (TyE a) (b, TySt a)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
forall a.
Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
TySt Int
i IntMap (T ())
forall a. IntMap a
IM.empty IntMap (T ())
forall a. IntMap a
IM.empty IntMap (C, a)
forall a. IntMap a
IM.empty)

mapMaxU :: (Int -> Int) -> TySt a -> TySt a
mapMaxU :: forall a. (Int -> Int) -> TySt a -> TySt a
mapMaxU Int -> Int
f (TySt Int
u IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs) = Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
forall a.
Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
TySt (Int -> Int
f Int
u) IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs

setMaxU :: Int -> TySt a -> TySt a
setMaxU :: forall a. Int -> TySt a -> TySt a
setMaxU Int
i (TySt Int
_ IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs) = Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
forall a.
Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
TySt Int
i IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs

addStaEnv :: Nm a -> T () -> TySt a -> TySt a
addStaEnv :: forall a. Nm a -> T () -> TySt a -> TySt a
addStaEnv Nm a
n T ()
t (TySt Int
u IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs) = Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
forall a.
Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
TySt Int
u (Nm a -> T () -> IntMap (T ()) -> IntMap (T ())
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n T ()
t IntMap (T ())
l) IntMap (T ())
v IntMap (C, a)
vcs

addPolyEnv :: Nm a -> T () -> TySt a -> TySt a
addPolyEnv :: forall a. Nm a -> T () -> TySt a -> TySt a
addPolyEnv Nm a
n T ()
t (TySt Int
u IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs) = Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
forall a.
Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
TySt Int
u IntMap (T ())
l (Nm a -> T () -> IntMap (T ()) -> IntMap (T ())
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n T ()
t IntMap (T ())
v) IntMap (C, a)
vcs

addVarConstrI :: Int -> a -> C -> TySt a -> TySt a
addVarConstrI :: forall a. Int -> a -> C -> TySt a -> TySt a
addVarConstrI Int
i a
ann C
c (TySt Int
u IntMap (T ())
l IntMap (T ())
v IntMap (C, a)
vcs) = Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
forall a.
Int -> IntMap (T ()) -> IntMap (T ()) -> IntMap (C, a) -> TySt a
TySt Int
u IntMap (T ())
l IntMap (T ())
v (Int -> (C, a) -> IntMap (C, a) -> IntMap (C, a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i (C
c, a
ann) IntMap (C, a)
vcs)

addVarConstr :: TyNm a -> a -> C -> TySt a -> TySt a
addVarConstr :: forall a. TyNm a -> a -> C -> TySt a -> TySt a
addVarConstr TyNm a
tn = Int -> a -> C -> TySt a -> TySt a
forall a. Int -> a -> C -> TySt a -> TySt a
addVarConstrI (U -> Int
unU(U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$TyNm a -> U
forall a. Nm a -> U
unique TyNm a
tn)

pushVarConstraint :: TyNm a -> a -> C -> TyM a ()
pushVarConstraint :: forall a. TyNm a -> a -> C -> TyM a ()
pushVarConstraint TyNm a
tn a
l C
c = (TySt a -> TySt a) -> StateT (TySt a) (Either (TyE a)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (TyNm a -> a -> C -> TySt a -> TySt a
forall a. TyNm a -> a -> C -> TySt a -> TySt a
addVarConstr TyNm a
tn a
l C
c)

freshN :: T.Text -> b -> TyM a (Nm b)
freshN :: forall b a. Text -> b -> TyM a (Nm b)
freshN Text
n b
l = do
    (TySt a -> TySt a) -> StateT (TySt a) (Either (TyE a)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Int -> Int) -> TySt a -> TySt a
forall a. (Int -> Int) -> TySt a -> TySt a
mapMaxU (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1))
    st <- (TySt a -> Int) -> StateT (TySt a) (Either (TyE a)) Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TySt a -> Int
forall a. TySt a -> Int
maxU
    pure $ Nm n (U st) l

ft :: T.Text -> b -> TyM a (T b)
ft :: forall b a. Text -> b -> TyM a (T b)
ft Text
n b
l = Nm b -> T b
forall a. TyNm a -> T a
TVar (Nm b -> T b)
-> StateT (TySt a) (Either (TyE a)) (Nm b)
-> StateT (TySt a) (Either (TyE a)) (T b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> b -> StateT (TySt a) (Either (TyE a)) (Nm b)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
n b
l

fsh :: T.Text -> TyM a (Sh ())
fsh :: forall a. Text -> TyM a (Sh ())
fsh Text
n = Nm () -> Sh ()
forall a. Nm a -> Sh a
SVar (Nm () -> Sh ())
-> StateT (TySt a) (Either (TyE a)) (Nm ())
-> StateT (TySt a) (Either (TyE a)) (Sh ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> StateT (TySt a) (Either (TyE a)) (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
n ()

fc :: T.Text -> a -> C -> TyM a (T ())
fc :: forall a. Text -> a -> C -> TyM a (T ())
fc Text
n a
l C
c = do
    n <- Text -> a -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
n a
l
    pushVarConstraint n l c $> TVar (void n)

ftv :: T.Text -> TyM a (T ())
ftv :: forall a. Text -> TyM a (T ())
ftv Text
n = Text -> () -> TyM a (T ())
forall b a. Text -> b -> TyM a (T b)
ft Text
n ()

fti :: T.Text -> TyM a (I ())
fti :: forall a. Text -> TyM a (I ())
fti Text
n = () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> StateT (TySt a) (Either (TyE a)) (Nm ())
-> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> StateT (TySt a) (Either (TyE a)) (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
n ()

ftie :: TyM a (I ())
ftie :: forall a. TyM a (I ())
ftie = () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IEVar () (Nm () -> I ())
-> StateT (TySt a) (Either (TyE a)) (Nm ())
-> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> StateT (TySt a) (Either (TyE a)) (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"n" ()

mapTySubst :: (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
mapTySubst IntMap (T a) -> IntMap (T a)
f (Subst IntMap (T a)
t IntMap (I a)
i IntMap (Sh a)
sh) = IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (IntMap (T a) -> IntMap (T a)
f IntMap (T a)
t) IntMap (I a)
i IntMap (Sh a)
sh
mapShSubst :: (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst IntMap (Sh a) -> IntMap (Sh a)
f (Subst IntMap (T a)
t IntMap (I a)
i IntMap (Sh a)
sh) = IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst IntMap (T a)
t IntMap (I a)
i (IntMap (Sh a) -> IntMap (Sh a)
f IntMap (Sh a)
sh)

data Focus = LF | RF

instance Pretty Focus where pretty :: forall ann. Focus -> Doc ann
pretty Focus
LF=Doc ann
"⦠"; pretty Focus
RF=Doc ann
"∢"

mguIPrep :: Focus -> IM.IntMap (I a) -> I a -> I a -> UM a (I a, IM.IntMap (I a))
mguIPrep :: forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
is I a
i0 I a
i1 =
    let i0' :: I a
i0' = IntMap (I a)
is IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
i0
        i1' :: I a
i1' = IntMap (I a)
is IntMap (I a) -> I a -> I a
forall a. IntMap (I a) -> I a -> I a
!> I a
i1
    in Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguI Focus
f IntMap (I a)
is (I a -> I a
forall a. I a -> I a
rwI I a
i0') (I a -> I a
forall a. I a -> I a
rwI I a
i1')

mguI :: Focus -> IM.IntMap (I a) -> I a -> I a -> UM a (I a, IM.IntMap (I a))
mguI :: forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguI Focus
_ IntMap (I a)
inp i0 :: I a
i0@(Ix a
_ Int
i) (Ix a
_ Int
j) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = (I a, IntMap (I a))
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I a
i0, IntMap (I a)
inp)
mguI Focus
RF IntMap (I a)
inp (Ix a
l Int
_) Ix{} = do {m <- a -> UM a (I a)
forall a b. a -> UM b (I a)
nI a
l; pure (m, inp)}
mguI Focus
_ IntMap (I a)
_ i0 :: I a
i0@(Ix a
l Int
_) i1 :: I a
i1@Ix{} = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1
mguI Focus
_ IntMap (I a)
inp i0 :: I a
i0@(IEVar a
_ Nm a
i) (IEVar a
_ Nm a
j) | Nm a
i Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
j = (I a, IntMap (I a))
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I a
i0, IntMap (I a)
inp)
mguI Focus
RF IntMap (I a)
inp (IEVar a
l Nm a
_) (IEVar a
_ Nm a
_) = do {m <- a -> UM a (I a)
forall a b. a -> UM b (I a)
nI a
l; pure (m, inp)}
mguI Focus
_ IntMap (I a)
_ i0 :: I a
i0@(IEVar a
l Nm a
_) i1 :: I a
i1@IEVar{} = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1
mguI Focus
_ IntMap (I a)
inp i0 :: I a
i0@(IVar a
_ Nm a
i) (IVar a
_ Nm a
j) | Nm a
i Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
j = (I a, IntMap (I a))
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I a
i0, IntMap (I a)
inp)
mguI Focus
_ IntMap (I a)
inp iix :: I a
iix@(IVar a
l (Nm Text
_ (U Int
i) a
_)) I a
ix | Int
i Int -> IntSet -> Bool
`IS.member` I a -> IntSet
forall a. I a -> IntSet
occI I a
ix = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
OI a
l I a
iix I a
ix
                                          | Bool
otherwise = (I a, IntMap (I a))
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I a
ix, Int -> I a -> IntMap (I a) -> IntMap (I a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i I a
ix IntMap (I a)
inp)
mguI Focus
_ IntMap (I a)
inp I a
ix iix :: I a
iix@(IVar a
l (Nm Text
_ (U Int
i) a
_)) | Int
i Int -> IntSet -> Bool
`IS.member` I a -> IntSet
forall a. I a -> IntSet
occI I a
ix = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
OI a
l I a
ix I a
iix
                                          | Bool
otherwise = (I a, IntMap (I a))
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I a
ix, Int -> I a -> IntMap (I a) -> IntMap (I a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i I a
ix IntMap (I a)
inp)
mguI Focus
f IntMap (I a)
inp (StaPlus a
_ I a
i0 (Ix a
_ Int
k0)) (StaPlus a
_ I a
i1 (Ix a
_ Int
k1)) | Int
k0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k1 = Focus
-> IntMap (I a)
-> I a
-> I a
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
inp I a
i0 I a
i1
mguI Focus
f IntMap (I a)
inp (StaMul a
_ I a
i0 (Ix a
_ Int
k0)) (StaMul a
_ I a
i1 (Ix a
_ Int
k1)) | Int
k0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k1 = Focus
-> IntMap (I a)
-> I a
-> I a
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
inp I a
i0 I a
i1
mguI Focus
f IntMap (I a)
inp i0 :: I a
i0@(StaPlus a
l I a
i (Ix a
_ Int
k)) i1 :: I a
i1@(Ix a
lk Int
j) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k = Focus
-> IntMap (I a)
-> I a
-> I a
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
inp I a
i (a -> Int -> I a
forall a. a -> Int -> I a
Ix a
lk (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
k))
                                                  | Bool
otherwise = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1
mguI Focus
f IntMap (I a)
inp i0 :: I a
i0@Ix{} i1 :: I a
i1@(StaPlus a
_ I a
_ Ix{}) = Focus
-> IntMap (I a)
-> I a
-> I a
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
inp I a
i1 I a
i0
mguI Focus
f IntMap (I a)
inp (StaPlus a
l I a
i0 I a
i1) (StaPlus a
_ I a
j0 I a
j1) = do
    -- FIXME: too stringent
    (k, s) <- Focus
-> IntMap (I a)
-> I a
-> I a
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
inp I a
i0 I a
j0
    (m, s') <- mguIPrep f s i1 j1
    pure (StaPlus l k m, s')
mguI Focus
f IntMap (I a)
inp (StaMul a
l I a
i0 I a
i1) (StaMul a
_ I a
j0 I a
j1) = do
    -- FIXME: too stringent
    (k, s) <- Focus
-> IntMap (I a)
-> I a
-> I a
-> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f IntMap (I a)
inp I a
i0 I a
j0
    (m, s') <- mguIPrep f s i1 j1
    pure (StaMul l k m, s')
mguI Focus
_ IntMap (I a)
_ i0 :: I a
i0@(IEVar a
l Nm a
_) i1 :: I a
i1@Ix{} = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1
mguI Focus
_ IntMap (I a)
_ i0 :: I a
i0@(Ix a
l Int
_) i1 :: I a
i1@IEVar{} = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1
mguI Focus
_ IntMap (I a)
_ i0 :: I a
i0@(IEVar a
l Nm a
_) i1 :: I a
i1@StaPlus{} = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1 -- TODO: focus case
mguI Focus
_ IntMap (I a)
_ i0 :: I a
i0@(StaPlus a
l I a
_ I a
_) i1 :: I a
i1@IEVar{} = TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a)))
-> TyE a -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a b. (a -> b) -> a -> b
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
UI a
l I a
i0 I a
i1
mguI Focus
_ IntMap (I a)
_ I a
i0 I a
i1 = String -> StateT Int (Either (TyE a)) (I a, IntMap (I a))
forall a. (?callStack::CallStack) => String -> a
error ((I a, I a) -> String
forall a. Show a => a -> String
show (I a
i0,I a
i1))

mgShPrep :: Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep :: forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep Focus
f a
l Subst a
s Sh a
sh0 Sh a
sh1 =
    let sh0' :: Sh a
sh0' = Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh0
        sh1' :: Sh a
sh1' = Subst a -> Sh a -> Sh a
forall a. Subst a -> Sh a -> Sh a
shSubst Subst a
s Sh a
sh1
    in Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgSh Focus
f a
l Subst a
s (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
sh0') (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
sh1')

mgSh :: Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgSh :: forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgSh Focus
_ a
_ Subst a
inp Sh a
Nil Sh a
Nil = (Sh a, Subst a) -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sh a
forall a. Sh a
Nil, Subst a
inp)
mgSh Focus
f a
l Subst a
inp (Cons I a
i Sh a
sh) (Cons I a
i' Sh a
sh') = do
    (i'', sI) <- Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f (Subst a -> IntMap (I a)
forall a. Subst a -> IntMap (I a)
iSubst Subst a
inp) I a
i I a
i'
    (sh'', s2) <- mgShPrep f l (inp { iSubst = sI }) sh sh'
    pure (Cons i'' sh'', s2)
mgSh Focus
_ a
_ Subst a
inp s :: Sh a
s@(SVar Nm a
sh) (SVar Nm a
sh') | Nm a
sh Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
sh' = (Sh a, Subst a) -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sh a
s, Subst a
inp)
mgSh Focus
_ a
l Subst a
inp s :: Sh a
s@(SVar (Nm Text
_ (U Int
i) a
_)) Sh a
sh | Int
i Int -> IntSet -> Bool
`IS.member` Sh a -> IntSet
forall a. Sh a -> IntSet
occSh Sh a
sh = TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a))
-> TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> Sh a -> Sh a -> TyE a
forall a. a -> Sh a -> Sh a -> TyE a
OSh a
l Sh a
s Sh a
sh
                                        | Bool
otherwise = (Sh a, Subst a) -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sh a
sh, (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Int -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i Sh a
sh) Subst a
inp)
mgSh Focus
_ a
l Subst a
inp Sh a
sh s :: Sh a
s@(SVar (Nm Text
_ (U Int
i) a
_)) | Int
i Int -> IntSet -> Bool
`IS.member` Sh a -> IntSet
forall a. Sh a -> IntSet
occSh Sh a
sh = TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a))
-> TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> Sh a -> Sh a -> TyE a
forall a. a -> Sh a -> Sh a -> TyE a
OSh a
l Sh a
sh Sh a
s
                                        | Bool
otherwise = (Sh a, Subst a) -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sh a
sh, (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Int -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i Sh a
sh) Subst a
inp)
mgSh Focus
_ a
l Subst a
_ sh :: Sh a
sh@Sh a
Nil sh' :: Sh a
sh'@Cons{} = TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a))
-> TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> Sh a -> Sh a -> TyE a
forall a. a -> Sh a -> Sh a -> TyE a
USh a
l Sh a
sh Sh a
sh'
mgSh Focus
_ a
l Subst a
_ sh :: Sh a
sh@Cons{} sh' :: Sh a
sh'@Nil{} = TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a))
-> TyE a -> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> Sh a -> Sh a -> TyE a
forall a. a -> Sh a -> Sh a -> TyE a
USh a
l Sh a
sh' Sh a
sh
mgSh Focus
f a
l Subst a
inp (Rev Sh a
sh) (Rev Sh a
sh') = Focus
-> a
-> Subst a
-> Sh a
-> Sh a
-> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep Focus
f a
l Subst a
inp Sh a
sh Sh a
sh'
mgSh Focus
f a
l Subst a
inp (Cat Sh a
sh0 Sh a
sh0') (Cat Sh a
sh1 Sh a
sh1') = do
    (sh', s) <- Focus
-> a
-> Subst a
-> Sh a
-> Sh a
-> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep Focus
f a
l Subst a
inp Sh a
sh0 Sh a
sh1
    (sh'', s') <- mgShPrep f l s sh0' sh1'
    pure (Cat sh' sh'', s')
mgSh Focus
f a
l Subst a
inp (Rev Sh a
sh) Sh a
sh' | ([I a]
is, Sh a
Nil) <- Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll Sh a
sh' = do
    Focus
-> a
-> Subst a
-> Sh a
-> Sh a
-> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep Focus
f a
l Subst a
inp Sh a
sh (Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
forall a. Sh a
Nil([I a] -> Sh a) -> [I a] -> Sh a
forall a b. (a -> b) -> a -> b
$[I a] -> [I a]
forall a. [a] -> [a]
reverse [I a]
is)
mgSh Focus
f a
l Subst a
inp Sh a
sh (Rev Sh a
sh') | ([I a]
is, Sh a
Nil) <- Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll Sh a
sh' = do
    Focus
-> a
-> Subst a
-> Sh a
-> Sh a
-> StateT Int (Either (TyE a)) (Sh a, Subst a)
forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep Focus
f a
l Subst a
inp (Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
forall a. Sh a
Nil([I a] -> Sh a) -> [I a] -> Sh a
forall a b. (a -> b) -> a -> b
$[I a] -> [I a]
forall a. [a] -> [a]
reverse [I a]
is) Sh a
sh

mguPrep :: Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep :: forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t0 T a
t1 =
    let t0' :: T a
t0' = Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
t0
        t1' :: T a
t1' = Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
t1
    in Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mgu Focus
f (a, E a)
l Subst a
s ({-# SCC "rwArr" #-} T a -> T a
forall a. T a -> T a
rwArr T a
t0') ({-# SCC "rwArr" #-} T a -> T a
forall a. T a -> T a
rwArr T a
t1')

mp :: (a, E a) -> Subst a -> T a -> T a -> UM a (Subst a)
mp :: forall a. (a, E a) -> Subst a -> T a -> T a -> UM a (Subst a)
mp (a, E a)
l Subst a
s T a
t0 T a
t1 = (T a, Subst a) -> Subst a
forall a b. (a, b) -> b
snd ((T a, Subst a) -> Subst a)
-> StateT Int (Either (TyE a)) (T a, Subst a)
-> StateT Int (Either (TyE a)) (Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus
-> (a, E a)
-> Subst a
-> T a
-> T a
-> StateT Int (Either (TyE a)) (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
LF (a, E a)
l Subst a
s T a
t0 T a
t1

occSh :: Sh a -> IS.IntSet
occSh :: forall a. Sh a -> IntSet
occSh (SVar (Nm Text
_ (U Int
i) a
_)) = Int -> IntSet
IS.singleton Int
i
occSh (Cat Sh a
sh0 Sh a
sh1)         = Sh a -> IntSet
forall a. Sh a -> IntSet
occSh Sh a
sh0 IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> Sh a -> IntSet
forall a. Sh a -> IntSet
occSh Sh a
sh1
occSh (I a
_ `Cons` Sh a
sh)         = Sh a -> IntSet
forall a. Sh a -> IntSet
occSh Sh a
sh
occSh Nil{}                 = IntSet
IS.empty

occI :: I a -> IS.IntSet
occI :: forall a. I a -> IntSet
occI Ix{}                    = IntSet
IS.empty
occI (IVar a
_ (Nm Text
_ (U Int
i) a
_)) = Int -> IntSet
IS.singleton Int
i
occI (StaPlus a
_ I a
i I a
j)         = I a -> IntSet
forall a. I a -> IntSet
occI I a
i IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> I a -> IntSet
forall a. I a -> IntSet
occI I a
j
occI (StaMul a
_ I a
i I a
j)          = I a -> IntSet
forall a. I a -> IntSet
occI I a
i IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> I a -> IntSet
forall a. I a -> IntSet
occI I a
j
occI IEVar{}                 = IntSet
IS.empty

occ :: T a -> IS.IntSet
occ :: forall a. T a -> IntSet
occ (TVar (Nm Text
_ (U Int
i) a
_)) = Int -> IntSet
IS.singleton Int
i
occ (Arrow T a
t T a
t')          = T a -> IntSet
forall a. T a -> IntSet
occ T a
t IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> T a -> IntSet
forall a. T a -> IntSet
occ T a
t'
occ (Arr Sh a
_ T a
a)             = T a -> IntSet
forall a. T a -> IntSet
occ T a
a -- shouldn't need shape?
occ T a
I                     = IntSet
IS.empty
occ T a
F                     = IntSet
IS.empty
occ T a
B                     = IntSet
IS.empty
occ Li{}                  = IntSet
IS.empty
occ (P [T a]
ts)                = (T a -> IntSet) -> [T a] -> IntSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap T a -> IntSet
forall a. T a -> IntSet
occ [T a]
ts
occ (Ρ (Nm Text
_ (U Int
i) a
_) IntMap (T a)
rs) = Int -> IntSet -> IntSet
IS.insert Int
i (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ (T a -> IntSet) -> IntMap (T a) -> IntSet
forall m a. Monoid m => (a -> m) -> IntMap a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap T a -> IntSet
forall a. T a -> IntSet
occ IntMap (T a)
rs

mgu :: Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mgu :: forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mgu Focus
f (a, E a)
l Subst a
s (Arrow T a
t0 T a
t1) (Arrow T a
t0' T a
t1') = do
    (t0'', s0) <- Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
LF (a, E a)
l Subst a
s T a
t0 T a
t0'
    (t1'', s1) <- mguPrep f l s0 t1 t1'
    pure (Arrow t0'' t1'', s1)
mgu Focus
_ (a, E a)
_ Subst a
s T a
I T a
I = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
forall a. T a
I, Subst a
s)
mgu Focus
_ (a, E a)
_ Subst a
s T a
F T a
F = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
forall a. T a
F, Subst a
s)
mgu Focus
_ (a, E a)
_ Subst a
s T a
B T a
B = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
forall a. T a
B, Subst a
s)
mgu Focus
_ (a, E a)
_ Subst a
s t :: T a
t@Li{} T a
I = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
t, Subst a
s)
mgu Focus
_ (a, E a)
_ Subst a
s T a
I t :: T a
t@Li{} = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
t, Subst a
s)
mgu Focus
f (a, E a)
_ Subst a
s (Li I a
i0) (Li I a
i1) = do {(i', iS) <- Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
forall a.
Focus -> IntMap (I a) -> I a -> I a -> UM a (I a, IntMap (I a))
mguIPrep Focus
f (Subst a -> IntMap (I a)
forall a. Subst a -> IntMap (I a)
iSubst Subst a
s) I a
i0 I a
i1; pure (Li i', Subst mempty iS mempty <> s)}
mgu Focus
_ (a, E a)
_ Subst a
s t :: T a
t@(TVar Nm a
n) (TVar Nm a
n') | Nm a
n Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
n' = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
t, Subst a
s)
mgu Focus
_ (a
l, E a
_) Subst a
s t' :: T a
t'@(TVar (Nm Text
_ (U Int
i) a
_)) T a
t | Int
i Int -> IntSet -> Bool
`IS.member` T a -> IntSet
forall a. T a -> IntSet
occ T a
t = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> T a -> T a -> TyE a
forall a. a -> T a -> T a -> TyE a
OT a
l T a
t' T a
t
                                          | Bool
otherwise = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
t, (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
forall {a}. (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
mapTySubst (Int -> T a -> IntMap (T a) -> IntMap (T a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i T a
t) Subst a
s)
mgu Focus
_ (a
l, E a
_) Subst a
s T a
t t' :: T a
t'@(TVar (Nm Text
_ (U Int
i) a
_)) | Int
i Int -> IntSet -> Bool
`IS.member` T a -> IntSet
forall a. T a -> IntSet
occ T a
t = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> T a -> T a -> TyE a
forall a. a -> T a -> T a -> TyE a
OT a
l T a
t' T a
t
                                          | Bool
otherwise = (T a, Subst a) -> UM a (T a, Subst a)
forall a. a -> StateT Int (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T a
t, (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
forall {a}. (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
mapTySubst (Int -> T a -> IntMap (T a) -> IntMap (T a)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i T a
t) Subst a
s)
mgu Focus
_ (a
l, E a
e) Subst a
_ t0 :: T a
t0@Arrow{} T a
t1 = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t0 T a
t1
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
t0 t1 :: T a
t1@Arrow{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t0 T a
t1
mgu Focus
f (a, E a)
l Subst a
s (Arr Sh a
sh T a
t) (Arr Sh a
sh' T a
t') = do
    (t'', s0) <- Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t T a
t'
    (sh'', s1) <- mgShPrep f (fst l) s0 sh sh'
    pure (Arr sh'' t'', s1)
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
F T a
I = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
F T a
forall a. T a
I
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
I T a
F = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
I T a
forall a. T a
F
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
F t :: T a
t@Li{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
F T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Li{} T a
F = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
F
mgu Focus
f (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) T a
F = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t T a
forall a. T a
F
mgu Focus
f (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) T a
I = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t T a
forall a. T a
I
mgu Focus
f (a, E a)
l Subst a
s T a
F (Arr (SVar Nm a
n) T a
t) = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
forall a. T a
F T a
t
mgu Focus
f (a, E a)
l Subst a
s T a
I (Arr (SVar Nm a
n) T a
t) = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
forall a. T a
I T a
t
mgu Focus
f (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) T a
B = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t T a
forall a. T a
B
mgu Focus
f (a, E a)
l Subst a
s T a
B (Arr (SVar Nm a
n) T a
t) = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
forall a. T a
B T a
t
mgu Focus
f (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) t' :: T a
t'@P{} = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t T a
t'
mgu Focus
f (a, E a)
l Subst a
s t' :: T a
t'@P{} (Arr (SVar Nm a
n) T a
t) = (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
forall {a}. (IntMap (Sh a) -> IntMap (Sh a)) -> Subst a -> Subst a
mapShSubst (Nm a -> Sh a -> IntMap (Sh a) -> IntMap (Sh a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n Sh a
forall a. Sh a
Nil)) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
s T a
t' T a
t
mgu Focus
f (a, E a)
l Subst a
s (P [T a]
ts) (P [T a]
ts') | [T a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T a]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [T a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T a]
ts' = ([T a] -> T a) -> ([T a], Subst a) -> (T a, Subst a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [T a] -> T a
forall a. [T a] -> T a
P (([T a], Subst a) -> (T a, Subst a))
-> StateT Int (Either (TyE a)) ([T a], Subst a)
-> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Subst a -> T a -> T a -> UM a (T a, Subst a))
-> Subst a
-> [T a]
-> [T a]
-> StateT Int (Either (TyE a)) ([T a], Subst a)
forall {f :: * -> *} {t} {t} {t} {a}.
Monad f =>
(t -> t -> t -> f (a, t)) -> t -> [t] -> [t] -> f ([a], t)
zSt (Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l) Subst a
s [T a]
ts [T a]
ts'
-- TODO: rho occurs check
mgu Focus
f l :: (a, E a)
l@(a
lϵ, E a
e) Subst a
s t :: T a
t@(Ρ Nm a
n IntMap (T a)
rs) t' :: T a
t'@(P [T a]
ts) | [T a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T a]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= (Int, T a) -> Int
forall a b. (a, b) -> a
fst (IntMap (T a) -> (Int, T a)
forall a. IntMap a -> (Int, a)
IM.findMax IntMap (T a)
rs) Bool -> Bool -> Bool
&& (Int, T a) -> Int
forall a b. (a, b) -> a
fst (IntMap (T a) -> (Int, T a)
forall a. IntMap a -> (Int, a)
IM.findMin IntMap (T a)
rs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = ([T a] -> T a) -> ([T a], Subst a) -> (T a, Subst a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [T a] -> T a
forall a. [T a] -> T a
P (([T a], Subst a) -> (T a, Subst a))
-> StateT Int (Either (TyE a)) ([T a], Subst a)
-> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Subst a -> (Int, T a) -> UM a (T a, Subst a))
-> Subst a
-> [(Int, T a)]
-> StateT Int (Either (TyE a)) ([T a], Subst a)
forall (m :: * -> *) a b x.
Monad m =>
(Subst a -> b -> m (x, Subst a))
-> Subst a -> [b] -> m ([x], Subst a)
tS (\Subst a
sϵ (Int
i, T a
tϵ) -> (Subst a -> Subst a) -> (T a, Subst a) -> (T a, Subst a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
forall {a}. (IntMap (T a) -> IntMap (T a)) -> Subst a -> Subst a
mapTySubst (Nm a -> T a -> IntMap (T a) -> IntMap (T a)
forall a b. Nm a -> b -> IntMap b -> IntMap b
insert Nm a
n T a
t')) ((T a, Subst a) -> (T a, Subst a))
-> UM a (T a, Subst a) -> UM a (T a, Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
f (a, E a)
l Subst a
sϵ ([T a]
ts[T a] -> Int -> T a
forall a. (?callStack::CallStack) => [a] -> Int -> a
!!(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) T a
tϵ) Subst a
s (IntMap (T a) -> [(Int, T a)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap (T a)
rs)
                                       | Bool
otherwise = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
lϵ E a
e T a
t T a
t'
mgu Focus
f (a, E a)
l Subst a
s t :: T a
t@P{} t' :: T a
t'@Ρ{} = Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mgu Focus
f (a, E a)
l Subst a
s T a
t' T a
t
mgu Focus
f (a, E a)
l Subst a
s (Ρ Nm a
n IntMap (T a)
rs) (Ρ Nm a
n' IntMap (T a)
rs') = do
    (_, rss) <- (Subst a -> (T a, T a) -> UM a (T a, Subst a))
-> Subst a
-> [(T a, T a)]
-> StateT Int (Either (TyE a)) ([T a], Subst a)
forall (m :: * -> *) a b x.
Monad m =>
(Subst a -> b -> m (x, Subst a))
-> Subst a -> [b] -> m ([x], Subst a)
tS (\Subst a
sϵ (T a
t0,T a
t1) -> Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
forall a.
Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)
mguPrep Focus
LF (a, E a)
l Subst a
sϵ T a
t0 T a
t1) Subst a
s ([(T a, T a)] -> StateT Int (Either (TyE a)) ([T a], Subst a))
-> [(T a, T a)] -> StateT Int (Either (TyE a)) ([T a], Subst a)
forall a b. (a -> b) -> a -> b
$ IntMap (T a, T a) -> [(T a, T a)]
forall a. IntMap a -> [a]
IM.elems (IntMap (T a, T a) -> [(T a, T a)])
-> IntMap (T a, T a) -> [(T a, T a)]
forall a b. (a -> b) -> a -> b
$ (T a -> T a -> (T a, T a))
-> IntMap (T a) -> IntMap (T a) -> IntMap (T a, T a)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IM.intersectionWith (,) IntMap (T a)
rs IntMap (T a)
rs'
    let t=Nm a -> IntMap (T a) -> T a
forall a. TyNm a -> IntMap (T a) -> T a
Ρ Nm a
n' (IntMap (T a)
rsIntMap (T a) -> IntMap (T a) -> IntMap (T a)
forall a. Semigroup a => a -> a -> a
<>IntMap (T a)
rs') in pure (t, mapTySubst (insert n t) rss)
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
F t :: T a
t@Arr{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
F T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} T a
F = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
F
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
B t :: T a
t@Arr{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
B T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} T a
B = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
B
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
I t :: T a
t@Arr{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
I T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} T a
I = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
I
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Li{} t' :: T a
t'@Arr{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
t'
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} t' :: T a
t'@Li{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
t'
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
F t :: T a
t@P{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
F T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@P{} T a
F = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
F
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
I t :: T a
t@P{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
I T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@P{} T a
I = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
I
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
B t :: T a
t@P{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
B T a
t
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@P{} T a
B = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
B
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@P{} t' :: T a
t'@Arr{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
t'
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} t' :: T a
t'@P{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
t'
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
I T a
B= TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
I T a
forall a. T a
B
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
B T a
I = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
B T a
forall a. T a
I
mgu Focus
_ (a
l, E a
e) Subst a
_ t :: T a
t@Li{} T a
B = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
t T a
forall a. T a
B
mgu Focus
_ (a
l, E a
e) Subst a
_ T a
B t :: T a
t@Li{} = TyE a -> UM a (T a, Subst a)
forall a. TyE a -> StateT Int (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> UM a (T a, Subst a)) -> TyE a -> UM a (T a, Subst a)
forall a b. (a -> b) -> a -> b
$ a -> E a -> T a -> T a -> TyE a
forall a. a -> E a -> T a -> T a -> TyE a
UF a
l E a
e T a
forall a. T a
B T a
t

zSt :: (t -> t -> t -> f (a, t)) -> t -> [t] -> [t] -> f ([a], t)
zSt t -> t -> t -> f (a, t)
_ t
s [] [t]
_           = ([a], t) -> f ([a], t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], t
s)
zSt t -> t -> t -> f (a, t)
_ t
s [t]
_ []           = ([a], t) -> f ([a], t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], t
s)
zSt t -> t -> t -> f (a, t)
op t
s (t
x:[t]
xs) (t
y:[t]
ys) = do{(t, next) <- t -> t -> t -> f (a, t)
op t
s t
x t
y; first (t:) <$> zSt op next xs ys}

zS :: (t -> t -> t -> f t) -> t -> [t] -> [t] -> f t
zS t -> t -> t -> f t
_ t
s [] [t]
_           = t -> f t
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
s
zS t -> t -> t -> f t
_ t
s [t]
_ []           = t -> f t
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
s
zS t -> t -> t -> f t
op t
s (t
x:[t]
xs) (t
y:[t]
ys) = do {next <- t -> t -> t -> f t
op t
s t
x t
y; zS op next xs ys}

tS :: Monad m => (Subst a -> b -> m (x, Subst a)) -> Subst a -> [b] -> m ([x], Subst a)
tS :: forall (m :: * -> *) a b x.
Monad m =>
(Subst a -> b -> m (x, Subst a))
-> Subst a -> [b] -> m ([x], Subst a)
tS Subst a -> b -> m (x, Subst a)
_ Subst a
s []     = ([x], Subst a) -> m ([x], Subst a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Subst a
s)
tS Subst a -> b -> m (x, Subst a)
f Subst a
s (b
t:[b]
ts) = do{(tϵ, next) <- Subst a -> b -> m (x, Subst a)
f Subst a
s b
t; first (tϵ:) <$> tS f next ts}

vx :: I a -> Sh a
vx = (I a -> Sh a -> Sh a
forall a. I a -> Sh a -> Sh a
`Cons` Sh a
forall a. Sh a
Nil)
vV :: I a -> T a -> T a
vV I a
i = Sh a -> T a -> T a
forall a. Sh a -> T a -> T a
Arr (I a -> Sh a
forall {a}. I a -> Sh a
vx I a
i)

tyNumBinOp :: a -> TyM a (T (), Subst a)
tyNumBinOp :: forall a. a -> TyM a (T (), Subst a)
tyNumBinOp a
l = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    pure (n ~> n ~> n, mempty)

mm :: a -> TyM a (T (), Subst a)
mm :: forall a. a -> TyM a (T (), Subst a)
mm a
l = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"o" a
l C
IsOrd
    pure (n ~> n ~> n, mempty)

tyBoo :: a -> TyM a (T (), Subst a)
tyBoo :: forall a. a -> TyM a (T (), Subst a)
tyBoo a
l = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"b" a
l C
HasBits
    pure (n ~> n ~> n, mempty)

tyOrdBinRel :: a -> TyM a (T (), Subst a)
tyOrdBinRel :: forall a. a -> TyM a (T (), Subst a)
tyOrdBinRel a
l = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"o" a
l C
IsOrd
    pure (n ~> n ~> B, mempty)

tyEqBinRel :: a -> TyM a (T (), Subst a)
tyEqBinRel :: forall a. a -> TyM a (T (), Subst a)
tyEqBinRel a
l = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"e" a
l C
IsEq
    pure (n ~> n ~> B, mempty)

sel :: [Int] -> Sh a -> Sh a
sel :: forall a. [Int] -> Sh a -> Sh a
sel [Int]
axes Sh a
sh = Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
forall a. Sh a
Nil (((Int, I a) -> I a) -> [(Int, I a)] -> [I a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, I a) -> I a
forall a b. (a, b) -> b
snd (((Int, I a) -> Bool) -> [(Int, I a)] -> [(Int, I a)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
axes) (Int -> Bool) -> ((Int, I a) -> Int) -> (Int, I a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, I a) -> Int
forall a b. (a, b) -> a
fst) ([Int] -> [I a] -> [(Int, I a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [I a]
unrolled))) where
    ([I a]
unrolled, Sh a
_) = Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll Sh a
sh

tydrop :: Int -> Sh a -> Sh a
tydrop :: forall a. Int -> Sh a -> Sh a
tydrop Int
0 Sh a
sh            = Sh a
sh
tydrop Int
_ (I a
_ `Cons` Sh a
sh) = Sh a
sh

del :: [Int] -> Sh a -> Sh a
del :: forall a. [Int] -> Sh a -> Sh a
del [Int]
axes Sh a
sh = Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
t (((Int, I a) -> I a) -> [(Int, I a)] -> [I a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, I a) -> I a
forall a b. (a, b) -> b
snd (((Int, I a) -> Bool) -> [(Int, I a)] -> [(Int, I a)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
axes) (Int -> Bool) -> ((Int, I a) -> Int) -> (Int, I a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, I a) -> Int
forall a b. (a, b) -> a
fst) ([Int] -> [I a] -> [(Int, I a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [I a]
unrolled))) where
    ([I a]
unrolled, Sh a
t) = Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll Sh a
sh

trim :: Sh a -> Sh a
trim :: forall a. Sh a -> Sh a
trim = Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
forall a. Sh a
Nil ([I a] -> Sh a) -> (Sh a -> [I a]) -> Sh a -> Sh a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([I a], Sh a) -> [I a]
forall a b. (a, b) -> a
fst (([I a], Sh a) -> [I a])
-> (Sh a -> ([I a], Sh a)) -> Sh a -> [I a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll

iunroll :: Sh a -> Maybe (I a)
iunroll (Cons I a
i Sh a
Nil) = I a -> Maybe (I a)
forall a. a -> Maybe a
Just I a
i
iunroll (Cons I a
i Sh a
shϵ) = a -> I a -> I a -> I a
forall a. a -> I a -> I a -> I a
StaMul (I a -> a
forall a. I a -> a
ia I a
i) I a
i (I a -> I a) -> Maybe (I a) -> Maybe (I a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sh a -> Maybe (I a)
iunroll Sh a
shϵ
iunroll Sh a
_            = Maybe (I a)
forall a. Maybe a
Nothing

unroll :: Sh a -> ([I a], Sh a)
unroll (Cons I a
i Sh a
shϵ) = ([I a] -> [I a]) -> ([I a], Sh a) -> ([I a], Sh a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (I a
i I a -> [I a] -> [I a]
forall a. a -> [a] -> [a]
:) (([I a], Sh a) -> ([I a], Sh a)) -> ([I a], Sh a) -> ([I a], Sh a)
forall a b. (a -> b) -> a -> b
$ Sh a -> ([I a], Sh a)
unroll Sh a
shϵ
unroll Sh a
s            = ([], Sh a
s)

roll :: Sh a -> [I a] -> Sh a
roll :: forall a. Sh a -> [I a] -> Sh a
roll = (I a -> Sh a -> Sh a) -> Sh a -> [I a] -> Sh a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr I a -> Sh a -> Sh a
forall a. I a -> Sh a -> Sh a
Cons

tyB :: a -> Builtin -> TyM a (T (), Subst a)
tyB :: forall a. a -> Builtin -> TyM a (T (), Subst a)
tyB a
_ Builtin
Floor = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I, Subst a
forall a. Monoid a => a
mempty); tyB a
_ Builtin
ItoF = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Even = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
B, Subst a
forall a. Monoid a => a
mempty); tyB a
_ Builtin
Odd = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
B, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Sr = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I, Subst a
forall a. Monoid a => a
mempty); tyB a
_ Builtin
Sl = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I, Subst a
forall a. Monoid a => a
mempty)
tyB a
l Builtin
R = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum; sh <- fsh "sh"
    pure (n ~> n ~> Arr sh n, mempty)
tyB a
_ Builtin
Iter = do{a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; let s = T () -> T () -> T ()
forall a. T a -> T a -> T a
Arrow T ()
a T ()
a in pure (s ~> I ~> s, mempty)}
tyB a
_ Builtin
ConsE = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"
    pure (a ~> vV i a ~> vV (StaPlus () i (Ix()1)) a, mempty)
tyB a
l Builtin
Snoc = a -> Builtin -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> Builtin -> TyM a (T (), Subst a)
tyB a
l Builtin
ConsE
tyB a
_ Builtin
A1 = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (i `Cons` sh) a ~> I ~> Arr sh a, mempty)
tyB a
_ Builtin
IOf = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"
    pure ((a ~> B) ~> vV i a ~> I, mempty)
tyB a
_ Builtin
Di = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"
    pure (Arr (i `Cons` i `Cons` Nil) a ~> vV i a, mempty)
tyB a
_ Builtin
LastM = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (i `Cons` sh) a ~> Arr sh a, mempty)
tyB a
_ Builtin
Last = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (StaPlus () i (Ix()1) `Cons` sh) a ~> Arr sh a, mempty)
tyB a
_ Builtin
Head = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (StaPlus () i (Ix()1) `Cons` sh) a ~> Arr sh a, mempty)
tyB a
_ Builtin
Init = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (StaPlus () i (Ix()1) `Cons` sh) a ~> Arr (i `Cons` sh) a, mempty)
tyB a
_ Builtin
InitM = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; n <- ftie; sh <- fsh "sh"
    pure (Arr (i `Cons` sh) a ~> Arr (n `Cons` sh) a, mempty)
tyB a
_ Builtin
Tail = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (StaPlus () i (Ix()1) `Cons` sh) a ~> Arr (i `Cons` sh) a, mempty)
tyB a
_ Builtin
TailM = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; n <- ftie; sh <- fsh "sh"
    pure (Arr (i `Cons` sh) a ~> Arr (n `Cons` sh) a, mempty)
tyB a
_ Builtin
Rot = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (I ~> Arr (i `Cons` sh) a ~> Arr (i `Cons` sh) a, mempty)
tyB a
_ Builtin
Cyc = do
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"; a <- ftv "a"; i <- fti "i"; n <- ftie
    pure (Arr (i `Cons` sh) a ~> I ~> Arr (n `Cons` sh) a, mempty)
tyB a
_ Builtin
HeadM = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    pure (Arr (i `Cons` sh) a ~> Arr sh a, mempty)
tyB a
_ Builtin
Re = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; n <- ftie
    pure (I ~> a ~> Arr (n `Cons` Nil) a, mempty)
tyB a
_ Builtin
FRange = do {n <- TyM a (I ())
forall a. TyM a (I ())
ftie; pure (F ~> F ~> I ~> Arr (n `Cons` Nil) F, mempty)}
tyB a
_ Builtin
Fib = do
    n <- TyM a (I ())
forall a. TyM a (I ())
ftie; a <- ftv "a"
    let arrTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I ()
n I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
forall a. Sh a
Nil) T ()
a
    pure (a ~> a ~> (a ~> a ~> a) ~> I ~> arrTy, mempty)
tyB a
_ Builtin
IRange = do {n <- TyM a (I ())
forall a. TyM a (I ())
ftie; pure (I ~> I ~> I ~> Arr (n `Cons` Nil) I, mempty)}
tyB a
l Builtin
Plus = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyNumBinOp a
l; tyB a
l Builtin
Minus = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyNumBinOp a
l
tyB a
l Builtin
Times = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyNumBinOp a
l
tyB a
l Builtin
Gte = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyOrdBinRel a
l; tyB a
l Builtin
Gt = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyOrdBinRel a
l; tyB a
l Builtin
Lt = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyOrdBinRel a
l
tyB a
l Builtin
Lte = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyOrdBinRel a
l; tyB a
l Builtin
Eq = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyEqBinRel a
l; tyB a
l Builtin
Neq = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyEqBinRel a
l
tyB a
l Builtin
And = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyBoo a
l; tyB a
l Builtin
Or = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyBoo a
l; tyB a
l Builtin
Xor = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
tyBoo a
l
tyB a
l Builtin
N = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"b" a
l C
HasBits
    pure (n ~> n, mempty)
tyB a
_ Builtin
Exp = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
l Builtin
Min = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
mm a
l; tyB a
l Builtin
Max = a -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> TyM a (T (), Subst a)
mm a
l
tyB a
l Builtin
IntExp = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    pure (n ~> I ~> n, mempty)
tyB a
l Builtin
Neg = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    pure (n ~> n, mempty)
tyB a
l Builtin
Abs = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    pure (n ~> n, mempty)
tyB a
_ Builtin
Sqrt = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Log = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Div = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Mod = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
IDiv = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Outer = do
    sh0 <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh0"; sh1 <- fsh "sh1"
    a <- ftv "a"; b <- ftv "b"; c <- ftv "c"
    pure ((a ~> b ~> c) ~> Arr sh0 a ~> Arr sh1 b ~> Arr (Cat sh0 sh1) c, mempty)
tyB a
_ Builtin
T = do
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"; a <- ftv "a"
    pure (Arr sh a ~> Arr (Rev sh) a, mempty)
tyB a
_ Builtin
Flat = do
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"; a <- ftv "a"
    pure (Arr sh a ~> Arr (Π sh) a, mempty)
tyB a
_ Builtin
AddDim = do
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"; a <- ftv "a"
    pure (Arr sh a ~> Arr (Ix()1 `Cons` sh) a, mempty)
tyB a
_ Builtin
CatE = do
    i <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; j <- fti "j"
    n <- ftv "a"
    pure (vV i n ~> vV j n ~> vV (StaPlus () i j) n, mempty)
tyB a
_ Builtin
Scan = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; sh <- fsh "sh"
    let i1 = () -> I () -> I () -> I ()
forall a. a -> I a -> I a -> I a
StaPlus () I ()
i (() -> Int -> I ()
forall a. a -> Int -> I a
Ix()Int
1)
        arrTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
Cons I ()
i1 Sh ()
sh) T ()
a
    pure ((a ~> a ~> a) ~> arrTy ~> arrTy, mempty)
tyB a
_ Builtin
ScanS = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; b <- ftv "b"
    i <- fti "i"; sh <- fsh "sh"
    let opTy = T ()
b T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
b
        arrTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
Cons I ()
i Sh ()
sh); rarrTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
Cons (() -> I () -> I () -> I ()
forall a. a -> I a -> I a -> I a
StaPlus () I ()
i (() -> Int -> I ()
forall a. a -> Int -> I a
Ix()Int
1)) Sh ()
sh)
        -- FIXME: 1+1?
    pure (opTy ~> b ~> arrTy a ~> rarrTy b, mempty)
tyB a
l (DI Int
n) = a -> Builtin -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> Builtin -> TyM a (T (), Subst a)
tyB a
l ([Int] -> Builtin
Conv [Int
n])
tyB a
_ (Conv [Int]
ns) = do
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"
    is <- zipWithM (\Int
_ Char
t -> Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti (Char -> Text
T.singleton Char
t)) ns ['i'..]
    a <- ftv "a"; b <- ftv "b"
    let nx = () -> Int -> I ()
forall a. a -> Int -> I a
Ix () (Int -> I ()) -> [Int] -> [I ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int]
ns
        opTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr ((I () -> Sh () -> Sh ()) -> Sh () -> [I ()] -> Sh ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
Cons Sh ()
sh [I ()]
nx) T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
b
        t = T () -> T () -> T ()
forall a. T a -> T a -> T a
Arrow (Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr ((I () -> Sh () -> Sh ()) -> Sh () -> [I ()] -> Sh ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
Cons Sh ()
sh ((I () -> I () -> I ()) -> [I ()] -> [I ()] -> [I ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (() -> I () -> I () -> I ()
forall a. a -> I a -> I a -> I a
StaPlus ()) [I ()]
is [I ()]
nx)) T ()
a) (Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr ((I () -> Sh () -> Sh ()) -> Sh () -> [I ()] -> Sh ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
Cons Sh ()
forall a. Sh a
Nil [I ()]
is) T ()
b)
    pure (opTy ~> t, mempty)
tyB a
_ Builtin
Succ = do
    i <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; sh <- fsh "sh"
    a <- ftv "a"; b <- ftv "b"
    let opTy = T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> (T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
b)
    pure (opTy ~> (Arr (StaPlus () i (Ix () 1) `Cons` sh) a ~> Arr (i `Cons` sh) b), mempty)
tyB a
_ (TAt Int
i) = do
    ρ <- Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"ρ" ()
    a <- ftv "a"
    pure (Ρ ρ (IM.singleton i a) ~> a, mempty)
tyB a
_ Builtin
Map = do
    i <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"
    a <- ftv "a"; b <- ftv "b"
    let fTy = T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
b
        gTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
i T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
i T ()
b
    -- depends on Arr nil a = a, Arr (i+j) a = Arr i (Arr j sh)
    pure (fTy ~> gTy, mempty)
tyB a
_ Builtin
Zip = do
    i <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"
    a <- ftv "a"; b <- ftv "b"; c <- ftv "c"
    let fTy = T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
b T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
c
        gTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
i T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
i T ()
b T () -> T () -> T ()
forall a. T a -> T a -> T a
~> I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
i T ()
c
    pure (fTy ~> gTy, mempty)
tyB a
l (Rank [(Int, Maybe [Int])]
as) = do
    let ixN :: a -> StateT (TySt a) (Either (TyE a)) [I ()]
ixN a
n = (a -> Char -> StateT (TySt a) (Either (TyE a)) (I ()))
-> [a] -> String -> StateT (TySt a) (Either (TyE a)) [I ()]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\a
_ Char
c -> Text -> StateT (TySt a) (Either (TyE a)) (I ())
forall a. Text -> TyM a (I ())
fti (Char -> Text
T.singleton Char
c)) [a
1..a
n] [Char
'i'..]
    shs <- ((Int, Maybe [Int]) -> TyM a (Sh ()))
-> [(Int, Maybe [Int])] -> StateT (TySt a) (Either (TyE a)) [Sh ()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Int
i,Maybe [Int]
ax) -> do {is <- Int -> StateT (TySt a) (Either (TyE a)) [I ()]
forall {a} {a}.
(Num a, Enum a) =>
a -> StateT (TySt a) (Either (TyE a)) [I ()]
ixN (Int -> ([Int] -> Int) -> Maybe [Int] -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
i [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Maybe [Int]
ax); sh <- fsh "sh"; pure $ foldr Cons sh is}) [(Int, Maybe [Int])]
as
    vs <- zipWithM (\(Int, Maybe [Int])
_ Char
c -> Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv (Char -> Text
T.singleton Char
c)) as ['a'..]
    codSh <- fsh "sh"
    cod <- ftv "c"
    let mArrs = (Sh () -> T () -> T ()) -> [Sh ()] -> [T ()] -> [T ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr [Sh ()]
shs [T ()]
vs
        codTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr Sh ()
codSh T ()
cod
        fTy = (T () -> T () -> T ()) -> T () -> [T ()] -> T ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr T () -> T () -> T ()
forall a. T a -> T a -> T a
(~>) T ()
cod ([T ()] -> T ()) -> [T ()] -> T ()
forall a b. (a -> b) -> a -> b
$ ((Int, Maybe [Int]) -> Sh () -> T () -> T ())
-> [(Int, Maybe [Int])] -> [Sh ()] -> [T ()] -> [T ()]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (\(Int, Maybe [Int])
ax Sh ()
sh T ()
t -> case (Int, Maybe [Int])
ax of {(Int
_,Maybe [Int]
Nothing) -> Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (Sh () -> Sh ()
forall a. Sh a -> Sh a
trim Sh ()
sh) T ()
t;(Int
_,Just [Int]
axs) -> Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr ([Int] -> Sh () -> Sh ()
forall a. [Int] -> Sh a -> Sh a
sel [Int]
axs Sh ()
sh) T ()
t}) [(Int, Maybe [Int])]
as [Sh ()]
shs [T ()]
vs
        rTy = (T () -> T () -> T ()) -> T () -> [T ()] -> T ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr T () -> T () -> T ()
forall a. T a -> T a -> T a
(~>) T ()
codTy [T ()]
mArrs
        shsU = ((Int, Maybe [Int]) -> Sh () -> Sh ())
-> [(Int, Maybe [Int])] -> [Sh ()] -> [Sh ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Int, Maybe [Int])
ax Sh ()
sh -> case (Int, Maybe [Int])
ax of {(Int
n,Maybe [Int]
Nothing) -> Int -> Sh () -> Sh ()
forall a. Int -> Sh a -> Sh a
tydrop Int
n Sh ()
sh;(Int
_,Just [Int]
axs) -> [Int] -> Sh () -> Sh ()
forall a. [Int] -> Sh a -> Sh a
del [Int]
axs Sh ()
sh}) [(Int, Maybe [Int])]
as [Sh ()]
shs
        shUHere Sh a
sh Sh a
sh' = ((Sh a, Subst a) -> Subst a)
-> StateT (TySt a) (Either (TyE a)) (Sh a, Subst a)
-> StateT (TySt a) (Either (TyE a)) (Subst a)
forall a b.
(a -> b)
-> StateT (TySt a) (Either (TyE a)) a
-> StateT (TySt a) (Either (TyE a)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sh a, Subst a) -> Subst a
forall a b. (a, b) -> b
snd (UM a (Sh a, Subst a)
-> StateT (TySt a) (Either (TyE a)) (Sh a, Subst a)
forall a x. UM a x -> TyM a x
liftU (UM a (Sh a, Subst a)
 -> StateT (TySt a) (Either (TyE a)) (Sh a, Subst a))
-> UM a (Sh a, Subst a)
-> StateT (TySt a) (Either (TyE a)) (Sh a, Subst a)
forall a b. (a -> b) -> a -> b
$ Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
forall a.
Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)
mgShPrep Focus
LF a
l Subst a
forall a. Monoid a => a
mempty (Sh a
shSh a -> a -> Sh a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>a
l) (Sh a
sh'Sh a -> a -> Sh a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>a
l))
    s <- zipWithM shUHere shsU (tail shsU++[codSh])
    pure (fTy ~> rTy, mconcat s)
tyB a
_ Builtin
Fold = do
    i <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; sh <- fsh "sh"; a <- ftv "a"
    let sh1 = () -> I () -> I () -> I ()
forall a. a -> I a -> I a -> I a
StaPlus () I ()
i (() -> Int -> I ()
forall a. a -> Int -> I a
Ix()Int
1) I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
sh
    pure ((a ~> a ~> a) ~> Arr sh1 a ~> Arr sh a, mempty)
tyB a
_ Builtin
FoldS = do
    i <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; sh <- fsh "sh"; a <- ftv "a"
    pure ((a ~> a ~> a) ~> a ~> Arr (i `Cons` sh) a ~> Arr sh a, mempty)
tyB a
_ Builtin
Foldl = do
    ix <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; sh <- fsh "sh"; a <- ftv "a"
    let sh1 = I ()
ix I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
sh
    pure ((a ~> a ~> a) ~> a ~> Arr sh1 a ~> Arr sh a, mempty)
tyB a
_ Builtin
FoldA = do
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"
    a <- ftv "a"
    pure ((a ~> a ~> a) ~> a ~> Arr sh a ~> a, mempty)
tyB a
_ Builtin
Dim = do
    iV <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; shV <- fsh "sh"; a <- ftv "a"
    pure (Arr (iV `Cons` shV) a ~> Li iV, mempty)
tyB a
_ Builtin
RevE = do
    iV <- Text -> TyM a (I ())
forall a. Text -> TyM a (I ())
fti Text
"i"; shV <- fsh "sh"; a <- ftv "a"
    let aTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I ()
iV I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
shV) T ()
a
    pure (aTy ~> aTy, mempty)
tyB a
_ Builtin
Size = do
    shV <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"
    a <- ftv "a"
    pure (Arr shV a ~> I, mempty)
tyB a
_ Builtin
Gen = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; n <- ftie
    let arrTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I ()
n I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
forall a. Sh a
Nil) T ()
a
    pure (a ~> (a ~> a) ~> I ~> arrTy, mempty)
tyB a
l Builtin
Mul = do
    a <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    i <- fti "i"; j <- fti "j"; k <- fti "k"
    pure (Arr (i `Cons` j `Cons` Nil) a ~> Arr (j `Cons` k `Cons` Nil) a ~> Arr (i `Cons` k `Cons` Nil) a, mempty)
tyB a
l Builtin
VMul = do
    a <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    i <- fti "i"; j <- fti "j"
    pure (Arr (i `Cons` j `Cons` Nil) a ~> vV j a ~> vV i a, mempty)
tyB a
l Builtin
Eye = do
    a <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum; i <- fti "i"
    pure (Arr (i `Cons` i `Cons` Nil) a, mempty)
tyB a
_ Builtin
Sin = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Cos = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Tan = (T (), Subst a) -> StateT (TySt a) (Either (TyE a)) (T (), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T ()
forall a. T a
F T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
F, Subst a
forall a. Monoid a => a
mempty)
tyB a
_ Builtin
Ices = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; n <- ftie
    pure ((a ~> B) ~> vV i a ~> vV n I, mempty)
tyB a
_ Builtin
Filt = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; i <- fti "i"; n <- ftie
    pure ((a ~> B) ~> vV i a ~> vV n a, mempty)
tyB a
_ Builtin
C = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"; b <- ftv "b"; c <- ftv "c"
    pure ((b ~> c) ~> (a ~> b) ~> a ~> c, mempty)

liftCloneTy :: T b -> TyM a (T b, IM.IntMap Int)
liftCloneTy :: forall b a. T b -> TyM a (T b, IntMap Int)
liftCloneTy T b
t = do
    i<- (TySt a -> Int) -> StateT (TySt a) (Either (TyE a)) Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TySt a -> Int
forall a. TySt a -> Int
maxU
    let (u,t',vs) = cloneT i t
    modify (setMaxU u) $> (t',vs)

cloneWithConstraints :: T b -> TyM a (T b)
cloneWithConstraints :: forall b a. T b -> TyM a (T b)
cloneWithConstraints T b
t = do
    (t', vs) <- T b -> TyM a (T b, IntMap Int)
forall b a. T b -> TyM a (T b, IntMap Int)
liftCloneTy T b
t
    traverse_ (\(Int
k,Int
v) -> do
        cst <- (TySt a -> IntMap (C, a))
-> StateT (TySt a) (Either (TyE a)) (IntMap (C, a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TySt a -> IntMap (C, a)
forall a. TySt a -> IntMap (C, a)
varConstr
        case IM.lookup k cst of
            Just (C
c,a
l) -> (TySt a -> TySt a) -> StateT (TySt a) (Either (TyE a)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> a -> C -> TySt a -> TySt a
forall a. Int -> a -> C -> TySt a -> TySt a
addVarConstrI Int
v a
l C
c)
            Maybe (C, a)
Nothing    -> () -> StateT (TySt a) (Either (TyE a)) ()
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
        (IM.toList vs)
    pure t'

rwI :: I a -> I a
rwI :: forall a. I a -> I a
rwI (StaPlus a
l I a
i0 I a
i1) =
    case (I a -> I a
forall a. I a -> I a
rwI I a
i0, I a -> I a
forall a. I a -> I a
rwI I a
i1) of
        (Ix a
lϵ Int
i, Ix a
_ Int
j) -> a -> Int -> I a
forall a. a -> Int -> I a
Ix a
lϵ (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j)
        (I a
i0', I a
i1')        -> a -> I a -> I a -> I a
forall a. a -> I a -> I a -> I a
StaPlus a
l I a
i0' I a
i1'
rwI (StaMul a
l I a
i0 I a
i1) =
    case (I a -> I a
forall a. I a -> I a
rwI I a
i0, I a -> I a
forall a. I a -> I a
rwI I a
i1) of
        (Ix a
lϵ Int
i, Ix a
_ Int
j) -> a -> Int -> I a
forall a. a -> Int -> I a
Ix a
lϵ (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
j)
        (I a
i0', I a
i1')        -> a -> I a -> I a -> I a
forall a. a -> I a -> I a -> I a
StaMul a
l I a
i0' I a
i1'
rwI I a
i = I a
i

rwSh :: Sh a -> Sh a
rwSh :: forall a. Sh a -> Sh a
rwSh s :: Sh a
s@SVar{}     = Sh a
s
rwSh s :: Sh a
s@Sh a
Nil        = Sh a
s
rwSh (I a
i `Cons` Sh a
s) = I a -> I a
forall a. I a -> I a
rwI I a
i I a -> Sh a -> Sh a
forall a. I a -> Sh a -> Sh a
`Cons` Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s
rwSh (Cat Sh a
s0 Sh a
s1) | ([I a]
is, Sh a
Nil) <- Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s0), ([I a]
js, Sh a
Nil) <- Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s1) = Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
forall a. Sh a
Nil ([I a]
is[I a] -> [I a] -> [I a]
forall a. [a] -> [a] -> [a]
++[I a]
js)
                 | Bool
otherwise = Sh a -> Sh a -> Sh a
forall a. Sh a -> Sh a -> Sh a
Cat (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s0) (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s1)
rwSh (Rev Sh a
s) | ([I a]
is, Sh a
Nil) <- Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s) = Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
forall a. Sh a
Nil ([I a] -> [I a]
forall a. [a] -> [a]
reverse [I a]
is)
             | Bool
otherwise = Sh a -> Sh a
forall a. Sh a -> Sh a
Rev (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s)
rwSh (Π Sh a
s) | Just I a
i <- Sh a -> Maybe (I a)
forall {a}. Sh a -> Maybe (I a)
iunroll (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s) = I a -> I a
forall a. I a -> I a
rwI I a
i I a -> Sh a -> Sh a
forall a. I a -> Sh a -> Sh a
`Cons` Sh a
forall a. Sh a
Nil
           | Bool
otherwise = Sh a -> Sh a
forall a. Sh a -> Sh a
Π (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
s)

rwArr :: T a -> T a
rwArr :: forall a. T a -> T a
rwArr (Arrow T a
t T a
t') = T a -> T a -> T a
forall a. T a -> T a -> T a
Arrow (T a -> T a
forall a. T a -> T a
rwArr T a
t) (T a -> T a
forall a. T a -> T a
rwArr T a
t')
rwArr T a
I            = T a
forall a. T a
I
rwArr T a
B            = T a
forall a. T a
B
rwArr T a
F            = T a
forall a. T a
F
rwArr t :: T a
t@Li{}       = T a
t
rwArr t :: T a
t@TVar{}     = T a
t
rwArr (P [T a]
ts)       = [T a] -> T a
forall a. [T a] -> T a
P (T a -> T a
forall a. T a -> T a
rwArr(T a -> T a) -> [T a] -> [T a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[T a]
ts)
rwArr (Arr Sh a
Nil T a
t)  = T a -> T a
forall a. T a -> T a
rwArr T a
t
rwArr (Arr Sh a
ixes T a
arr) | ([I a]
is, Sh a
Nil) <- Sh a -> ([I a], Sh a)
forall {a}. Sh a -> ([I a], Sh a)
unroll (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
ixes), Arr Sh a
sh T a
t <- T a -> T a
forall a. T a -> T a
rwArr T a
arr = Sh a -> T a -> T a
forall a. Sh a -> T a -> T a
Arr (Sh a -> [I a] -> Sh a
forall a. Sh a -> [I a] -> Sh a
roll Sh a
sh [I a]
is) T a
t
rwArr (Arr Sh a
sh T a
t)   = Sh a -> T a -> T a
forall a. Sh a -> T a -> T a
Arr (Sh a -> Sh a
forall a. Sh a -> Sh a
rwSh Sh a
sh) (T a -> T a
forall a. T a -> T a
rwArr T a
t)
rwArr (Ρ TyNm a
n IntMap (T a)
fs)     = TyNm a -> IntMap (T a) -> T a
forall a. TyNm a -> IntMap (T a) -> T a
Ρ TyNm a
n (T a -> T a
forall a. T a -> T a
rwArr(T a -> T a) -> IntMap (T a) -> IntMap (T a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>IntMap (T a)
fs)

hasEI :: I a -> Bool
hasEI :: forall a. I a -> Bool
hasEI IEVar{}            = Bool
True
hasEI (StaPlus a
_ I a
ix I a
ix') = I a -> Bool
forall a. I a -> Bool
hasEI I a
ix Bool -> Bool -> Bool
|| I a -> Bool
forall a. I a -> Bool
hasEI I a
ix'
hasEI (StaMul a
_ I a
ix I a
ix')  = I a -> Bool
forall a. I a -> Bool
hasEI I a
ix Bool -> Bool -> Bool
|| I a -> Bool
forall a. I a -> Bool
hasEI I a
ix'
hasEI I a
_                  = Bool
False

hasESh :: Sh a -> Bool
hasESh :: forall a. Sh a -> Bool
hasESh (Cons I a
i Sh a
sh) = I a -> Bool
forall a. I a -> Bool
hasEI I a
i Bool -> Bool -> Bool
|| Sh a -> Bool
forall a. Sh a -> Bool
hasESh Sh a
sh
hasESh Sh a
_           = Bool
False

hasE :: T a -> Bool
hasE :: forall a. T a -> Bool
hasE (Arrow T a
t t' :: T a
t'@Arrow{}) = T a -> Bool
forall a. T a -> Bool
hasE T a
t Bool -> Bool -> Bool
|| T a -> Bool
forall a. T a -> Bool
hasE T a
t'
hasE (Arr Sh a
sh T a
t)           = Sh a -> Bool
forall a. Sh a -> Bool
hasESh Sh a
sh Bool -> Bool -> Bool
|| T a -> Bool
forall a. T a -> Bool
hasE T a
t
hasE (P [T a]
ts)               = (T a -> Bool) -> [T a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T a -> Bool
forall a. T a -> Bool
hasE [T a]
ts
hasE T a
_                    = Bool
False

chkE :: T () -> Either (TyE a) ()
chkE :: forall a. T () -> Either (TyE a) ()
chkE t :: T ()
t@Arrow{} = if T () -> Bool
forall a. T a -> Bool
hasE T ()
t then TyE a -> Either (TyE a) ()
forall a b. a -> Either a b
Left (T () -> TyE a
forall a. T () -> TyE a
ExistentialArg T ()
t) else () -> Either (TyE a) ()
forall a b. b -> Either a b
Right ()
chkE T ()
_         = () -> Either (TyE a) ()
forall a b. b -> Either a b
Right ()

checkTy :: T a -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
checkTy :: forall a. T a -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
checkTy (TVar Nm a
n) (C
c, a
_)       = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C)))
-> Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a b. (a -> b) -> a -> b
$ (Nm a, C) -> Maybe (Nm a, C)
forall a. a -> Maybe a
Just(Nm a
n, C
c)
checkTy T a
I (C
IsNum, a
_)          = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
F (C
IsNum, a
_)          = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
I (C
IsOrd, a
_)          = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
I (C
HasBits, a
_)        = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
B (C
HasBits, a
_)        = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
F (C
IsOrd, a
_)          = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
I (C
IsEq, a
_)           = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
F (C
IsEq, a
_)           = Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing
checkTy T a
t (c :: C
c@C
IsNum, a
l)        = TyE a -> Either (TyE a) (Maybe (Nm a, C))
forall a b. a -> Either a b
Left(TyE a -> Either (TyE a) (Maybe (Nm a, C)))
-> TyE a -> Either (TyE a) (Maybe (Nm a, C))
forall a b. (a -> b) -> a -> b
$ a -> T a -> C -> TyE a
forall a. a -> T a -> C -> TyE a
Doesn'tSatisfy a
l T a
t C
c
checkTy T a
t (c :: C
c@C
HasBits, a
l)      = TyE a -> Either (TyE a) (Maybe (Nm a, C))
forall a b. a -> Either a b
Left(TyE a -> Either (TyE a) (Maybe (Nm a, C)))
-> TyE a -> Either (TyE a) (Maybe (Nm a, C))
forall a b. (a -> b) -> a -> b
$ a -> T a -> C -> TyE a
forall a. a -> T a -> C -> TyE a
Doesn'tSatisfy a
l T a
t C
c
checkTy (Arr Sh a
_ T a
t) c :: (C, a)
c@(C
IsEq, a
l) = T a -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
forall a. T a -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
checkTy T a
t (C, a)
c

substI :: Subst a -> Int -> Maybe (T a)
substI :: forall a. Subst a -> Int -> Maybe (T a)
substI s :: Subst a
s@(Subst IntMap (T a)
ts IntMap (I a)
is IntMap (Sh a)
sh) Int
i =
    case Int -> IntMap (T a) -> Maybe (T a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (T a)
ts of
        Just ty :: T a
ty@TVar{} -> T a -> Maybe (T a)
forall a. a -> Maybe a
Just (T a -> Maybe (T a)) -> T a -> Maybe (T a)
forall a b. (a -> b) -> a -> b
$ Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT (IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
forall a. IntMap (T a) -> IntMap (I a) -> IntMap (Sh a) -> Subst a
Subst (Int -> IntMap (T a) -> IntMap (T a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap (T a)
ts) IntMap (I a)
is IntMap (Sh a)
sh) T a
ty
        Just T a
ty        -> T a -> Maybe (T a)
forall a. a -> Maybe a
Just (T a -> Maybe (T a)) -> T a -> Maybe (T a)
forall a b. (a -> b) -> a -> b
$ Subst a -> T a -> T a
forall a. Subst a -> T a -> T a
aT Subst a
s T a
ty
        Maybe (T a)
Nothing        -> Maybe (T a)
forall a. Maybe a
Nothing

checkClass :: Subst a -> Int -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
checkClass :: forall a.
Subst a -> Int -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
checkClass Subst a
s Int
i (C, a)
c =
    case Subst a -> Int -> Maybe (T a)
forall a. Subst a -> Int -> Maybe (T a)
substI Subst a
s Int
i of
        Just T a
ty -> T a -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
forall a. T a -> (C, a) -> Either (TyE a) (Maybe (Nm a, C))
checkTy (T a -> T a
forall a. T a -> T a
rwArr T a
ty) (C, a)
c
        Maybe (T a)
Nothing -> Maybe (Nm a, C) -> Either (TyE a) (Maybe (Nm a, C))
forall a. a -> Either (TyE a) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Nm a, C)
forall a. Maybe a
Nothing

tyClosed :: Int -> E a -> Either (TyE a) (E (T ()), [(Nm a, C)], Int)
tyClosed :: forall a. Int -> E a -> Either (TyE a) (E (T ()), [(Nm a, C)], Int)
tyClosed Int
u E a
e = do
    ((eS, scs), i) <- Int
-> TyM a (E (T ()), [(Nm a, C)])
-> Either (TyE a) ((E (T ()), [(Nm a, C)]), Int)
forall a b. Int -> TyM a b -> Either (TyE a) (b, Int)
runTyM Int
u (do { (e', s) <- Subst a -> E a -> TyM a (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
forall a. Monoid a => a
mempty E a
e; cvs <- gets varConstr; scs <- liftEither $ catMaybes <$> traverse (uncurry$checkClass s) (IM.toList cvs); pure (rwArr.aT (void s)<$>e', scs) })
    let vs = T () -> IntSet
forall a. T a -> IntSet
occ (E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
eS); scs' = ((Nm a, C) -> Bool) -> [(Nm a, C)] -> [(Nm a, C)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Nm Text
_ (U Int
iϵ) a
_, C
_) -> Int
iϵ Int -> IntSet -> Bool
`IS.member` IntSet
vs) [(Nm a, C)]
scs
    chkE (eAnn eS) $> (eS, nubOrd scs', i)

tyE :: Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE :: forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s (EApp a
_ (Builtin a
_ Builtin
Re) (ILit a
_ Integer
n)) = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    let arrTy = T ()
a T () -> T () -> T ()
forall a. T a -> T a -> T a
~> I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV (() -> Int -> I ()
forall a. a -> Int -> I a
Ix () (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) T ()
a
    pure (EApp arrTy (Builtin (I ~> arrTy) Re) (ILit I n), s)
tyE Subst a
s (EApp a
_ (EApp a
_ (EApp a
_ (Builtin a
_ Builtin
FRange) E a
e0) E a
e1) (ILit a
_ Integer
n)) = do
    (e0',s0) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e0; (e1',s1) <- tyE s0 e1
    let tyE0 = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e0'; tyE1 = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e1'
        arrTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV (() -> Int -> I ()
forall a. a -> Int -> I a
Ix () (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) T ()
forall a. T a
F
        l0 = E a -> a
forall a. E a -> a
eAnn E a
e0; l1 = E a -> a
forall a. E a -> a
eAnn E a
e1
    s0' <- liftU $ mp (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftU $ mp (l1,e1) s0' F (eAnn e1' $> l1)
    pure (EApp arrTy (EApp (I ~> arrTy) (EApp (tyE1 ~> I ~> arrTy) (Builtin (tyE0 ~> tyE1 ~> I ~> arrTy) FRange) e0') e1') (ILit I n), s1')
tyE Subst a
s (EApp a
l eϵ :: E a
eϵ@(EApp a
_ (EApp a
_ (Builtin a
_ Builtin
FRange) E a
e0) E a
e1) E a
n) = do
    (nA, sϵ) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
n
    case aT (void sϵ) $ eAnn nA of
        iT :: T ()
iT@(Li I ()
ix) -> do
            (e0',s0) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
sϵ E a
e0; (e1',s1) <- tyE s0 e1
            let tyE0 = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e0'; tyE1 = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e1'
                arrTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
ix T ()
forall a. T a
F
                l0 = E a -> a
forall a. E a -> a
eAnn E a
e0; l1 = E a -> a
forall a. E a -> a
eAnn E a
e1
            s0' <- liftU $ mp (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftU $ mp (l1,e1) s0' F (eAnn e1' $> l1)
            pure (EApp arrTy (EApp (iT ~> arrTy) (EApp (tyE1 ~> iT ~> arrTy) (Builtin (tyE0 ~> tyE1 ~> iT ~> arrTy) FRange) e0') e1') nA, s1')
        T ()
_ -> do
            a <- Text -> a -> TyM a (T a)
forall b a. Text -> b -> TyM a (T b)
ft Text
"a" a
l; b <- ft "b" l
            (eϵ', s0) <- tyE sϵ eϵ
            let eϵTy = T a
a T a -> T a -> T a
forall a. T a -> T a -> T a
~> T a
b
            s1 <- liftU $ mp (l,eϵ) s0 (eAnn eϵ'$>l) eϵTy
            s2 <- liftU $ mp (l,n) s1 (eAnn nA$>l) a
            pure (EApp (void b) eϵ' nA, s2)
tyE Subst a
s (EApp a
_ (EApp a
_ (EApp a
_ (Builtin a
_ Builtin
Gen) E a
x) E a
f) (ILit a
_ Integer
n)) = do
    (x',s0) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
x; (f',s1) <- tyE s0 f
    let tyX = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
x'; tyF = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f'
        arrTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV (() -> Int -> I ()
forall a. a -> Int -> I a
Ix () (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) T ()
tyX
        lX = E a -> a
forall a. E a -> a
eAnn E a
x; lF = E a -> a
forall a. E a -> a
eAnn E a
f
    s1' <- liftU $ mp (lF, f) s1 ((tyX $> lX) ~> (tyX $> lX)) (tyF $> lF)
    pure (EApp arrTy (EApp (I ~> arrTy) (EApp (tyF ~> I ~> arrTy) (Builtin (tyX ~> tyF ~> I ~> arrTy) Gen) x') f') (ILit I n), s1')
tyE Subst a
s (EApp a
l e :: E a
e@(EApp a
_ (EApp a
_ (Builtin a
_ Builtin
Gen) E a
x) E a
f) E a
n) = do
    (nA, sϵ) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
n
    case aT (void sϵ) $ eAnn nA of
        iT :: T ()
iT@(Li I ()
ix) -> do
            (x',s0) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
sϵ E a
x; (f',s1) <- tyE s0 f
            let tyX = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
x'; tyF = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f'
                arrTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV I ()
ix T ()
tyX
                lX = E a -> a
forall a. E a -> a
eAnn E a
x; lF = E a -> a
forall a. E a -> a
eAnn E a
f
            s1' <- liftU $ mp (lF, f) s1 ((tyX $> lX) ~> (tyX $> lX)) (tyF $> lF)
            pure (EApp arrTy (EApp (iT ~> arrTy) (EApp (tyF ~> iT ~> arrTy) (Builtin (tyX ~> tyF ~> iT ~> arrTy) Gen) x') f') nA, s1')
        T ()
_ -> do
            a <- Text -> a -> TyM a (T a)
forall b a. Text -> b -> TyM a (T b)
ft Text
"a" a
l; b <- ft "b" l
            (e', s0) <- tyE sϵ e
            let eT = T a -> T a -> T a
forall a. T a -> T a -> T a
Arrow T a
a T a
b
            s1 <- liftU $ mp (l,e) s0 (eAnn e'$>l) eT
            s2 <- liftU $ mp (l,n) s1 (eAnn nA$>l) a
            pure (EApp (void b) e' nA, s2)
tyE Subst a
s eC :: E a
eC@(EApp a
lC (EApp a
_ (Builtin a
_ Builtin
Cyc) E a
e) (ILit a
_ Integer
m)) = do
    (e0, s0) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e
    ix <- fti "ix"
    a <- ftv "a"
    let t=Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I ()
ix I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
forall a. Sh a
Nil) T ()
a
        arrTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (() -> I () -> I () -> I ()
forall a. a -> I a -> I a -> I a
StaMul () I ()
ix (() -> Int -> I ()
forall a. a -> Int -> I a
Ix () (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m)) I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
forall a. Sh a
Nil) T ()
a
        lE=E a -> a
forall a. E a -> a
eAnn E a
e
    s1 <- liftU $ mp (lC,eC) s0 (eAnn e0$>lE) (t$>lE)
    pure (EApp arrTy (EApp (I ~> arrTy) (Builtin (t ~> I ~> arrTy) Cyc) e0) (ILit I m), s1)
tyE Subst a
s (EApp a
_ (EApp a
_ (EApp a
_ (Builtin a
_ Builtin
IRange) (ILit a
_ Integer
b)) (ILit a
_ Integer
e)) (ILit a
_ Integer
si)) = do
    let arrTy :: T ()
arrTy = I () -> T () -> T ()
forall {a}. I a -> T a -> T a
vV (() -> Int -> I ()
forall a. a -> Int -> I a
Ix () (Integer -> Int
forall a. Num a => Integer -> a
fromInteger ((Integer
eInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
bInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
si) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
si))) T ()
forall a. T a
I
    (E (T ()), Subst a)
-> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
arrTy (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
arrTy) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
arrTy) (T () -> Builtin -> E (T ())
forall a. a -> Builtin -> E a
Builtin (T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
forall a. T a
I T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
arrTy) Builtin
IRange) (T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I Integer
b)) (T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I Integer
e)) (T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I Integer
si), Subst a
s)
tyE Subst a
s (FLit a
_ Double
x) = (E (T ()), Subst a)
-> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F Double
x, Subst a
s)
tyE Subst a
s (BLit a
_ Bool
x) = (E (T ()), Subst a)
-> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> Bool -> E (T ())
forall a. a -> Bool -> E a
BLit T ()
forall a. T a
B Bool
x, Subst a
s)
tyE Subst a
s (ILit a
l Integer
m) = do
    n <- Text -> a -> C -> TyM a (T ())
forall a. Text -> a -> C -> TyM a (T ())
fc Text
"a" a
l C
IsNum
    pure (ILit n m, s)
tyE Subst a
s (Builtin a
l Builtin
b) = do {(t,sϵ) <- a -> Builtin -> TyM a (T (), Subst a)
forall a. a -> Builtin -> TyM a (T (), Subst a)
tyB a
l Builtin
b ; pure (Builtin t b, sϵ<>s)}
tyE Subst a
s (Lam a
_ Nm a
nϵ E a
e) = do
    n <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    modify (addStaEnv nϵ n)
    (e', s') <- tyE s e
    let lamTy = T ()
n T () -> T () -> T ()
forall a. T a -> T a -> T a
~> E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e'
    pure (Lam lamTy (nϵ { loc = n }) e', s')
tyE Subst a
s (Let a
_ (Nm a
n, E a
e') E a
e) = do
    (e'Res, s') <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e'
    let e'Ty = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e'Res
    modify (addStaEnv n (aT (void s') e'Ty))
    (eRes, s'') <- tyE s' e
    pure (Let (eAnn eRes) (n { loc = e'Ty }, e'Res) eRes, s'')
tyE Subst a
s (Def a
_ (Nm a
n, E a
e') E a
e) = do
    (e'Res, s') <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e'
    let e'Ty = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e'Res
    modify (addPolyEnv n (aT (void s') e'Ty))
    (eRes, s'') <- tyE s' e
    pure (Def (eAnn eRes) (n { loc = e'Ty }, e'Res) eRes, s'')
tyE Subst a
s (LLet a
_ (Nm a
n, E a
e') E a
e) = do
    (e'Res, s') <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e'
    let e'Ty = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e'Res
    modify (addStaEnv n (aT (void s') e'Ty))
    (eRes, s'') <- tyE s' e
    pure (LLet (eAnn eRes) (n { loc = e'Ty }, e'Res) eRes, s'')
tyE Subst a
s e :: E a
e@(ALit a
l [E a]
es) = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    (es', s') <- sSt s es
    let eTys = T ()
a T () -> [T ()] -> [T ()]
forall a. a -> [a] -> [a]
: (E (T ()) -> T ()) -> [E (T ())] -> [T ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap E (T ()) -> T ()
forall a. E a -> a
eAnn [E (T ())]
es'
        uHere Subst a
sϵ T a
t T a
t' = (a, E a) -> Subst a -> T a -> T a -> UM a (Subst a)
forall a. (a, E a) -> Subst a -> T a -> T a -> UM a (Subst a)
mp (a
l,E a
e) Subst a
sϵ (T a
tT a -> a -> T a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>a
l) (T a
t'T a -> a -> T a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>a
l)
    ss' <- liftU $ zS uHere s' eTys (tail eTys)
    pure (ALit (vV (Ix () $ length es) a) es', ss')
tyE Subst a
s (EApp a
l E a
e0 E a
e1) = do
    a <- Text -> a -> TyM a (T a)
forall b a. Text -> b -> TyM a (T b)
ft Text
"a" a
l; b <- ft "b" l
    (e0', s0) <- tyE s e0
    (e1', s1) <- tyE s0 e1
    let e0Ty = T a
a T a -> T a -> T a
forall a. T a -> T a -> T a
~> T a
b
    s2 <- liftU $ mp (l,e0) s1 (eAnn e0'$>l) e0Ty
    s3 <- liftU $ mp (l,e1) s2 (eAnn e1'$>l) a
    pure (EApp (void b) e0' e1', s3)
tyE Subst a
s (Cond a
l E a
p E a
e0 E a
e1) = do
    (p',sP) <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
p
    (e0',s0) <- tyE sP e0
    (e1',s1) <- tyE s0 e1
    sP' <- liftU $ mp (eAnn p,p) s1 B (eAnn p'$>eAnn p); (tB, s0') <- liftU $ mguPrep RF (l,e0) sP' (eAnn e0'$>l) (eAnn e1'$>eAnn e1)
    pure (Cond (void tB) p' e0' e1', s0')
tyE Subst a
s (Var a
l n :: Nm a
n@(Nm Text
_ (U Int
u) a
_)) = do
    lSt<- (TySt a -> IntMap (T ()))
-> StateT (TySt a) (Either (TyE a)) (IntMap (T ()))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TySt a -> IntMap (T ())
forall a. TySt a -> IntMap (T ())
staEnv
    case IM.lookup u lSt of
        Just T ()
t  -> (E (T ()), Subst a)
-> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
t (Nm a
n Nm a -> T () -> Nm (T ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> T ()
t), Subst a
s)
        Maybe (T ())
Nothing -> do
            vSt<- (TySt a -> IntMap (T ()))
-> StateT (TySt a) (Either (TyE a)) (IntMap (T ()))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TySt a -> IntMap (T ())
forall a. TySt a -> IntMap (T ())
polyEnv
            case IM.lookup u vSt of
                Just T ()
t  -> do {t'<- T () -> TyM a (T ())
forall b a. T b -> TyM a (T b)
cloneWithConstraints T ()
t; pure (Var t' (n$>t'), s)}
                Maybe (T ())
Nothing -> TyE a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. TyE a -> StateT (TySt a) (Either (TyE a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TyE a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a))
-> TyE a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a b. (a -> b) -> a -> b
$ a -> Nm a -> TyE a
forall a. a -> Nm a -> TyE a
IllScoped a
l Nm a
n
tyE Subst a
s (Tup a
_ [E a]
es) = do
    (es', s') <- Subst a -> [E a] -> TyM a ([E (T ())], Subst a)
forall a. Subst a -> [E a] -> TyM a ([E (T ())], Subst a)
sSt Subst a
s [E a]
es
    let eTys = E (T ()) -> T ()
forall a. E a -> a
eAnn(E (T ()) -> T ()) -> [E (T ())] -> [T ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[E (T ())]
es'
    pure (Tup (P eTys) es', s')
tyE Subst a
s (Ann a
l E a
e T a
t) = do
    (e', s') <- Subst a
-> E a -> StateT (TySt a) (Either (TyE a)) (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e
    s'' <- liftEither $ maM LF (aT s'$fmap ($>l) eAnn e') (aT s' (t$>l))
    pure (e', s'<>s'')

sSt :: Subst a -> [E a] -> TyM a ([E (T ())], Subst a)
sSt :: forall a. Subst a -> [E a] -> TyM a ([E (T ())], Subst a)
sSt Subst a
s []     = ([E (T ())], Subst a)
-> StateT (TySt a) (Either (TyE a)) ([E (T ())], Subst a)
forall a. a -> StateT (TySt a) (Either (TyE a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure([], Subst a
s)
sSt Subst a
s (E a
e:[E a]
es) = do{(e',s') <- Subst a -> E a -> TyM a (E (T ()), Subst a)
forall a. Subst a -> E a -> TyM a (E (T ()), Subst a)
tyE Subst a
s E a
e; first (e':) <$> sSt s' es} -- TODO: recurse other way idk