{-# 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
              -- The hoist pass needs globally uniqiue identifiers
              (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