{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE OverloadedStrings #-}

module Ty.M ( check, RE (..) ) where

import           A
import           Control.Applicative (Alternative (..))
import           Control.DeepSeq     (NFData)
import           Data.Foldable       (asum)
import           GHC.Generics        (Generic)
import           Prettyprinter       (Pretty (..), squotes, (<+>))

data RE = MR (E (T ())) (T ()) | Unflat (E (T ())) (T ()) | UT (E (T ())) (T ()) | IS (Sh ()) | ES (Sh ()) deriving ((forall x. RE -> Rep RE x)
-> (forall x. Rep RE x -> RE) -> Generic RE
forall x. Rep RE x -> RE
forall x. RE -> Rep RE x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RE -> Rep RE x
from :: forall x. RE -> Rep RE x
$cto :: forall x. Rep RE x -> RE
to :: forall x. Rep RE x -> RE
Generic)

instance NFData RE where

instance Pretty RE where
    pretty :: forall ann. RE -> Doc ann
pretty (MR E (T ())
e T ()
t)     = Doc ann
"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) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of 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 (T ()) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. E (T ()) -> Doc ann
pretty E (T ())
e) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not sufficiently monomorphic."
    pretty (Unflat E (T ())
e T ()
t) = Doc ann
"Error 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 (T ()) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. E (T ()) -> Doc ann
pretty E (T ())
e) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of 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) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
": arrays of functions are not supported."
    pretty (UT E (T ())
e T ()
t)     = Doc ann
"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) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of 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 (T ()) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. E (T ()) -> Doc ann
pretty E (T ())
e) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"tuples of arrays of tuples are not supported"
    pretty (IS Sh ()
s)       = Doc ann
"𝔯 requires statically known dimensions; inferred 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 ()
s)
    pretty (ES Sh ()
s)       = Doc ann
"👁️ requires statically known dimensions; inferred 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 ()
s)

check :: E (T ()) -> Maybe RE
check = E (T ()) -> Maybe RE
cM

