{-# 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)
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 ()) (Sh ())
           | MatchIFailed a (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 ()
sh Sh ()
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 () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh () -> Doc ann
pretty Sh ()
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 () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Sh () -> Doc ann
pretty Sh ()
sh')
    pretty (MatchIFailed a
l I a
i I a
i')   = 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
"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))

mI :: I a -> I a -> Either (TyE a) (Subst a)
mI :: forall a. I a -> I a -> Either (TyE a) (Subst a)
mI i0 :: I a
i0@(Ix a
l 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
$ a -> I a -> I a -> TyE a
forall a. a -> I a -> I a -> TyE a
MatchIFailed a
l I a
i0 I a
i1
mI (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 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 (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 (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ϵ = I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI 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 (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 = I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI 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 (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
<$> I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI 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
<*> I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI I a
j I a
j' -- FIXME: too stringent
mI (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
<$> I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI 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
<*> I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI I a
j I a
j' -- FIXME: too stringent

mSh :: Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh :: forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh (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 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 (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
<$> I a -> I a -> Either (TyE a) (Subst a)
forall a. I a -> I a -> Either (TyE a) (Subst a)
mI 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
<*> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Sh a
sh Sh a
sh'
mSh (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
<$> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh 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
<*> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Sh a
sh1 Sh a
sh1'
mSh (Rev Sh a
sh) (Rev Sh a
sh')            = Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh Sh a
sh Sh a
sh'
mSh 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 () -> Sh () -> TyE a
forall a. Sh () -> Sh () -> TyE a
MatchShFailed (Sh a -> Sh ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Sh a
sh) (Sh a -> Sh ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void 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 (T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM T a
t T a
t')

maM :: T a -> T a -> Either (TyE a) (Subst a)
maM :: forall a. T a -> T a -> Either (TyE a) (Subst a)
maM 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 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 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 (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 (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 (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
<$> T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM 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
<*> T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM T a
t1 T a
t1' -- FIXME: use <\> over <>
maM (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
<$> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh 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
<*> T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM T a
t T a
t'
maM (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
<$> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. Sh a -> Sh a -> Either (TyE a) (Subst a)
mSh 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
<*> T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM T a
t T a
t'
maM (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 T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM [T a]
ts [T a]
ts'
maM (Ρ 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 (Ρ 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 T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM) (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 (Ρ 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 T a -> T a -> Either (TyE a) (Subst a)
forall a. T a -> T a -> Either (TyE a) (Subst a)
maM) [ ([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 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 ()

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 ()

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)

mguIPrep :: IM.IntMap (I a) -> I a -> I a -> Either (TyE a) (IM.IntMap (I a))
mguIPrep :: forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep 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 IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguI 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 :: IM.IntMap (I a) -> I a -> I a -> Either (TyE a) (IM.IntMap (I a))
mguI :: forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguI IntMap (I a)
inp i0 :: I a
i0@(Ix a
l Int
i) i1 :: I a
i1@(Ix a
_ Int
j) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. b -> Either a b
Right IntMap (I a)
inp
                                 | Bool
otherwise = TyE a -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left(TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
inp i0 :: I a
i0@(IEVar a
l Nm a
i) i1 :: I a
i1@(IEVar a
_ Nm a
j) | Nm a
i Nm a -> Nm a -> Bool
forall a. Eq a => a -> a -> Bool
== Nm a
j = IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. b -> Either a b
Right IntMap (I a)
inp
                                       | Bool
otherwise = TyE a -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
inp (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 = IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. b -> Either a b
Right IntMap (I a)
inp
mguI 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 -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 = IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. b -> Either a b
Right (IntMap (I a) -> Either (TyE a) (IntMap (I a)))
-> IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. (a -> b) -> a -> b
$ 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 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 -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left(TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 = IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. b -> Either a b
Right (IntMap (I a) -> Either (TyE a) (IntMap (I a)))
-> IntMap (I a) -> Either (TyE a) (IntMap (I a))
forall a b. (a -> b) -> a -> b
$ 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 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 = IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep IntMap (I a)
inp I a
i0 I a
i1
mguI 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 = IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep IntMap (I a)
inp I a
i0 I a
i1
mguI 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 = IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep 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 -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
inp i0 :: I a
i0@Ix{} i1 :: I a
i1@(StaPlus a
_ I a
_ Ix{}) = IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep IntMap (I a)
inp I a
i1 I a
i0
mguI IntMap (I a)
inp (StaMul a
_ I a
i0 I a
i1) (StaMul a
_ I a
j0 I a
j1) = do
    -- FIXME: too stringent
    s <- IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep IntMap (I a)
inp I a
i0 I a
j0
    mguIPrep s i1 j1
mguI IntMap (I a)
_ i0 :: I a
i0@(IEVar a
l Nm a
_) i1 :: I a
i1@Ix{} = TyE a -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
_ i0 :: I a
i0@(Ix a
l Int
_) i1 :: I a
i1@IEVar{} = TyE a -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
_ i0 :: I a
i0@(IEVar a
l Nm a
_) i1 :: I a
i1@StaPlus{} = TyE a -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
_ i0 :: I a
i0@(StaPlus a
l I a
_ I a
_) i1 :: I a
i1@IEVar{} = TyE a -> Either (TyE a) (IntMap (I a))
forall a b. a -> Either a b
Left (TyE a -> Either (TyE a) (IntMap (I a)))
-> TyE a -> Either (TyE 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 IntMap (I a)
_ I a
i0 I a
i1 = String -> Either (TyE 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 :: a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep :: forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep 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 a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgSh 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 :: a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgSh :: forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgSh a
_ Subst a
inp Sh a
Nil Sh a
Nil = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
inp
mgSh a
l Subst a
inp (Cons I a
i Sh a
sh) (Cons I a
i' Sh a
sh') = do
    sI <- IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep (Subst a -> IntMap (I a)
forall a. Subst a -> IntMap (I a)
iSubst Subst a
inp) I a
i I a
i'
    mgShPrep l (inp { iSubst = sI }) sh sh'
mgSh a
_ Subst a
inp (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' = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
inp
mgSh 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 -> 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
$ 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 = 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 (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 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 -> 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
$ 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 = 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 (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 a
l Subst a
_ sh :: Sh a
sh@Sh a
Nil sh' :: Sh a
sh'@Cons{} = 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
$ 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 a
l Subst a
_ sh :: Sh a
sh@Cons{} sh' :: Sh a
sh'@Nil{} = 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
$ 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 a
l Subst a
inp (Rev Sh a
sh) (Rev Sh a
sh') = a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep a
l Subst a
inp Sh a
sh Sh a
sh'
mgSh a
l Subst a
inp (Cat Sh a
sh0 Sh a
sh0') (Cat Sh a
sh1 Sh a
sh1') = do
    s <- a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep a
l Subst a
inp Sh a
sh0 Sh a
sh1
    mgShPrep l s sh0' sh1'
mgSh 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
    a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep 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 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
    a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep 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 :: (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep :: forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (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 (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mgu (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')

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 :: (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mgu :: forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mgu (a, E a)
l Subst a
s (Arrow T a
t0 T a
t1) (Arrow T a
t0' T a
t1') = do
    s0 <- (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
t0 T a
t0'
    mguPrep l s0 t1 t1'
mgu (a, E a)
_ Subst a
s T a
I T a
I = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
s
mgu (a, E a)
_ Subst a
s T a
F T a
F = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
s
mgu (a, E a)
_ Subst a
s T a
B T a
B = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
s
mgu (a, E a)
_ Subst a
s Li{} T a
I = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
s
mgu (a, E a)
_ Subst a
s T a
I Li{} = Subst a -> Either (TyE a) (Subst a)
forall a b. b -> Either a b
Right Subst a
s
mgu (a, E a)
_ Subst a
s (Li I a
i0) (Li I a
i1) = do {iS <- IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
forall a.
IntMap (I a) -> I a -> I a -> Either (TyE a) (IntMap (I a))
mguIPrep (Subst a -> IntMap (I a)
forall a. Subst a -> IntMap (I a)
iSubst Subst a
s) I a
i0 I a
i1; pure $ Subst mempty iS mempty <> s}
mgu (a, E a)
_ Subst a
s (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
s
mgu (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 -> 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
$ 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 = 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 (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 (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 -> 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
$ 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 = 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 (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 (a
l, E a
e) Subst a
_ t0 :: T a
t0@Arrow{} T a
t1 = 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
$ 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 (a
l, E a
e) Subst a
_ T a
t0 t1 :: T a
t1@Arrow{} = 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
$ 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 (a, E a)
l Subst a
s (Arr Sh a
sh T a
t) (Arr Sh a
sh' T a
t') = do
    s0 <- (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
t T a
t'
    mgShPrep (fst l) s0 sh sh'
mgu (a
l, E a
e) Subst a
_ T a
F T a
I = 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
$ 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 (a
l, E a
e) Subst a
_ T a
I T a
F = 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
$ 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 (a
l, E a
e) Subst a
_ T a
F t :: T a
t@Li{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Li{} T a
F = 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
$ 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 (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) T a
F = (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) (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
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
t T a
forall a. T a
F
mgu (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) T a
I = (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) (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
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
t T a
forall a. T a
I
mgu (a, E a)
l Subst a
s T a
F (Arr (SVar Nm a
n) T a
t) = (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) (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
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
forall a. T a
F T a
t
mgu (a, E a)
l Subst a
s T a
I (Arr (SVar Nm a
n) T a
t) = (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) (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
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
forall a. T a
I T a
t
mgu (a, E a)
l Subst a
s (Arr (SVar Nm a
n) T a
t) t' :: T a
t'@P{} = (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) (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
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
t T a
t'
mgu (a, E a)
l Subst a
s t' :: T a
t'@P{} (Arr (SVar Nm a
n) T a
t) = (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) (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
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
s T a
t' T a
t
mgu (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' = (Subst a -> T a -> T a -> Either (TyE a) (Subst a))
-> Subst a -> [T a] -> [T a] -> Either (TyE a) (Subst a)
forall {f :: * -> *} {t} {t} {t}.
Monad f =>
(t -> t -> t -> f t) -> t -> [t] -> [t] -> f t
zS ((a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l) Subst a
s [T a]
ts [T a]
ts'
-- TODO: rho occurs check
mgu 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 = (Subst a -> (Int, T a) -> Either (TyE a) (Subst a))
-> Subst a -> [(Int, T a)] -> Either (TyE a) (Subst a)
forall (m :: * -> *) a b.
Monad m =>
(Subst a -> b -> m (Subst a)) -> Subst a -> [b] -> m (Subst a)
tS (\Subst a
sϵ (Int
i, 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 (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)
-> Either (TyE a) (Subst a) -> Either (TyE a) (Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (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 -> 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
$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 (a, E a)
l Subst a
s t :: T a
t@P{} t' :: T a
t'@Ρ{} = (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mgu (a, E a)
l Subst a
s T a
t' T a
t
mgu (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) -> Either (TyE a) (Subst a))
-> Subst a -> [(T a, T a)] -> Either (TyE a) (Subst a)
forall (m :: * -> *) a b.
Monad m =>
(Subst a -> b -> m (Subst a)) -> Subst a -> [b] -> m (Subst a)
tS (\Subst a
sϵ (T a
t0,T a
t1) -> (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (a, E a)
l Subst a
sϵ T a
t0 T a
t1) Subst a
s ([(T a, T a)] -> Either (TyE a) (Subst a))
-> [(T a, T a)] -> Either (TyE 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'
    pure $ mapTySubst (insert n (Ρ n' (rs<>rs'))) rss
mgu (a
l, E a
e) Subst a
_ T a
F t :: T a
t@Arr{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} T a
F = 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
$ 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 (a
l, E a
e) Subst a
_ T a
B t :: T a
t@Arr{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} T a
B = 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
$ 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 (a
l, E a
e) Subst a
_ T a
I t :: T a
t@Arr{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} T a
I = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Li{} t' :: T a
t'@Arr{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} t' :: T a
t'@Li{} = 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
$ 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 (a
l, E a
e) Subst a
_ T a
F t :: T a
t@P{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@P{} T a
F = 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
$ 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 (a
l, E a
e) Subst a
_ T a
I t :: T a
t@P{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@P{} T a
I = 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
$ 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 (a
l, E a
e) Subst a
_ T a
B t :: T a
t@P{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@P{} T a
B = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@P{} t' :: T a
t'@Arr{} = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Arr{} t' :: T a
t'@P{} = 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
$ 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 (a
l, E a
e) Subst a
_ T a
I T a
B= 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
$ 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 (a
l, E a
e) Subst a
_ T a
B T a
I = 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
$ 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 (a
l, E a
e) Subst a
_ t :: T a
t@Li{} T a
B = 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
$ 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 (a
l, E a
e) Subst a
_ T a
B t :: T a
t@Li{} = 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
$ 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

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 (Subst a)) -> Subst a -> [b] -> m (Subst a)
tS :: forall (m :: * -> *) a b.
Monad m =>
(Subst a -> b -> m (Subst a)) -> Subst a -> [b] -> m (Subst a)
tS Subst a -> b -> m (Subst a)
_ Subst a
s []     = Subst a -> m (Subst a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst a
s
tS Subst a -> b -> m (Subst a)
f Subst a
s (b
t:[b]
ts) = do{next <- Subst a -> b -> m (Subst a)
f Subst a
s b
t; tS f next ts}

vx :: I a -> Sh a
vx I a
i = I a -> Sh a -> Sh a
forall a. I a -> Sh a -> Sh a
Cons I a
i Sh a
forall a. Sh a
Nil

tyNumBinOp :: a -> TyM a (T (), Subst a)
tyNumBinOp :: forall a. a -> TyM a (T (), Subst a)
tyNumBinOp a
l = do
    n <- Text -> a -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l 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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"o" a
l
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l 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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"b" a
l
    let n'=Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l 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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"o" a
l
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l IsOrd
    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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l; sh <- freshN "sh" ()
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l IsNum
    pure (n' ~> n' ~> Arr (SVar 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 <- IVar () <$> freshN "i" ()
    pure (a ~> Arr (i `Cons` Nil) a ~> Arr (StaPlus () i (Ix()1) `Cons` Nil) 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 <- IVar () <$> freshN "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 <- IVar () <$> freshN "i" ()
    pure ((a ~> B) ~> Arr (i `Cons` Nil) a ~> I, mempty)
tyB a
_ Builtin
Di = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (Arr (i `Cons` i `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)
tyB a
_ Builtin
LastM = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (Arr (i `Cons` Nil) a ~> a, mempty)
tyB a
_ Builtin
Last = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> a, mempty)
tyB a
_ Builtin
Head = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> a, mempty)
tyB a
_ Builtin
Init = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)
tyB a
_ Builtin
Tail = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)
tyB a
_ Builtin
Rot = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    pure (I ~> Arr (i `Cons` Nil) a ~> Arr (i `Cons` Nil) 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 <- IVar () <$> freshN "i" ()
    n <- IEVar () <$> freshN "n" ()
    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 <- IVar () <$> freshN "i" ()
    pure (Arr (i `Cons` Nil) a ~> a, mempty)
tyB a
_ Builtin
Re = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    n <- IEVar () <$> freshN "n" ()
    pure (I ~> a ~> Arr (n `Cons` Nil) a, mempty)
tyB a
_ Builtin
FRange = do
    n <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IEVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"n" ()
    pure (F ~> F ~> I ~> Arr (n `Cons` Nil) F, mempty)
tyB a
_ Builtin
Fib = do
    n <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IEVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"n" ()
    a <- freshN "a" ()
    let a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
a
        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 <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IEVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"n" ()
    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)
tyOrdBinRel 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)
tyOrdBinRel 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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"b" a
l
    let n'=Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l 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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l IsNum
    pure (n' ~> I ~> n', mempty)
tyB a
l Builtin
Neg = do
    n <- Text -> a -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l IsNum
    pure (n' ~> n', mempty)
tyB a
l Builtin
Abs = do
    n <- Text -> a -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    let n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
n)
    pushVarConstraint n l 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 (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"i" (); j <- freshN "j" ()
    n <- freshN "a" ()
    let i' = () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () Nm ()
i; j' = () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () Nm ()
j; n' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
n
    pure (Arr (vx i') n' ~> Arr (vx j') n' ~> Arr (vx $ 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 <- IVar () <$> freshN "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 <- IVar () <$> freshN "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 -> () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN (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
    sh <- Text -> TyM a (Sh ())
forall a. Text -> TyM a (Sh ())
fsh Text
"sh"
    i <- IVar () <$> freshN "i" ()
    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 <- freshN "a" ()
    let aV = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
a
    pure (Ρ ρ (IM.singleton i aV) ~> aV, mempty)
tyB a
_ Builtin
Map = do
    ix <- Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"i" ()
    a <- freshN "a" (); b <- freshN "b" ()
    let arrSh = () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () Nm ()
ix I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
forall a. Sh a
Nil -- TODO: sh??
        a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
a; b' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
b
        fTy = T ()
a' T () -> T () -> T ()
forall a. T a -> T a -> T a
~> T ()
b'
        gTy = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr Sh ()
arrSh T ()
a' T () -> T () -> T ()
forall a. T a -> T a -> T a
~> Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr Sh ()
arrSh 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 (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"i" ()
    a <- freshN "a" (); b <- freshN "b" (); c <- freshN "c" ()
    let arrSh = () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () Nm ()
i I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
forall a. Sh a
Nil
        a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
a; b' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
b; c' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
c
        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 = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr Sh ()
arrSh T ()
a' T () -> T () -> T ()
forall a. T a -> T a -> T a
~> Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr Sh ()
arrSh T ()
b' T () -> T () -> T ()
forall a. T a -> T a -> T a
~> Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr Sh ()
arrSh T ()
c'
    pure (fTy ~> gTy, mempty)
tyB a
l (Rank [(Int, Maybe [Int])]
as) = do
    let ixN :: a -> StateT (TySt a) (Either (TyE a)) [Nm ()]
ixN a
n = (a -> Char -> StateT (TySt a) (Either (TyE a)) (Nm ()))
-> [a] -> String -> StateT (TySt a) (Either (TyE a)) [Nm ()]
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)) (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN (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)) [Nm ()]
forall {a} {a}.
(Num a, Enum a) =>
a -> StateT (TySt a) (Either (TyE a)) [Nm ()]
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 (IVar () <$> 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 <- freshN "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 (Nm () -> Sh ()
forall a. Nm a -> Sh a
SVar Nm ()
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' = Either (TyE a) (Subst a) -> m (Subst a)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TyE a) (Subst a) -> m (Subst a))
-> Either (TyE a) (Subst a) -> m (Subst a)
forall a b. (a -> b) -> a -> b
$ a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
forall a. a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)
mgShPrep 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++[SVar codSh])
    pure (fTy ~> rTy, mconcat s)
tyB a
_ Builtin
Fold = do
    ix <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"i" ()
    sh <- fsh "sh"
    a <- freshN "a" ()
    let sh1 = () -> I () -> I () -> I ()
forall a. a -> I a -> I a -> I a
StaPlus () I ()
ix (() -> 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
        a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
a
    pure ((a' ~> a' ~> a') ~> Arr sh1 a' ~> Arr sh a', mempty)
tyB a
_ Builtin
FoldS = do
    ix <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"i" ()
    sh <- fsh "sh"
    a <- freshN "a" ()
    let sh1 = I ()
ix I () -> Sh () -> Sh ()
forall a. I a -> Sh a -> Sh a
`Cons` Sh ()
sh
        a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar Nm ()
a
    pure ((a' ~> a' ~> a') ~> a' ~> Arr sh1 a' ~> Arr sh a', mempty)
tyB a
_ Builtin
Foldl = do
    ix <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN 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 <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"i" ()
    shV <- fsh "sh"
    a <- ftv "a"
    pure (Arr (iV `Cons` shV) a ~> Li iV, mempty)
tyB a
_ Builtin
RevE = do
    iV <- () -> Nm () -> I ()
forall a. a -> Nm a -> I a
IVar () (Nm () -> I ())
-> TyM a (Nm ()) -> StateT (TySt a) (Either (TyE a)) (I ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> () -> TyM a (Nm ())
forall b a. Text -> b -> TyM a (Nm b)
freshN 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 <- IEVar () <$> freshN "n" ()
    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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    i <- IVar () <$> freshN "i" (); j <- IVar () <$> freshN "j" (); k <- IVar () <$> freshN "k" ()
    pushVarConstraint a l IsNum
    let a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
a)
    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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    i <- IVar () <$> freshN "i" (); j <- IVar () <$> freshN "j" ()
    pushVarConstraint a l IsNum
    let a' = Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
a)
    pure (Arr (i `Cons` j `Cons` Nil) a' ~> Arr (j `Cons` Nil) a' ~> Arr (i `Cons` Nil) a', mempty)
tyB a
l Builtin
Eye = do
    a <- Text -> a -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    i <- IVar () <$> freshN "i" ()
    pushVarConstraint a l IsNum
    let a'=Nm () -> T ()
forall a. TyNm a -> T a
TVar (Nm a -> Nm ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Nm a
a)
    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 <- IVar () <$> freshN "i" ()
    n <- IEVar () <$> freshN "n" ()
    pure ((a ~> B) ~> Arr (vx i) a ~> Arr (vx n) I, mempty)
tyB a
_ Builtin
Filt = do
    a <- Text -> TyM a (T ())
forall a. Text -> TyM a (T ())
ftv Text
"a"
    i <- IVar () <$> freshN "i" ()
    n <- IEVar () <$> freshN "n" ()
    pure ((a ~> B) ~> Arr (vx i) a ~> Arr (vx n) I, 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
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

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
~> Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh ()
forall {a}. I a -> Sh a
vx (I () -> Sh ()) -> I () -> Sh ()
forall a b. (a -> b) -> a -> b
$ () -> 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 = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh ()
forall {a}. I a -> Sh a
vx (() -> 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' <- liftEither $ mguPrep (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftEither $ mguPrep (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 = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh ()
forall {a}. I a -> Sh a
vx 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' <- liftEither $ mguPrep (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftEither $ mguPrep (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 <- liftEither $ mguPrep (l,eϵ) s0 (eAnn eϵ'$>l) eϵTy
            s2 <- liftEither $ mguPrep (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 = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh ()
forall {a}. I a -> Sh a
vx (I () -> Sh ()) -> I () -> Sh ()
forall a b. (a -> b) -> a -> b
$ () -> 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' <- liftEither $ mguPrep (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 = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh ()
forall {a}. I a -> Sh a
vx 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' <- liftEither $ mguPrep (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 <- liftEither $ mguPrep (l,e) s0 (eAnn e'$>l) eT
            s2 <- liftEither $ mguPrep (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 <- IVar () <$> freshN "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 <- liftEither $ mguPrep (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 = Sh () -> T () -> T ()
forall a. Sh a -> T a -> T a
Arr (I () -> Sh ()
forall {a}. I a -> Sh a
vx (() -> 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 -> TyM a (Nm a)
forall b a. Text -> b -> TyM a (Nm b)
freshN Text
"a" a
l
    pushVarConstraint n l IsNum
    pure (ILit (TVar (void 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 -> Either (TyE a) (Subst a)
forall a.
(a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)
mguPrep (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' <- liftEither $ zS uHere s' eTys (tail eTys)
    pure (ALit (Arr (vx (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 <- liftEither $ mguPrep (l,e0) s1 (eAnn e0'$>l) e0Ty
    s3 <- liftEither $ mguPrep (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' <- liftEither $ mguPrep (eAnn p,p) s1 B (eAnn p'$>eAnn p); s0' <- liftEither $ mguPrep (l,e0) sP' (eAnn e0'$>l) (eAnn e1'$>eAnn e1)
    pure (Cond (eAnn e0') 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 (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