{-# LANGUAGE CPP
           , DataKinds
           , KindSignatures
           , GADTs
           , ScopedTypeVariables
           , Rank2Types
           , FlexibleContexts
           , PolyKinds
           , ViewPatterns
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.02.23
-- |
-- Module      :  Language.Hakaru.Syntax.TypeOf
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- BUG: can't put this in "Language.Hakaru.Syntax.AST.Sing" because
-- of some sort of cyclic dependency...
----------------------------------------------------------------
module Language.Hakaru.Syntax.TypeOf
    (
    -- * Get singletons for well-typed ABTs
      typeOf
    , typeOfReducer
    -- * Implementation details
    , 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)

----------------------------------------------------------------
----------------------------------------------------------------

-- | Given any well-typed term, produce its type.
--
-- TODO: at present this function may throw errors; in particular,
-- whenever encountering a 'Case_' or 'Superpose_' which is either
-- empty or where all the branches fail. This is considered a bug
-- (since all well-typed terms should be able to produce their
-- types), however it only arises on programs which are (at least
-- partially) undefined or (where defined) are the zero measure,
-- so fixing this is a low priority. When working to correct this
-- bug, it is strongly discouraged to try correcting it by adding
-- singletons to the 'Case_' and 'Superpose_' constructors; since
-- doing so will cause a lot of code to break (and therefore is not
-- a lightweight change), as well as greatly increasing the memory
-- cost for storing ASTs. It would be much better to consider whole
-- programs as being something more than just the AST, thus when
-- trying to get the type of subterms (which should be the only
-- time we ever call this function) we should have access to some
-- sort of context, or intern-table for type singletons, or whatever
-- else makes something a whole program.
--
-- N.B., this is a bit of a hack in order to avoid using 'SingI'
-- or needing to memoize the types of everything. You should really
-- avoid using this function if at all possible since it's very
-- expensive.
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


-- | For private use only.
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) -- cast out phantoms
        (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

-- | This newtype serves two roles. First we add the phantom @xs@
-- so that we can fit this in with the types of 'paraABT'. And
-- second, we wrap up the 'Sing' in a monad for capturing errors,
-- so that we can bring them all the way to the top of the term
-- before deciding whether to throw them or not.
newtype LiftSing (xs :: [Hakaru]) (a :: Hakaru) =
    LiftSing { LiftSing xs a -> Either String (Sing a)
unLiftSing :: Either String (Sing a) }


----------------------------------------------------------------
-- | This is the core of the 'Term'-algebra for computing 'typeOf'.
-- It is exported because it is useful for constructing other
-- 'Term'-algebras for use with 'paraABT'; namely, for callers who
-- need singletons for every subterm while converting an ABT to
-- something else (e.g., pretty printing).
--
-- The @r@ type is whatever it is you're building up via 'paraABT'.
-- The first argument to 'getTermSing' gives some way of projecting
-- a singleton out of @r@ (to avoid the need to map that projection
-- over the term before calling 'getTermSing'). You can then use
-- the resulting singleton for constructing the overall @r@ to be
-- returned.
--
-- If this function returns 'Left', this is considered an error
-- (see the description of 'typeOf'). We pose things in this form
-- (rather than throwing the error immediately) because it enables
-- us to automatically recover from certain error situations.
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 #-}

----------------------------------------------------------------
----------------------------------------------------------- fin.