{-# LANGUAGE FlexibleContexts
, GADTs
, ScopedTypeVariables
, DataKinds
, TypeOperators
, OverloadedStrings
, LambdaCase
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.AST.Transforms where
import qualified Data.Sequence as S
import Language.Hakaru.Syntax.ANF (normalize)
import Language.Hakaru.Syntax.CSE (cse)
import Language.Hakaru.Syntax.Prune (prune)
import Language.Hakaru.Syntax.Uniquify (uniquify)
import Language.Hakaru.Syntax.Hoist (hoist)
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Syntax.Prelude (lamWithVar, app)
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Expect (expectInCtx, determineExpect)
import Language.Hakaru.Disintegrate (determine, observeInCtx, disintegrateInCtx)
import Language.Hakaru.Inference (mcmc', mh')
import Language.Hakaru.Maple (sendToMaple, MapleOptions(..)
,defaultMapleOptions, MapleCommand(..)
,MapleException)
import Data.Ratio (numerator, denominator)
import Language.Hakaru.Types.Sing (sing, Sing(..), sUnFun)
import Language.Hakaru.Types.HClasses (HFractional(..))
import Language.Hakaru.Types.Coercion (findCoercion, Coerce(..))
import qualified Data.Sequence as Seq
import Control.Monad.Fix (MonadFix)
import Control.Monad (liftM)
import Control.Monad.Trans (MonadTrans(..))
import Control.Monad.State (StateT(..), evalStateT, put, get, withStateT)
import Control.Applicative (Applicative(..), Alternative(..), (<$>), (<$))
import Data.Functor.Identity (Identity(..))
import Control.Exception (try)
import System.IO (stderr)
import Data.Text.Utf8 (hPutStrLn)
import Data.Text (pack)
import Data.Monoid (Monoid(..), (<>))
import Debug.Trace
optimizations
:: (ABT Term abt)
=> abt '[] a
-> abt '[] a
optimizations :: abt '[] a -> abt '[] a
optimizations = abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
uniquify
(abt '[] a -> abt '[] a)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
prune
(abt '[] a -> abt '[] a)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
cse
(abt '[] a -> abt '[] a)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
hoist
(abt '[] a -> abt '[] a)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
uniquify
(abt '[] a -> abt '[] a)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
normalize
underLam
:: (ABT Term abt, Monad m)
=> (abt '[] b -> m (abt '[] b))
-> abt '[] (a ':-> b)
-> m (abt '[] (a ':-> b))
underLam :: (abt '[] b -> m (abt '[] b))
-> abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
underLam abt '[] b -> m (abt '[] b)
f abt '[] (a ':-> b)
e = abt '[] (a ':-> b)
-> (Variable (a ':-> b) -> m (abt '[] (a ':-> b)))
-> (Term abt (a ':-> b) -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] (a ':-> b)
e (abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] (a ':-> b) -> m (abt '[] (a ':-> b)))
-> (Variable (a ':-> b) -> abt '[] (a ':-> b))
-> Variable (a ':-> b)
-> m (abt '[] (a ':-> b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable (a ':-> b) -> abt '[] (a ':-> b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var) ((Term abt (a ':-> b) -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b)))
-> (Term abt (a ':-> b) -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b))
forall a b. (a -> b) -> a -> b
$ \Term abt (a ':-> b)
t ->
case Term abt (a ':-> b)
t of
SCon args (a ':-> b)
Lam_ :$ abt vars a
e1 :* SArgs abt args
End ->
abt '[a] a
-> (Variable a -> abt '[] a -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b))
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 abt vars a
abt '[a] a
e1 ((Variable a -> abt '[] a -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b)))
-> (Variable a -> abt '[] a -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b))
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e1' -> do
abt '[] b
e1'' <- abt '[] b -> m (abt '[] b)
f abt '[] b
abt '[] a
e1'
abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] (a ':-> b) -> m (abt '[] (a ':-> b)))
-> (Term abt (a ':-> b) -> abt '[] (a ':-> b))
-> Term abt (a ':-> b)
-> m (abt '[] (a ':-> b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term abt (a ':-> b) -> abt '[] (a ':-> b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt (a ':-> b) -> m (abt '[] (a ':-> b)))
-> Term abt (a ':-> b) -> m (abt '[] (a ':-> b))
forall a b. (a -> b) -> a -> b
$
SCon '[ '( '[a], b)] (a ':-> b)
forall (a :: Hakaru) (b :: Hakaru). SCon '[ '( '[a], b)] (a ':-> b)
Lam_ SCon '[ '( '[a], b)] (a ':-> b)
-> SArgs abt '[ '( '[a], b)] -> Term abt (a ':-> b)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ (Variable a -> abt '[] b -> abt '[a] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x abt '[] b
e1'' abt '[a] b -> SArgs abt '[] -> SArgs abt '[ '( '[a], b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
SCon args (a ':-> b)
Let_ :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End ->
case Sing a -> Sing (a ':-> b) -> Maybe (TypeEq a (a ':-> b))
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1) (abt '[] (a ':-> b) -> Sing (a ':-> b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] (a ':-> b)
e) of
Just TypeEq a (a ':-> b)
Refl -> do
abt '[] (a ':-> b)
e1' <- (abt '[] b -> m (abt '[] b))
-> abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (b :: Hakaru)
(a :: Hakaru).
(ABT Term abt, Monad m) =>
(abt '[] b -> m (abt '[] b))
-> abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
underLam abt '[] b -> m (abt '[] b)
f abt vars a
abt '[] (a ':-> b)
e1
abt '[] a -> m (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] a -> m (abt '[] a))
-> (Term abt a -> abt '[] a) -> Term abt a -> m (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt a -> m (abt '[] a)) -> Term abt a -> m (abt '[] a)
forall a b. (a -> b) -> a -> b
$
SCon '[LC (a ':-> b), '( '[ a ':-> b], a)] a
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC (a ':-> b), '( '[ a ':-> b], a)] a
-> SArgs abt '[LC (a ':-> b), '( '[ a ':-> b], a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] (a ':-> b)
e1' abt '[] (a ':-> b)
-> SArgs abt '[ '(vars, a)]
-> SArgs abt '[LC (a ':-> b), '(vars, a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt vars a
e2 abt vars a -> SArgs abt '[] -> SArgs abt '[ '(vars, a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
Maybe (TypeEq a (a ':-> b))
Nothing -> abt '[a] a
-> (Variable a -> abt '[] a -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b))
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 abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b)))
-> (Variable a -> abt '[] a -> m (abt '[] (a ':-> b)))
-> m (abt '[] (a ':-> b))
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' -> do
abt '[] (a ':-> b)
e2'' <- (abt '[] b -> m (abt '[] b))
-> abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (b :: Hakaru)
(a :: Hakaru).
(ABT Term abt, Monad m) =>
(abt '[] b -> m (abt '[] b))
-> abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
underLam abt '[] b -> m (abt '[] b)
f abt '[] a
abt '[] (a ':-> b)
e2'
abt '[] (a ':-> b) -> m (abt '[] (a ':-> b))
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] (a ':-> b) -> m (abt '[] (a ':-> b)))
-> (Term abt (a ':-> b) -> abt '[] (a ':-> b))
-> Term abt (a ':-> b)
-> m (abt '[] (a ':-> b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term abt (a ':-> b) -> abt '[] (a ':-> b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt (a ':-> b) -> m (abt '[] (a ':-> b)))
-> Term abt (a ':-> b) -> m (abt '[] (a ':-> b))
forall a b. (a -> b) -> a -> b
$
SCon '[LC a, '( '[a], a ':-> b)] (a ':-> b)
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], a ':-> b)] (a ':-> b)
-> SArgs abt '[LC a, '( '[a], a ':-> b)] -> Term abt (a ':-> b)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt vars a
e1 abt vars a
-> SArgs abt '[ '( '[a], a ':-> b)]
-> SArgs abt '[ '(vars, a), '( '[a], a ':-> b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* (Variable a -> abt '[] (a ':-> b) -> abt '[a] (a ':-> b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x abt '[] (a ':-> b)
e2'') abt '[a] (a ':-> b)
-> SArgs abt '[] -> SArgs abt '[ '( '[a], a ':-> b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
Term abt (a ':-> b)
_ -> [Char] -> m (abt '[] (a ':-> b))
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: underLam"
underLam'
:: forall abt m a b b'
. (ABT Term abt, MonadFix m)
=> (abt '[] b -> m (abt '[] b'))
-> abt '[] (a ':-> b)
-> m (abt '[] (a ':-> b'))
underLam' :: (abt '[] b -> m (abt '[] b'))
-> abt '[] (a ':-> b) -> m (abt '[] (a ':-> b'))
underLam' abt '[] b -> m (abt '[] b')
f abt '[] (a ':-> b)
e = do
abt '[] b -> abt '[] b'
f' <- [Char]
-> m (abt '[] b -> abt '[] b') -> m (abt '[] b -> abt '[] b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': build function" (m (abt '[] b -> abt '[] b') -> m (abt '[] b -> abt '[] b'))
-> m (abt '[] b -> abt '[] b') -> m (abt '[] b -> abt '[] b')
forall a b. (a -> b) -> a -> b
$
(abt '[b] b' -> abt '[] b -> abt '[] b')
-> m (abt '[b] b') -> m (abt '[] b -> abt '[] b')
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\abt '[b] b'
f' abt '[] b
b -> abt '[] (b ':-> b') -> abt '[] b -> abt '[] b'
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app (Term abt (b ':-> b') -> abt '[] (b ':-> b')
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt (b ':-> b') -> abt '[] (b ':-> b'))
-> Term abt (b ':-> b') -> abt '[] (b ':-> b')
forall a b. (a -> b) -> a -> b
$ SCon '[ '( '[b], b')] (b ':-> b')
forall (a :: Hakaru) (b :: Hakaru). SCon '[ '( '[a], b)] (a ':-> b)
Lam_ SCon '[ '( '[b], b')] (b ':-> b')
-> SArgs abt '[ '( '[b], b')] -> Term abt (b ':-> b')
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[b] b'
f' abt '[b] b' -> SArgs abt '[] -> SArgs abt '[ '( '[b], b')]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End) abt '[] b
b) (m (abt '[b] b') -> m (abt '[] b -> abt '[] b'))
-> m (abt '[b] b') -> m (abt '[] b -> abt '[] b')
forall a b. (a -> b) -> a -> b
$
Text -> Sing b -> (abt '[] b -> m (abt '[] b')) -> m (abt '[b] b')
forall a1 (m :: * -> *) (syn :: ([a1] -> a1 -> *) -> a1 -> *)
(abt :: [a1] -> a1 -> *) (a2 :: a1) (xs :: [a1]) (b :: a1).
(MonadFix m, ABT syn abt) =>
Text
-> Sing a2 -> (abt '[] a2 -> m (abt xs b)) -> m (abt (a2 : xs) b)
binderM Text
"" ((Sing a, Sing b) -> Sing b
forall a b. (a, b) -> b
snd ((Sing a, Sing b) -> Sing b) -> (Sing a, Sing b) -> Sing b
forall a b. (a -> b) -> a -> b
$ Sing (a ':-> b) -> (Sing a, Sing b)
forall (a :: Hakaru) (b :: Hakaru).
Sing (a ':-> b) -> (Sing a, Sing b)
sUnFun (Sing (a ':-> b) -> (Sing a, Sing b))
-> Sing (a ':-> b) -> (Sing a, Sing b)
forall a b. (a -> b) -> a -> b
$ abt '[] (a ':-> b) -> Sing (a ':-> b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] (a ':-> b)
e) abt '[] b -> m (abt '[] b')
f
abt '[] (a ':-> b') -> m (abt '[] (a ':-> b'))
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] (a ':-> b') -> m (abt '[] (a ':-> b')))
-> abt '[] (a ':-> b') -> m (abt '[] (a ':-> b'))
forall a b. (a -> b) -> a -> b
$ (abt '[] b -> abt '[] b')
-> abt '[] (a ':-> b) -> abt '[] (a ':-> b')
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(b' :: Hakaru).
ABT Term abt =>
(abt '[] b -> abt '[] b')
-> abt '[] (a ':-> b) -> abt '[] (a ':-> b')
underLam'p abt '[] b -> abt '[] b'
f' abt '[] (a ':-> b)
e
underLam'p
:: forall abt a b b'
. (ABT Term abt)
=> (abt '[] b -> abt '[] b')
-> abt '[] (a ':-> b)
-> abt '[] (a ':-> b')
underLam'p :: (abt '[] b -> abt '[] b')
-> abt '[] (a ':-> b) -> abt '[] (a ':-> b')
underLam'p abt '[] b -> abt '[] b'
f abt '[] (a ':-> b)
e =
let var_ :: Variable (a ':-> b) -> abt '[] (a ':-> b')
var_ :: Variable (a ':-> b) -> abt '[] (a ':-> b')
var_ Variable (a ':-> b)
v_ab = [Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': entered var" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
Text -> Sing a -> (abt '[] a -> abt '[] b') -> abt '[] (a ':-> b')
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Text -> Sing a -> (abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
lamWithVar Text
"" ((Sing a, Sing b) -> Sing a
forall a b. (a, b) -> a
fst ((Sing a, Sing b) -> Sing a) -> (Sing a, Sing b) -> Sing a
forall a b. (a -> b) -> a -> b
$ Sing (a ':-> b) -> (Sing a, Sing b)
forall (a :: Hakaru) (b :: Hakaru).
Sing (a ':-> b) -> (Sing a, Sing b)
sUnFun (Sing (a ':-> b) -> (Sing a, Sing b))
-> Sing (a ':-> b) -> (Sing a, Sing b)
forall a b. (a -> b) -> a -> b
$ Variable (a ':-> b) -> Sing (a ':-> b)
forall k (a :: k). Variable a -> Sing a
varType Variable (a ':-> b)
v_ab) ((abt '[] a -> abt '[] b') -> abt '[] (a ':-> b'))
-> (abt '[] a -> abt '[] b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$ \abt '[] a
a ->
[Char] -> abt '[] b' -> abt '[] b'
forall a. [Char] -> a -> a
trace [Char]
"underLam': applied function" (abt '[] b' -> abt '[] b') -> abt '[] b' -> abt '[] b'
forall a b. (a -> b) -> a -> b
$ abt '[] b -> abt '[] b'
f (abt '[] b -> abt '[] b') -> abt '[] b -> abt '[] b'
forall a b. (a -> b) -> a -> b
$ abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app (Variable (a ':-> b) -> abt '[] (a ':-> b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable (a ':-> b)
v_ab) abt '[] a
a
syn_ :: Term abt (a ':-> b) -> abt '[] (a ':-> b')
syn_ Term abt (a ':-> b)
t = [Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': entered syn" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
case Term abt (a ':-> b)
t of
SCon args (a ':-> b)
Lam_ :$ abt vars a
e1 :* SArgs abt args
End -> [Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': entered syn/Lam_" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
abt '[a] a
-> (Variable a -> abt '[] a -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b')
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 abt vars a
abt '[a] a
e1 ((Variable a -> abt '[] a -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b'))
-> (Variable a -> abt '[] a -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e1' ->
[Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': rebuilt Lam_" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
Term abt (a ':-> b') -> abt '[] (a ':-> b')
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt (a ':-> b') -> abt '[] (a ':-> b'))
-> Term abt (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$ SCon '[ '( '[a], b')] (a ':-> b')
forall (a :: Hakaru) (b :: Hakaru). SCon '[ '( '[a], b)] (a ':-> b)
Lam_ SCon '[ '( '[a], b')] (a ':-> b')
-> SArgs abt '[ '( '[a], b')] -> Term abt (a ':-> b')
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$
([Char] -> abt '[a] b' -> abt '[a] b'
forall a. [Char] -> a -> a
trace [Char]
"underLam': applied bind{Lam_}" (abt '[a] b' -> abt '[a] b') -> abt '[a] b' -> abt '[a] b'
forall a b. (a -> b) -> a -> b
$
Variable a -> abt '[] b' -> abt '[a] b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x ([Char] -> abt '[] b' -> abt '[] b'
forall a. [Char] -> a -> a
trace [Char]
"underLam': applied function{Lam_}"
(abt '[] b' -> abt '[] b') -> abt '[] b' -> abt '[] b'
forall a b. (a -> b) -> a -> b
$ abt '[] b -> abt '[] b'
f abt '[] b
abt '[] a
e1')) abt '[a] b' -> SArgs abt '[] -> SArgs abt '[ '( '[a], b')]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
SCon args (a ':-> b)
Let_ :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> [Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': entered syn/Lam_" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
abt '[a] a
-> (Variable a -> abt '[] a -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b')
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 abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b'))
-> (Variable a -> abt '[] a -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' ->
[Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': rebuilt Let_" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
Term abt (a ':-> b') -> abt '[] (a ':-> b')
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt (a ':-> b') -> abt '[] (a ':-> b'))
-> Term abt (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$ SCon '[LC a, '( '[a], a ':-> b')] (a ':-> b')
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], a ':-> b')] (a ':-> b')
-> SArgs abt '[LC a, '( '[a], a ':-> b')] -> Term abt (a ':-> b')
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt vars a
e1 abt vars a
-> SArgs abt '[ '( '[a], a ':-> b')]
-> SArgs abt '[ '(vars, a), '( '[a], a ':-> b')]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:*
([Char] -> abt '[a] (a ':-> b') -> abt '[a] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': applied bind{Lam_}" (abt '[a] (a ':-> b') -> abt '[a] (a ':-> b'))
-> abt '[a] (a ':-> b') -> abt '[a] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
Variable a -> abt '[] (a ':-> b') -> abt '[a] (a ':-> b')
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x ([Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': recursive case{Let_}" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
abt '[] (a ':-> b) -> abt '[] (a ':-> b')
go abt '[] a
abt '[] (a ':-> b)
e2')) abt '[a] (a ':-> b')
-> SArgs abt '[] -> SArgs abt '[ '( '[a], a ':-> b')]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
Term abt (a ':-> b)
_ -> [Char] -> abt '[] (a ':-> b')
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: underLam'"
go :: abt '[] (a ':-> b) -> abt '[] (a ':-> b')
go abt '[] (a ':-> b)
e' = [Char] -> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a. [Char] -> a -> a
trace [Char]
"underLam': entered main body" (abt '[] (a ':-> b') -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b') -> abt '[] (a ':-> b')
forall a b. (a -> b) -> a -> b
$
abt '[] (a ':-> b)
-> (Variable (a ':-> b) -> abt '[] (a ':-> b'))
-> (Term abt (a ':-> b) -> abt '[] (a ':-> b'))
-> abt '[] (a ':-> b')
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] (a ':-> b)
e' Variable (a ':-> b) -> abt '[] (a ':-> b')
var_ Term abt (a ':-> b) -> abt '[] (a ':-> b')
syn_
in abt '[] (a ':-> b) -> abt '[] (a ':-> b')
go abt '[] (a ':-> b)
e
expandTransformations
:: forall abt a
. (ABT Term abt)
=> abt '[] a -> abt '[] a
expandTransformations :: abt '[] a -> abt '[] a
expandTransformations =
TransformTable abt Identity -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformTable abt Identity -> abt '[] a -> abt '[] a
expandTransformationsWith' TransformTable abt Identity
forall (m :: * -> *) (abt :: [Hakaru] -> Hakaru -> *).
(Applicative m, ABT Term abt) =>
TransformTable abt m
haskellTransformations
expandAllTransformations
:: forall abt a
. (ABT Term abt)
=> abt '[] a -> IO (abt '[] a)
expandAllTransformations :: abt '[] a -> IO (abt '[] a)
expandAllTransformations =
TransformTable abt IO -> abt '[] a -> IO (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(m :: * -> *).
(ABT Term abt, Applicative m, Monad m) =>
TransformTable abt m -> abt '[] a -> m (abt '[] a)
expandTransformationsWith TransformTable abt IO
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
TransformTable abt IO
allTransformations
expandTransformationsWith'
:: forall abt a
. (ABT Term abt)
=> TransformTable abt Identity
-> abt '[] a -> abt '[] a
expandTransformationsWith' :: TransformTable abt Identity -> abt '[] a -> abt '[] a
expandTransformationsWith' TransformTable abt Identity
tbl =
Identity (abt '[] a) -> abt '[] a
forall a. Identity a -> a
runIdentity (Identity (abt '[] a) -> abt '[] a)
-> (abt '[] a -> Identity (abt '[] a)) -> abt '[] a -> abt '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransformTable abt Identity -> abt '[] a -> Identity (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(m :: * -> *).
(ABT Term abt, Applicative m, Monad m) =>
TransformTable abt m -> abt '[] a -> m (abt '[] a)
expandTransformationsWith TransformTable abt Identity
tbl
type TransformM = StateT TransformCtx
expandTransformationsWith
:: forall abt a m
. (ABT Term abt, Applicative m, Monad m)
=> TransformTable abt m
-> abt '[] a -> m (abt '[] a)
expandTransformationsWith :: TransformTable abt m -> abt '[] a -> m (abt '[] a)
expandTransformationsWith TransformTable abt m
tbl abt '[] a
t0 =
(StateT TransformCtx m (abt '[] a)
-> TransformCtx -> m (abt '[] a))
-> TransformCtx
-> StateT TransformCtx m (abt '[] a)
-> m (abt '[] a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT TransformCtx m (abt '[] a) -> TransformCtx -> m (abt '[] a)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (TransformCtx
forall a. Monoid a => a
mempty {nextFreeVar :: Nat
nextFreeVar = abt '[] a -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind abt '[] a
t0}) (StateT TransformCtx m (abt '[] a) -> m (abt '[] a))
-> (abt '[] a -> StateT TransformCtx m (abt '[] a))
-> abt '[] a
-> m (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(forall (a :: Hakaru).
Variable a -> StateT TransformCtx m (abt '[] a))
-> (forall (x :: Hakaru) (xs :: [Hakaru]) (a :: Hakaru).
Variable x
-> StateT TransformCtx m (abt xs a)
-> StateT TransformCtx m (abt (x : xs) a))
-> (forall (a :: Hakaru).
StateT TransformCtx m (Term abt a)
-> StateT TransformCtx m (abt '[] a))
-> forall (xs :: [Hakaru]) (a :: Hakaru).
abt xs a -> StateT TransformCtx m (abt xs a)
forall k (abt :: [k] -> k -> *) (syn :: ([k] -> k -> *) -> k -> *)
(r :: [k] -> k -> *) (f :: * -> *).
(ABT syn abt, Traversable21 syn, Applicative f) =>
(forall (a :: k). Variable a -> f (r '[] a))
-> (forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> f (r xs a) -> f (r (x : xs) a))
-> (forall (a :: k). f (syn r a) -> f (r '[] a))
-> forall (xs :: [k]) (a :: k). abt xs a -> f (r xs a)
cataABTM (abt '[] a -> StateT TransformCtx m (abt '[] a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (abt '[] a -> StateT TransformCtx m (abt '[] a))
-> (Variable a -> abt '[] a)
-> Variable a
-> StateT TransformCtx m (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var) forall (x :: Hakaru) (xs :: [Hakaru]) (a :: Hakaru).
Variable x
-> StateT TransformCtx m (abt xs a)
-> StateT TransformCtx m (abt (x : xs) a)
bind_ (StateT TransformCtx m (Term abt a)
-> (Term abt a -> StateT TransformCtx m (abt '[] a))
-> StateT TransformCtx m (abt '[] a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term abt a -> StateT TransformCtx m (abt '[] a)
forall (b :: Hakaru). Term abt b -> TransformM m (abt '[] b)
syn_) (abt '[] a -> m (abt '[] a)) -> abt '[] a -> m (abt '[] a)
forall a b. (a -> b) -> a -> b
$ abt '[] a
t0
where
bind_ :: forall x xs b
. Variable x
-> TransformM m (abt xs b)
-> TransformM m (abt (x ': xs) b)
bind_ :: Variable x
-> TransformM m (abt xs b) -> TransformM m (abt (x : xs) b)
bind_ Variable x
v TransformM m (abt xs b)
mt = Variable x -> abt xs b -> abt (x : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable x
v (abt xs b -> abt (x : xs) b)
-> TransformM m (abt xs b) -> TransformM m (abt (x : xs) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TransformCtx -> TransformCtx)
-> TransformM m (abt xs b) -> TransformM m (abt xs b)
forall s (m :: * -> *) a. (s -> s) -> StateT s m a -> StateT s m a
withStateT (Variable x -> TransformCtx
forall x. HasTransformCtx x => x -> TransformCtx
ctxOf Variable x
v TransformCtx -> TransformCtx -> TransformCtx
forall a. Semigroup a => a -> a -> a
<>) TransformM m (abt xs b)
mt
syn_ :: forall b. Term abt b -> TransformM m (abt '[] b)
syn_ :: Term abt b -> TransformM m (abt '[] b)
syn_ Term abt b
t =
case Term abt b
t of
Transform_ Transform args b
tr :$ SArgs abt args
as ->
StateT TransformCtx m TransformCtx
forall s (m :: * -> *). MonadState s m => m s
get StateT TransformCtx m TransformCtx
-> (TransformCtx -> TransformM m (abt '[] b))
-> TransformM m (abt '[] b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TransformCtx
ctx ->
TransformM m (abt '[] b)
-> (abt '[] b -> TransformM m (abt '[] b))
-> Maybe (abt '[] b)
-> TransformM m (abt '[] b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (abt '[] b -> TransformM m (abt '[] b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (abt '[] b -> TransformM m (abt '[] b))
-> abt '[] b -> TransformM m (abt '[] b)
forall a b. (a -> b) -> a -> b
$ Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt b
t)
(\abt '[] b
r -> abt '[] b
r abt '[] b -> StateT TransformCtx m () -> TransformM m (abt '[] b)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TransformCtx -> StateT TransformCtx m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (abt '[] b -> TransformCtx
forall x. HasTransformCtx x => x -> TransformCtx
ctxOf abt '[] b
r TransformCtx -> TransformCtx -> TransformCtx
forall a. Semigroup a => a -> a -> a
<> TransformCtx
ctx))
(Maybe (abt '[] b) -> TransformM m (abt '[] b))
-> StateT TransformCtx m (Maybe (abt '[] b))
-> TransformM m (abt '[] b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (Maybe (abt '[] b)) -> StateT TransformCtx m (Maybe (abt '[] b))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TransformTable abt m
-> Transform args b
-> TransformCtx
-> SArgs abt args
-> m (Maybe (abt '[] b))
forall (m :: * -> *) (abt :: [Hakaru] -> Hakaru -> *)
(as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Applicative m =>
TransformTable abt m
-> Transform as b
-> TransformCtx
-> SArgs abt as
-> m (Maybe (abt '[] b))
lookupTransform' TransformTable abt m
tbl Transform args b
tr TransformCtx
ctx SArgs abt args
as)
Term abt b
_ -> abt '[] b -> TransformM m (abt '[] b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (abt '[] b -> TransformM m (abt '[] b))
-> abt '[] b -> TransformM m (abt '[] b)
forall a b. (a -> b) -> a -> b
$ Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt b
t
mapleTransformationsWithOpts
:: forall abt
. ABT Term abt
=> MapleOptions ()
-> TransformTable abt IO
mapleTransformationsWithOpts :: MapleOptions () -> TransformTable abt IO
mapleTransformationsWithOpts MapleOptions ()
opts = (forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> TransformTable abt IO
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *).
(forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> m (Maybe (abt '[] b))))
-> TransformTable abt m
TransformTable ((forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> TransformTable abt IO)
-> (forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> TransformTable abt IO
forall a b. (a -> b) -> a -> b
$ \Transform as b
tr ->
let cmd :: Transform '[LC i] o
-> TransformCtx -> abt '[] i -> IO (Maybe (abt '[] o))
cmd Transform '[LC i] o
c TransformCtx
ctx abt '[] i
x =
IO (abt '[] o) -> IO (Either MapleException (abt '[] o))
forall e a. Exception e => IO a -> IO (Either e a)
try (MapleOptions (MapleCommand i o) -> abt '[] i -> IO (abt '[] o)
forall (abt :: [Hakaru] -> Hakaru -> *) (i :: Hakaru)
(o :: Hakaru).
ABT Term abt =>
MapleOptions (MapleCommand i o) -> abt '[] i -> IO (abt '[] o)
sendToMaple MapleOptions ()
opts{command :: MapleCommand i o
command=Transform '[LC i] o -> MapleCommand i o
forall (i :: Hakaru) (o :: Hakaru).
Transform '[ '( '[], i)] o -> MapleCommand i o
MapleCommand Transform '[LC i] o
c
,context :: TransformCtx
context=TransformCtx
ctx} abt '[] i
x) IO (Either MapleException (abt '[] o))
-> (Either MapleException (abt '[] o) -> IO (Maybe (abt '[] o)))
-> IO (Maybe (abt '[] o))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\case
Left (MapleException
err :: MapleException) ->
Handle -> Text -> IO ()
hPutStrLn Handle
stderr ([Char] -> Text
pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ MapleException -> [Char]
forall a. Show a => a -> [Char]
show MapleException
err) IO () -> IO (Maybe (abt '[] o)) -> IO (Maybe (abt '[] o))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (abt '[] o) -> IO (Maybe (abt '[] o))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (abt '[] o)
forall a. Maybe a
Nothing
Right abt '[] o
r ->
Maybe (abt '[] o) -> IO (Maybe (abt '[] o))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (abt '[] o) -> IO (Maybe (abt '[] o)))
-> Maybe (abt '[] o) -> IO (Maybe (abt '[] o))
forall a b. (a -> b) -> a -> b
$ abt '[] o -> Maybe (abt '[] o)
forall a. a -> Maybe a
Just abt '[] o
r
cmd :: Transform '[LC i] o -> TransformCtx
-> abt '[] i -> IO (Maybe (abt '[] o)) in
case Transform as b
tr of
Transform as b
Simplify ->
(TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case { abt vars a
e1 :* SArgs abt args
End -> Transform '[LC a] b
-> TransformCtx -> abt '[] a -> IO (Maybe (abt '[] b))
forall (i :: Hakaru) (o :: Hakaru).
Transform '[LC i] o
-> TransformCtx -> abt '[] i -> IO (Maybe (abt '[] o))
cmd Transform as b
Transform '[LC a] b
tr TransformCtx
ctx abt vars a
abt '[] a
e1 }
Transform as b
Summarize ->
(TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case { abt vars a
e1 :* SArgs abt args
End -> Transform '[LC a] b
-> TransformCtx -> abt '[] a -> IO (Maybe (abt '[] b))
forall (i :: Hakaru) (o :: Hakaru).
Transform '[LC i] o
-> TransformCtx -> abt '[] i -> IO (Maybe (abt '[] o))
cmd Transform as b
Transform '[LC a] b
tr TransformCtx
ctx abt vars a
abt '[] a
e1 }
Transform as b
Reparam ->
(TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case { abt vars a
e1 :* SArgs abt args
End -> Transform '[LC a] b
-> TransformCtx -> abt '[] a -> IO (Maybe (abt '[] b))
forall (i :: Hakaru) (o :: Hakaru).
Transform '[LC i] o
-> TransformCtx -> abt '[] i -> IO (Maybe (abt '[] o))
cmd Transform as b
Transform '[LC a] b
tr TransformCtx
ctx abt vars a
abt '[] a
e1 }
Disint TransformImpl
InMaple ->
(TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b))))
-> (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
-> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case { abt vars a
e1 :* SArgs abt args
End -> Transform '[LC a] b
-> TransformCtx -> abt '[] a -> IO (Maybe (abt '[] b))
forall (i :: Hakaru) (o :: Hakaru).
Transform '[LC i] o
-> TransformCtx -> abt '[] i -> IO (Maybe (abt '[] o))
cmd Transform as b
Transform '[LC a] b
tr TransformCtx
ctx abt vars a
abt '[] a
e1 }
Transform as b
_ -> Maybe (TransformCtx -> SArgs abt as -> IO (Maybe (abt '[] b)))
forall a. Maybe a
Nothing
mapleTransformations
:: ABT Term abt
=> TransformTable abt IO
mapleTransformations :: TransformTable abt IO
mapleTransformations = MapleOptions () -> TransformTable abt IO
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
MapleOptions () -> TransformTable abt IO
mapleTransformationsWithOpts MapleOptions ()
defaultMapleOptions
haskellTransformations :: (Applicative m, ABT Term abt) => TransformTable abt m
haskellTransformations :: TransformTable abt m
haskellTransformations = (forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> TransformTable abt m
forall (m :: * -> *) (abt :: [Hakaru] -> Hakaru -> *).
Applicative m =>
(forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> TransformTable abt m
simpleTable ((forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> TransformTable abt m)
-> (forall (as :: [([Hakaru], Hakaru)]) (b :: Hakaru).
Transform as b
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> TransformTable abt m
forall a b. (a -> b) -> a -> b
$ \Transform as b
tr ->
case Transform as b
tr of
Transform as b
Expect ->
(TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case
abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> abt '[] 'HProb -> Maybe (abt '[] 'HProb)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> Maybe (abt '[] 'HProb)
determineExpect (abt '[] 'HProb -> Maybe (abt '[] 'HProb))
-> abt '[] 'HProb -> Maybe (abt '[] 'HProb)
forall a b. (a -> b) -> a -> b
$ TransformCtx
-> abt '[] ('HMeasure a) -> abt '[a] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] ('HMeasure a) -> abt '[a] 'HProb -> abt '[] 'HProb
expectInCtx TransformCtx
ctx abt vars a
abt '[] ('HMeasure a)
e1 abt vars a
abt '[a] 'HProb
e2
Transform as b
Observe ->
(TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case
abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> [abt '[] ('HMeasure a)] -> Maybe (abt '[] ('HMeasure a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] ('HMeasure a)] -> Maybe (abt '[] ('HMeasure a)))
-> [abt '[] ('HMeasure a)] -> Maybe (abt '[] ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ TransformCtx
-> abt '[] ('HMeasure a) -> abt '[] a -> [abt '[] ('HMeasure a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] ('HMeasure a) -> abt '[] a -> [abt '[] ('HMeasure a)]
observeInCtx TransformCtx
ctx abt vars a
abt '[] ('HMeasure a)
e1 abt vars a
abt '[] a
e2
Transform as b
MCMC ->
(TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case
abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure a))
mcmc' TransformCtx
ctx abt vars a
abt '[] (a ':-> 'HMeasure a)
e1 abt vars a
abt '[] ('HMeasure a)
e2
Transform as b
MH ->
(TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case
abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
mh' TransformCtx
ctx abt vars a
abt '[] (a ':-> 'HMeasure a)
e1 abt vars a
abt '[] ('HMeasure a)
e2
Disint TransformImpl
InHaskell ->
(TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a. a -> Maybe a
Just ((TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b)))
-> (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
-> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a b. (a -> b) -> a -> b
$ \TransformCtx
ctx -> \case
abt vars a
e1 :* SArgs abt args
End -> [abt '[] (a ':-> 'HMeasure b)]
-> Maybe (abt '[] (a ':-> 'HMeasure b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (a ':-> 'HMeasure b)]
-> Maybe (abt '[] (a ':-> 'HMeasure b)))
-> [abt '[] (a ':-> 'HMeasure b)]
-> Maybe (abt '[] (a ':-> 'HMeasure b))
forall a b. (a -> b) -> a -> b
$ TransformCtx
-> abt '[] ('HMeasure (HPair a b))
-> [abt '[] (a ':-> 'HMeasure b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] ('HMeasure (HPair a b))
-> [abt '[] (a ':-> 'HMeasure b)]
disintegrateInCtx TransformCtx
ctx abt vars a
abt '[] ('HMeasure (HPair a b))
e1
Transform as b
_ -> Maybe (TransformCtx -> SArgs abt as -> Maybe (abt '[] b))
forall a. Maybe a
Nothing
allTransformationsWithMOpts
:: ABT Term abt
=> MapleOptions ()
-> TransformTable abt IO
allTransformationsWithMOpts :: MapleOptions () -> TransformTable abt IO
allTransformationsWithMOpts MapleOptions ()
opts = TransformTable abt IO
-> TransformTable abt IO -> TransformTable abt IO
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *).
TransformTable abt m
-> TransformTable abt m -> TransformTable abt m
unionTable
(MapleOptions () -> TransformTable abt IO
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
MapleOptions () -> TransformTable abt IO
mapleTransformationsWithOpts MapleOptions ()
opts)
TransformTable abt IO
forall (m :: * -> *) (abt :: [Hakaru] -> Hakaru -> *).
(Applicative m, ABT Term abt) =>
TransformTable abt m
haskellTransformations
allTransformations :: ABT Term abt => TransformTable abt IO
allTransformations :: TransformTable abt IO
allTransformations = MapleOptions () -> TransformTable abt IO
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
MapleOptions () -> TransformTable abt IO
allTransformationsWithMOpts MapleOptions ()
defaultMapleOptions
coalesce
:: forall abt a
. (ABT Term abt)
=> abt '[] a
-> abt '[] a
coalesce :: abt '[] a -> abt '[] a
coalesce abt '[] a
abt = abt '[] a
-> (Variable a -> abt '[] a)
-> (Term abt a -> abt '[] a)
-> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
abt Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Term abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Term abt a -> abt '[] a
onNaryOps
where onNaryOps :: Term abt a -> abt '[] a
onNaryOps (NaryOp_ NaryOp a
t Seq (abt '[] a)
es) = Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt a -> abt '[] a) -> Term abt a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ NaryOp a -> Seq (abt '[] a) -> Term abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
NaryOp a -> Seq (abt '[] a) -> Term abt a
NaryOp_ NaryOp a
t (NaryOp a -> Seq (abt '[] a) -> Seq (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NaryOp a -> Seq (abt '[] a) -> Seq (abt '[] a)
coalesceNaryOp NaryOp a
t Seq (abt '[] a)
es)
onNaryOps Term abt a
term = Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt a
term
coalesceNaryOp
:: ABT Term abt
=> NaryOp a
-> S.Seq (abt '[] a)
-> S.Seq (abt '[] a)
coalesceNaryOp :: NaryOp a -> Seq (abt '[] a) -> Seq (abt '[] a)
coalesceNaryOp NaryOp a
typ Seq (abt '[] a)
args =
do abt '[] a
abt <- Seq (abt '[] a)
args
case abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
abt of
Syn (NaryOp_ typ' args') ->
if NaryOp a
typ NaryOp a -> NaryOp a -> Bool
forall a. Eq a => a -> a -> Bool
== NaryOp a
typ'
then NaryOp a -> Seq (abt '[] a) -> Seq (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NaryOp a -> Seq (abt '[] a) -> Seq (abt '[] a)
coalesceNaryOp NaryOp a
typ Seq (abt '[] a)
args'
else abt '[] a -> Seq (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
coalesce abt '[] a
abt)
View (Term abt) '[] a
_ -> abt '[] a -> Seq (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a
abt