cM :: E (T ()) -> Maybe RE
cM :: E (T ()) -> Maybe RE
cM E (T ())
e | Just T ()
t <- T () -> Maybe (T ())
forall a. T a -> Maybe (T a)
mrT (E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e) = RE -> Maybe RE
forall a. a -> Maybe a
Just (E (T ()) -> T () -> RE
MR E (T ())
e T ()
t)
cM E (T ())
e | Just T ()
t <- T () -> Maybe (T ())
forall a. T a -> Maybe (T a)
flT (E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e) = RE -> Maybe RE
forall a. a -> Maybe a
Just (E (T ()) -> T () -> RE
Unflat E (T ())
e T ()
t)
cM E (T ())
e | Just T ()
t <- T () -> Maybe (T ())
forall a. T a -> Maybe (T a)
ata (E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e) = RE -> Maybe RE
forall a. a -> Maybe a
Just (E (T ()) -> T () -> RE
UT E (T ())
e T ()
t)
cM (Builtin (Arrow T ()
_ (Arrow T ()
_ (Arr Sh ()
sh T ()
_))) Builtin
R) | Sh () -> Bool
forall a. Sh a -> Bool
dynSh Sh ()
sh = RE -> Maybe RE
forall a. a -> Maybe a
Just (Sh () -> RE
IS Sh ()
sh)
cM (Builtin (Arr Sh ()
sh T ()
_) Builtin
Eye) | Sh () -> Bool
forall a. Sh a -> Bool
dynSh Sh ()
sh = RE -> Maybe RE
forall a. a -> Maybe a
Just (Sh () -> RE
ES Sh ()
sh)
cM (Let T ()
_ (Nm (T ())
_, E (T ())
e) E (T ())
e') = E (T ()) -> Maybe RE
cM E (T ())
e Maybe RE -> Maybe RE -> Maybe RE
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> E (T ()) -> Maybe RE
cM E (T ())
e'
cM (LLet T ()
_ (Nm (T ())
_, E (T ())
e) E (T ())
e') = E (T ()) -> Maybe RE
cM E (T ())
e Maybe RE -> Maybe RE -> Maybe RE
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> E (T ()) -> Maybe RE
cM E (T ())
e'
cM (Def T ()
_ (Nm (T ()), E (T ()))
_ E (T ())
e') = E (T ()) -> Maybe RE
cM E (T ())
e' -- FIXME hm
cM (EApp T ()
_ E (T ())
e E (T ())
e') = E (T ()) -> Maybe RE
cM E (T ())
e Maybe RE -> Maybe RE -> Maybe RE
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> E (T ()) -> Maybe RE
cM E (T ())
e'
cM (ALit T ()
_ [E (T ())]
es) = (E (T ()) -> Maybe RE) -> [E (T ())] -> Maybe RE
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Alternative f) =>
(a -> f b) -> t a -> f b
foldMapAlternative E (T ()) -> Maybe RE
cM [E (T ())]
es
cM (Lam T ()
_ Nm (T ())
_ E (T ())
e) = E (T ()) -> Maybe RE
cM E (T ())
e
cM (Cond T ()
_ E (T ())
p E (T ())
e E (T ())
e') = E (T ()) -> Maybe RE
cM E (T ())
p Maybe RE -> Maybe RE -> Maybe RE
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> E (T ()) -> Maybe RE
cM E (T ())
e Maybe RE -> Maybe RE -> Maybe RE
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> E (T ()) -> Maybe RE
cM E (T ())
e'
cM (Tup T ()
_ [E (T ())]
es) = (E (T ()) -> Maybe RE) -> [E (T ())] -> Maybe RE
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Alternative f) =>
(a -> f b) -> t a -> f b
foldMapAlternative E (T ()) -> Maybe RE
cM [E (T ())]
es
cM Builtin{} = Maybe RE
forall a. Maybe a
Nothing
cM ILit{} = Maybe RE
forall a. Maybe a
Nothing
cM FLit{} = Maybe RE
forall a. Maybe a
Nothing
cM BLit{} = Maybe RE
forall a. Maybe a
Nothing
cM Var{} = Maybe RE
forall a. Maybe a
Nothing

mrT :: T a -> Maybe (T a)
mrT :: forall a. T a -> Maybe (T a)
mrT t :: T a
t@TVar{}     = T a -> Maybe (T a)
forall a. a -> Maybe a
Just T a
t
mrT (Arr Sh a
_ T a
t)    = T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
mrT T a
t
mrT (Arrow T a
t T a
t') = T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
mrT T a
t Maybe (T a) -> Maybe (T a) -> Maybe (T a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
mrT T a
t'
mrT (P [T a]
ts)       = (T a -> Maybe (T a)) -> [T a] -> Maybe (T a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Alternative f) =>
(a -> f b) -> t a -> f b
foldMapAlternative T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
mrT [T a]
ts
mrT t :: T a
t@Ρ{}        = T a -> Maybe (T a)
forall a. a -> Maybe a
Just T a
t
mrT T a
_            = Maybe (T a)
forall a. Maybe a
Nothing

flT :: T a -> Maybe (T a)
flT :: forall a. T a -> Maybe (T a)
flT t :: T a
t@(Arr Sh a
_ T a
tϵ) | T a -> Bool
forall a. T a -> Bool
ha T a
tϵ = T a -> Maybe (T a)
forall a. a -> Maybe a
Just T a
t
flT (Arrow T a
t T a
t') = T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
flT T a
t Maybe (T a) -> Maybe (T a) -> Maybe (T a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
flT T a
t'
flT (P [T a]
ts) = (T a -> Maybe (T a)) -> [T a] -> Maybe (T a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Alternative f) =>
(a -> f b) -> t a -> f b
foldMapAlternative T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
flT [T a]
ts
flT T a
_ = Maybe (T a)
forall a. Maybe a
Nothing

ha :: T a -> Bool
ha :: forall a. T a -> Bool
ha Arrow{}   = Bool
True
ha (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
ha [T a]
ts
ha (Arr Sh a
_ T a
t) = T a -> Bool
forall a. T a -> Bool
ha T a
t
ha T a
_         = Bool
False

har :: T a -> Bool
har :: forall a. T a -> Bool
har Arr{} = Bool
True; har (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
har [T a]
ts; har T a
_ = Bool
False

ata :: T a -> Maybe (T a)
ata :: forall a. T a -> Maybe (T a)
ata t :: T a
t@(Arr Sh a
_ (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
har [T a]
ts = T a -> Maybe (T a)
forall a. a -> Maybe a
Just T a
t
ata (Arrow T a
t T a
t') = T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
ata T a
t Maybe (T a) -> Maybe (T a) -> Maybe (T a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
ata T a
t'
ata (P [T a]
t) = (T a -> Maybe (T a)) -> [T a] -> Maybe (T a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Alternative f) =>
(a -> f b) -> t a -> f b
foldMapAlternative T a -> Maybe (T a)
forall a. T a -> Maybe (T a)
ata [T a]
t
ata T a
_ = Maybe (T a)
forall a. Maybe a
Nothing

dynI :: I a -> Bool
dynI :: forall a. I a -> Bool
dynI Ix{}      = Bool
False
dynI IVar{}    = Bool
True
dynI IEVar{}   = Bool
True
dynI StaPlus{} = Bool
True
dynI StaMul{}  = Bool
True

dynSh :: Sh a -> Bool
dynSh :: forall a. Sh a -> Bool
dynSh SVar{}      = Bool
True
dynSh Sh a
Nil         = Bool
False
dynSh (Cons I a
i Sh a
sh) = I a -> Bool
forall a. I a -> Bool
dynI I a
i Bool -> Bool -> Bool
|| Sh a -> Bool
forall a. Sh a -> Bool
dynSh Sh a
sh
dynSh Rev{}       = Bool
True
dynSh Cat{}       = Bool
True
dynSh Π{}         = Bool
True

foldMapAlternative :: (Traversable t, Alternative f) => (a -> f b) -> t a -> f b
foldMapAlternative :: forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Alternative f) =>
(a -> f b) -> t a -> f b
foldMapAlternative a -> f b
f t a
xs = t (f b) -> f b
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum (a -> f b
f (a -> f b) -> t a -> t (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t a
xs)