{-# LANGUAGE CPP
, DataKinds
, KindSignatures
, GADTs
, ScopedTypeVariables
, Rank2Types
, FlexibleContexts
, PolyKinds
, ViewPatterns
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.TypeOf
(
typeOf
, typeOfReducer
, getTermSing
) where
import qualified Data.Foldable as F
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (Applicative(..), (<$>))
#endif
import Language.Hakaru.Syntax.IClasses (Pair2(..), fst2, snd2)
import Language.Hakaru.Syntax.Variable (varType)
import Language.Hakaru.Syntax.ABT (ABT, caseBind, paraABT)
import Language.Hakaru.Types.DataKind (Hakaru())
import Language.Hakaru.Types.HClasses (sing_HSemiring)
import Language.Hakaru.Types.Sing (Sing(..), sUnMeasure, sUnit, sPair)
import Language.Hakaru.Types.Coercion
(singCoerceCod, singCoerceDom, Coerce(..))
import Language.Hakaru.Syntax.Datum (Datum(..), Branch(..))
import Language.Hakaru.Syntax.Reducer
import Language.Hakaru.Syntax.AST (Term(..), SCon(..), SArgs(..)
,typeOfTransform
,getSArgsSing)
import Language.Hakaru.Syntax.AST.Sing
(sing_PrimOp, sing_ArrayOp, sing_MeasureOp, sing_NaryOp, sing_Literal)
typeOf :: (ABT Term abt) => abt '[] a -> Sing a
typeOf :: abt '[] a -> Sing a
typeOf abt '[] a
e0 =
case abt '[] a -> Either String (Sing a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Either String (Sing a)
typeOf_ abt '[] a
e0 of
Left String
err -> String -> Sing a
forall a. HasCallStack => String -> a
error (String -> Sing a) -> String -> Sing a
forall a b. (a -> b) -> a -> b
$ String
"typeOf: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
Right Sing a
typ -> Sing a
typ
typeOf_ :: (ABT Term abt) => abt '[] a -> Either String (Sing a)
typeOf_ :: abt '[] a -> Either String (Sing a)
typeOf_
= LiftSing '[] a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
LiftSing xs a -> Either String (Sing a)
unLiftSing
(LiftSing '[] a -> Either String (Sing a))
-> (abt '[] a -> LiftSing '[] a)
-> abt '[] a
-> Either String (Sing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: Hakaru). Variable a -> LiftSing '[] a)
-> (forall (x :: Hakaru) (xs :: [Hakaru]) (a :: Hakaru).
Variable x -> abt xs a -> LiftSing xs a -> LiftSing (x : xs) a)
-> (forall (a :: Hakaru).
Term (Pair2 abt LiftSing) a -> LiftSing '[] a)
-> forall (xs :: [Hakaru]) (a :: Hakaru). abt xs a -> LiftSing xs a
forall k (abt :: [k] -> k -> *) (syn :: ([k] -> k -> *) -> k -> *)
(r :: [k] -> k -> *).
(ABT syn abt, Functor21 syn) =>
(forall (a :: k). Variable a -> r '[] a)
-> (forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> abt xs a -> r xs a -> r (x : xs) a)
-> (forall (a :: k). syn (Pair2 abt r) a -> r '[] a)
-> forall (xs :: [k]) (a :: k). abt xs a -> r xs a
paraABT
(Either String (Sing a) -> LiftSing '[] a
forall (xs :: [Hakaru]) (a :: Hakaru).
Either String (Sing a) -> LiftSing xs a
LiftSing (Either String (Sing a) -> LiftSing '[] a)
-> (Variable a -> Either String (Sing a))
-> Variable a
-> LiftSing '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> (Variable a -> Sing a) -> Variable a -> Either String (Sing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType)
(\Variable x
_ abt xs a
_ -> Either String (Sing a) -> LiftSing (x : xs) a
forall (xs :: [Hakaru]) (a :: Hakaru).
Either String (Sing a) -> LiftSing xs a
LiftSing (Either String (Sing a) -> LiftSing (x : xs) a)
-> (LiftSing xs a -> Either String (Sing a))
-> LiftSing xs a
-> LiftSing (x : xs) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftSing xs a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
LiftSing xs a -> Either String (Sing a)
unLiftSing)
(Either String (Sing a) -> LiftSing '[] a
forall (xs :: [Hakaru]) (a :: Hakaru).
Either String (Sing a) -> LiftSing xs a
LiftSing (Either String (Sing a) -> LiftSing '[] a)
-> (Term (Pair2 abt LiftSing) a -> Either String (Sing a))
-> Term (Pair2 abt LiftSing) a
-> LiftSing '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (xs :: [Hakaru]) (a :: Hakaru).
LiftSing xs a -> Either String (Sing a))
-> forall (a :: Hakaru).
Term (Pair2 abt LiftSing) a -> Either String (Sing a)
forall (abt :: [Hakaru] -> Hakaru -> *)
(r :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
(forall (xs :: [Hakaru]) (a :: Hakaru).
r xs a -> Either String (Sing a))
-> forall (a :: Hakaru).
Term (Pair2 abt r) a -> Either String (Sing a)
getTermSing forall (xs :: [Hakaru]) (a :: Hakaru).
LiftSing xs a -> Either String (Sing a)
unLiftSing)
typeOfReducer
:: Reducer abt xs a
-> Sing a
typeOfReducer :: Reducer abt xs a -> Sing a
typeOfReducer (Red_Fanout Reducer abt xs a
a Reducer abt xs b
b) = Sing a -> Sing b -> Sing (HPair a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HPair a b)
sPair (Reducer abt xs a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
Reducer abt xs a -> Sing a
typeOfReducer Reducer abt xs a
a) (Reducer abt xs b -> Sing b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
Reducer abt xs a -> Sing a
typeOfReducer Reducer abt xs b
b)
typeOfReducer (Red_Index abt xs 'HNat
_ abt ('HNat : xs) 'HNat
_ Reducer abt ('HNat : xs) a
a) = Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray (Reducer abt ('HNat : xs) a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
Reducer abt xs a -> Sing a
typeOfReducer Reducer abt ('HNat : xs) a
a)
typeOfReducer (Red_Split abt ('HNat : xs) HBool
_ Reducer abt xs a
a Reducer abt xs b
b) = Sing a -> Sing b -> Sing (HPair a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HPair a b)
sPair (Reducer abt xs a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
Reducer abt xs a -> Sing a
typeOfReducer Reducer abt xs a
a) (Reducer abt xs b -> Sing b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
Reducer abt xs a -> Sing a
typeOfReducer Reducer abt xs b
b)
typeOfReducer Reducer abt xs a
Red_Nop = Sing a
Sing HUnit
sUnit
typeOfReducer (Red_Add HSemiring a
h abt ('HNat : xs) a
_) = HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h
newtype LiftSing (xs :: [Hakaru]) (a :: Hakaru) =
LiftSing { LiftSing xs a -> Either String (Sing a)
unLiftSing :: Either String (Sing a) }
getTermSing
:: forall abt r
. (ABT Term abt)
=> (forall xs a. r xs a -> Either String (Sing a))
-> forall a
. Term (Pair2 abt r) a
-> Either String (Sing a)
getTermSing :: (forall (xs :: [Hakaru]) (a :: Hakaru).
r xs a -> Either String (Sing a))
-> forall (a :: Hakaru).
Term (Pair2 abt r) a -> Either String (Sing a)
getTermSing forall (xs :: [Hakaru]) (a :: Hakaru).
r xs a -> Either String (Sing a)
singify = Term (Pair2 abt r) a -> Either String (Sing a)
forall (a :: Hakaru).
Term (Pair2 abt r) a -> Either String (Sing a)
go
where
getSing :: forall xs a. Pair2 abt r xs a -> Either String (Sing a)
getSing :: Pair2 abt r xs a -> Either String (Sing a)
getSing = r xs a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
r xs a -> Either String (Sing a)
singify (r xs a -> Either String (Sing a))
-> (Pair2 abt r xs a -> r xs a)
-> Pair2 abt r xs a
-> Either String (Sing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pair2 abt r xs a -> r xs a
forall k1 k2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (i :: k1)
(j :: k2).
Pair2 a b i j -> b i j
snd2
{-# INLINE getSing #-}
getBranchSing
:: forall a b
. Branch a (Pair2 abt r) b
-> Either String (Sing b)
getBranchSing :: Branch a (Pair2 abt r) b -> Either String (Sing b)
getBranchSing (Branch Pattern xs a
_ Pair2 abt r xs b
e) = Pair2 abt r xs b -> Either String (Sing b)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r xs b
e
{-# INLINE getBranchSing #-}
go :: forall a. Term (Pair2 abt r) a -> Either String (Sing a)
go :: Term (Pair2 abt r) a -> Either String (Sing a)
go (SCon args a
Lam_ :$ Pair2 abt r vars a
r1 :* SArgs (Pair2 abt r) args
End) =
abt '[a] a
-> (Variable a -> abt '[] a -> Either String (Sing (a ':-> a)))
-> Either String (Sing (a ':-> a))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind (Pair2 abt r vars a -> abt vars a
forall k1 k2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (i :: k1)
(j :: k2).
Pair2 a b i j -> a i j
fst2 Pair2 abt r vars a
r1) ((Variable a -> abt '[] a -> Either String (Sing (a ':-> a)))
-> Either String (Sing (a ':-> a)))
-> (Variable a -> abt '[] a -> Either String (Sing (a ':-> a)))
-> Either String (Sing (a ':-> a))
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
_ ->
Sing a -> Sing a -> Sing (a ':-> a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':-> b)
SFun (Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType Variable a
x) (Sing a -> Sing (a ':-> a))
-> Either String (Sing a) -> Either String (Sing (a ':-> a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r1
go (SCon args a
App_ :$ Pair2 abt r vars a
r1 :* Pair2 abt r vars a
_ :* SArgs (Pair2 abt r) args
End) = do
Sing a
typ1 <- Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r1
case Sing a
typ1 of SFun _ typ3 -> Sing b -> Either String (Sing b)
forall (m :: * -> *) a. Monad m => a -> m a
return Sing b
typ3
go (SCon args a
Let_ :$ Pair2 abt r vars a
_ :* Pair2 abt r vars a
r2 :* SArgs (Pair2 abt r) args
End) = Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r2
go (CoerceTo_ Coercion a a
c :$ Pair2 abt r vars a
r1 :* SArgs (Pair2 abt r) args
End) =
Either String (Sing a)
-> (Sing a -> Either String (Sing a))
-> Maybe (Sing a)
-> Either String (Sing a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Coercion a a -> Sing a -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion a a
c (Sing a -> Sing a)
-> Either String (Sing a) -> Either String (Sing a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r1) Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion a a -> Maybe (Sing a)
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Maybe (Sing b)
singCoerceCod Coercion a a
c)
go (UnsafeFrom_ Coercion a b
c :$ Pair2 abt r vars a
r1 :* SArgs (Pair2 abt r) args
End) =
Either String (Sing a)
-> (Sing a -> Either String (Sing a))
-> Maybe (Sing a)
-> Either String (Sing a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Coercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion a b
c (Sing b -> Sing a)
-> Either String (Sing b) -> Either String (Sing a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r1) Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion a b -> Maybe (Sing a)
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion a b
c)
go (PrimOp_ PrimOp typs a
o :$ SArgs (Pair2 abt r) args
_) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> ((List1 Sing typs, Sing a) -> Sing a)
-> (List1 Sing typs, Sing a)
-> Either String (Sing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (List1 Sing typs, Sing a) -> Sing a
forall a b. (a, b) -> b
snd ((List1 Sing typs, Sing a) -> Either String (Sing a))
-> (List1 Sing typs, Sing a) -> Either String (Sing a)
forall a b. (a -> b) -> a -> b
$ PrimOp typs a -> (List1 Sing typs, Sing a)
forall (typs :: [Hakaru]) (a :: Hakaru).
PrimOp typs a -> (List1 Sing typs, Sing a)
sing_PrimOp PrimOp typs a
o
go (ArrayOp_ ArrayOp typs a
o :$ SArgs (Pair2 abt r) args
_) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> ((List1 Sing typs, Sing a) -> Sing a)
-> (List1 Sing typs, Sing a)
-> Either String (Sing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (List1 Sing typs, Sing a) -> Sing a
forall a b. (a, b) -> b
snd ((List1 Sing typs, Sing a) -> Either String (Sing a))
-> (List1 Sing typs, Sing a) -> Either String (Sing a)
forall a b. (a -> b) -> a -> b
$ ArrayOp typs a -> (List1 Sing typs, Sing a)
forall (typs :: [Hakaru]) (a :: Hakaru).
ArrayOp typs a -> (List1 Sing typs, Sing a)
sing_ArrayOp ArrayOp typs a
o
go (MeasureOp_ MeasureOp typs a
o :$ SArgs (Pair2 abt r) args
_) =
Sing ('HMeasure a) -> Either String (Sing ('HMeasure a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing ('HMeasure a) -> Either String (Sing ('HMeasure a)))
-> ((List1 Sing typs, Sing a) -> Sing ('HMeasure a))
-> (List1 Sing typs, Sing a)
-> Either String (Sing ('HMeasure a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Sing ('HMeasure a)
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure (Sing a -> Sing ('HMeasure a))
-> ((List1 Sing typs, Sing a) -> Sing a)
-> (List1 Sing typs, Sing a)
-> Sing ('HMeasure a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (List1 Sing typs, Sing a) -> Sing a
forall a b. (a, b) -> b
snd ((List1 Sing typs, Sing a) -> Either String (Sing ('HMeasure a)))
-> (List1 Sing typs, Sing a) -> Either String (Sing ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ MeasureOp typs a -> (List1 Sing typs, Sing a)
forall (typs :: [Hakaru]) (a :: Hakaru).
MeasureOp typs a -> (List1 Sing typs, Sing a)
sing_MeasureOp MeasureOp typs a
o
go (SCon args a
Dirac :$ Pair2 abt r vars a
r1 :* SArgs (Pair2 abt r) args
End) = Sing a -> Sing ('HMeasure a)
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure (Sing a -> Sing ('HMeasure a))
-> Either String (Sing a) -> Either String (Sing ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r1
go (SCon args a
MBind :$ Pair2 abt r vars a
_ :* Pair2 abt r vars a
r2 :* SArgs (Pair2 abt r) args
End) = Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r2
go (SCon args a
Plate :$ Pair2 abt r vars a
_ :* Pair2 abt r vars a
r2 :* SArgs (Pair2 abt r) args
End) = Sing ('HArray a) -> Sing ('HMeasure ('HArray a))
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure (Sing ('HArray a) -> Sing ('HMeasure ('HArray a)))
-> (Sing ('HMeasure a) -> Sing ('HArray a))
-> Sing ('HMeasure a)
-> Sing ('HMeasure ('HArray a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray (Sing a -> Sing ('HArray a))
-> (Sing ('HMeasure a) -> Sing a)
-> Sing ('HMeasure a)
-> Sing ('HArray a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing ('HMeasure a) -> Sing a
forall (a :: Hakaru). Sing ('HMeasure a) -> Sing a
sUnMeasure (Sing ('HMeasure a) -> Sing ('HMeasure ('HArray a)))
-> Either String (Sing ('HMeasure a))
-> Either String (Sing ('HMeasure ('HArray a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair2 abt r vars a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r vars a
r2
go (SCon args a
Integrate :$ SArgs (Pair2 abt r) args
_) = Sing 'HProb -> Either String (Sing 'HProb)
forall (m :: * -> *) a. Monad m => a -> m a
return Sing 'HProb
SProb
go (Summate HDiscrete a
_ HSemiring a
h :$ SArgs (Pair2 abt r) args
_) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> Sing a -> Either String (Sing a)
forall a b. (a -> b) -> a -> b
$ HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h
go (Product HDiscrete a
_ HSemiring a
h :$ SArgs (Pair2 abt r) args
_) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> Sing a -> Either String (Sing a)
forall a b. (a -> b) -> a -> b
$ HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h
go (Transform_ Transform args a
t :$ SArgs (Pair2 abt r) args
as) =
Transform args a -> SArgsSing args -> Sing a
forall (as :: [([Hakaru], Hakaru)]) (x :: Hakaru).
Transform as x -> SArgsSing as -> Sing x
typeOfTransform Transform args a
t (SArgsSing args -> Sing a)
-> Either String (SArgsSing args) -> Either String (Sing a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a))
-> SArgs (Pair2 abt r) args -> Either String (SArgsSing args)
forall (abt :: [Hakaru] -> Hakaru -> *)
(xs :: [([Hakaru], Hakaru)]) (m :: * -> *).
Applicative m =>
(forall (ys :: [Hakaru]) (a :: Hakaru). abt ys a -> m (Sing a))
-> SArgs abt xs -> m (SArgsSing xs)
getSArgsSing forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing SArgs (Pair2 abt r) args
as
go (NaryOp_ NaryOp a
o Seq (Pair2 abt r '[] a)
_) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> Sing a -> Either String (Sing a)
forall a b. (a -> b) -> a -> b
$ NaryOp a -> Sing a
forall (a :: Hakaru). NaryOp a -> Sing a
sing_NaryOp NaryOp a
o
go (Literal_ Literal a
v) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sing a -> Either String (Sing a))
-> Sing a -> Either String (Sing a)
forall a b. (a -> b) -> a -> b
$ Literal a -> Sing a
forall (a :: Hakaru). Literal a -> Sing a
sing_Literal Literal a
v
go (Empty_ Sing ('HArray a)
typ) = Sing ('HArray a) -> Either String (Sing ('HArray a))
forall (m :: * -> *) a. Monad m => a -> m a
return Sing ('HArray a)
typ
go (Array_ Pair2 abt r '[] 'HNat
_ Pair2 abt r '[ 'HNat] a
r2) = Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray (Sing a -> Sing ('HArray a))
-> Either String (Sing a) -> Either String (Sing ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair2 abt r '[ 'HNat] a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing Pair2 abt r '[ 'HNat] a
r2
go (ArrayLiteral_ [Pair2 abt r '[] a]
es) = Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray (Sing a -> Sing ('HArray a))
-> Either String (Sing a) -> Either String (Sing ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> (Pair2 abt r '[] a -> Either String (Sing a))
-> [Pair2 abt r '[] a]
-> Either String (Sing a)
forall (f :: * -> *) a b.
Foldable f =>
String -> (a -> Either String b) -> f a -> Either String b
tryAll String
"ArrayLiteral_" Pair2 abt r '[] a -> Either String (Sing a)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing [Pair2 abt r '[] a]
es
go (Bucket Pair2 abt r '[] 'HNat
_ Pair2 abt r '[] 'HNat
_ Reducer (Pair2 abt r) '[] a
r) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reducer (Pair2 abt r) '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
Reducer abt xs a -> Sing a
typeOfReducer Reducer (Pair2 abt r) '[] a
r)
go (Datum_ (Datum Text
_ Sing (HData' t)
typ DatumCode (Code t) (Pair2 abt r '[]) (HData' t)
_)) = Sing a -> Either String (Sing a)
forall (m :: * -> *) a. Monad m => a -> m a
return Sing a
Sing (HData' t)
typ
go (Case_ Pair2 abt r '[] a
_ [Branch a (Pair2 abt r) a]
bs) = String
-> (Branch a (Pair2 abt r) a -> Either String (Sing a))
-> [Branch a (Pair2 abt r) a]
-> Either String (Sing a)
forall (f :: * -> *) a b.
Foldable f =>
String -> (a -> Either String b) -> f a -> Either String b
tryAll String
"Case_" Branch a (Pair2 abt r) a -> Either String (Sing a)
forall (a :: Hakaru) (b :: Hakaru).
Branch a (Pair2 abt r) b -> Either String (Sing b)
getBranchSing [Branch a (Pair2 abt r) a]
bs
go (Superpose_ NonEmpty (Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
pes) = String
-> ((Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
-> Either String (Sing ('HMeasure a)))
-> NonEmpty (Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
-> Either String (Sing ('HMeasure a))
forall (f :: * -> *) a b.
Foldable f =>
String -> (a -> Either String b) -> f a -> Either String b
tryAll String
"Superpose_" (Pair2 abt r '[] ('HMeasure a) -> Either String (Sing ('HMeasure a))
forall (xs :: [Hakaru]) (a :: Hakaru).
Pair2 abt r xs a -> Either String (Sing a)
getSing (Pair2 abt r '[] ('HMeasure a)
-> Either String (Sing ('HMeasure a)))
-> ((Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
-> Pair2 abt r '[] ('HMeasure a))
-> (Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
-> Either String (Sing ('HMeasure a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
-> Pair2 abt r '[] ('HMeasure a)
forall a b. (a, b) -> b
snd) NonEmpty (Pair2 abt r '[] 'HProb, Pair2 abt r '[] ('HMeasure a))
pes
go (Reject_ Sing ('HMeasure a)
typ) = Sing ('HMeasure a) -> Either String (Sing ('HMeasure a))
forall (m :: * -> *) a. Monad m => a -> m a
return Sing ('HMeasure a)
typ
go (SCon args a
_ :$ SArgs (Pair2 abt r) args
_) = String -> Either String (Sing a)
forall a. HasCallStack => String -> a
error String
"getTermSing: the impossible happened"
tryAll
:: F.Foldable f
=> String
-> (a -> Either String b)
-> f a
-> Either String b
tryAll :: String -> (a -> Either String b) -> f a -> Either String b
tryAll String
name a -> Either String b
f =
(a -> Either String b -> Either String b)
-> Either String b -> f a -> Either String b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
F.foldr a -> Either String b -> Either String b
step (String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ String
"no unique type for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name)
where
step :: a -> Either String b -> Either String b
step a
x Either String b
rest =
case a -> Either String b
f a
x of
r :: Either String b
r@(Right b
_) -> Either String b
r
Left String
_ -> Either String b
rest
{-# INLINE tryAll #-}