{-# LANGUAGE CPP
, GADTs
, DataKinds
, KindSignatures
, MultiParamTypeClasses
, FunctionalDependencies
, ScopedTypeVariables
, FlexibleContexts
, Rank2Types
, TypeSynonymInstances
, FlexibleInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Evaluation.Lazy
( evaluate
, evaluateNaryOp
, evaluatePrimOp
, evaluateArrayOp
, Interp(..), reifyPair
) where
import Prelude hiding (id, (.))
import Control.Category (Category(..))
#if __GLASGOW_HASKELL__ < 710
import Data.Functor ((<$>))
#endif
import Control.Monad ((<=<))
import Control.Monad.Identity (Identity, runIdentity)
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import qualified Data.Text as Text
import Language.Hakaru.Syntax.IClasses
import Data.Number.Nat
import Data.Number.Natural
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.DatumCase (DatumEvaluator, MatchState(..), matchTopPattern)
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Evaluation.Types
import qualified Language.Hakaru.Syntax.Prelude as P
#ifdef __TRACE_DISINTEGRATE__
import Language.Hakaru.Pretty.Haskell (pretty)
import Debug.Trace (trace)
#endif
evaluate
:: forall abt m p
. (ABT Term abt, EvaluationMonad abt m p)
=> MeasureEvaluator abt m
-> TermEvaluator abt m
{-# INLINE evaluate #-}
evaluate :: MeasureEvaluator abt m -> TermEvaluator abt m
evaluate MeasureEvaluator abt m
perform = abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_
where
evaluateCase_ :: CaseEvaluator abt m
evaluateCase_ :: abt '[] a -> [Branch a abt b] -> m (Whnf abt b)
evaluateCase_ = TermEvaluator abt m -> CaseEvaluator abt m
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
EvaluationMonad abt m p =>
TermEvaluator abt m -> CaseEvaluator abt m
evaluateCase TermEvaluator abt m
evaluate_
evaluate_ :: TermEvaluator abt m
evaluate_ :: abt '[] a -> m (Whnf abt a)
evaluate_ abt '[] a
e0 =
#ifdef __TRACE_DISINTEGRATE__
trace ("-- evaluate_: " ++ show (pretty e0)) $
#endif
abt '[] a
-> (Variable a -> m (Whnf abt a))
-> (Term abt a -> m (Whnf abt a))
-> m (Whnf 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
e0 (MeasureEvaluator abt m
-> TermEvaluator abt m -> VariableEvaluator abt m
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
EvaluationMonad abt m p =>
MeasureEvaluator abt m
-> TermEvaluator abt m -> VariableEvaluator abt m
evaluateVar MeasureEvaluator abt m
perform TermEvaluator abt m
evaluate_) ((Term abt a -> m (Whnf abt a)) -> m (Whnf abt a))
-> (Term abt a -> m (Whnf abt a)) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
case Term abt a
t of
Literal_ Literal a
v -> Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (Head abt a -> Whnf abt a) -> Head abt a -> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt a -> m (Whnf abt a)) -> Head abt a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ Literal a -> Head abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral Literal a
v
Datum_ Datum (abt '[]) (HData' t)
d -> Whnf abt (HData' t) -> m (Whnf abt (HData' t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt (HData' t) -> m (Whnf abt (HData' t)))
-> (Head abt (HData' t) -> Whnf abt (HData' t))
-> Head abt (HData' t)
-> m (Whnf abt (HData' t))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt (HData' t) -> Whnf abt (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt (HData' t) -> m (Whnf abt a))
-> Head abt (HData' t) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ Datum (abt '[]) (HData' t) -> Head abt (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' t)
d
Empty_ Sing ('HArray a)
typ -> Whnf abt ('HArray a) -> m (Whnf abt ('HArray a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HArray a) -> m (Whnf abt ('HArray a)))
-> (Head abt ('HArray a) -> Whnf abt ('HArray a))
-> Head abt ('HArray a)
-> m (Whnf abt ('HArray a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HArray a) -> Whnf abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HArray a) -> m (Whnf abt a))
-> Head abt ('HArray a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ Sing ('HArray a) -> Head abt ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Head abt ('HArray a)
WEmpty Sing ('HArray a)
typ
Array_ abt '[] 'HNat
e1 abt '[ 'HNat] a
e2 -> Whnf abt ('HArray a) -> m (Whnf abt ('HArray a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HArray a) -> m (Whnf abt ('HArray a)))
-> (Head abt ('HArray a) -> Whnf abt ('HArray a))
-> Head abt ('HArray a)
-> m (Whnf abt ('HArray a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HArray a) -> Whnf abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HArray a) -> m (Whnf abt a))
-> Head abt ('HArray a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[] 'HNat -> abt '[ 'HNat] a -> Head abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Head abt ('HArray a)
WArray abt '[] 'HNat
e1 abt '[ 'HNat] a
e2
ArrayLiteral_ [abt '[] a]
es -> Whnf abt ('HArray a) -> m (Whnf abt ('HArray a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HArray a) -> m (Whnf abt ('HArray a)))
-> (Head abt ('HArray a) -> Whnf abt ('HArray a))
-> Head abt ('HArray a)
-> m (Whnf abt ('HArray a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HArray a) -> Whnf abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HArray a) -> m (Whnf abt a))
-> Head abt ('HArray a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ [abt '[] a] -> Head abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Head abt ('HArray a)
WArrayLiteral [abt '[] a]
es
SCon args a
Lam_ :$ abt vars a
e1 :* SArgs abt args
End -> Whnf abt (a ':-> b) -> m (Whnf abt (a ':-> b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt (a ':-> b) -> m (Whnf abt (a ':-> b)))
-> (Head abt (a ':-> b) -> Whnf abt (a ':-> b))
-> Head abt (a ':-> b)
-> m (Whnf abt (a ':-> b))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt (a ':-> b) -> Whnf abt (a ':-> b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt (a ':-> a) -> m (Whnf abt a))
-> Head abt (a ':-> a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[a] a -> Head abt (a ':-> a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(typs :: Hakaru).
abt '[a] typs -> Head abt (a ':-> typs)
WLam abt vars a
abt '[a] a
e1
SCon args a
Dirac :$ abt vars a
e1 :* SArgs abt args
End -> Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a)))
-> (Head abt ('HMeasure a) -> Whnf abt ('HMeasure a))
-> Head abt ('HMeasure a)
-> m (Whnf abt ('HMeasure a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HMeasure a) -> Whnf abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HMeasure a) -> m (Whnf abt a))
-> Head abt ('HMeasure a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[] a -> Head abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Head abt ('HMeasure a)
WDirac abt vars a
abt '[] a
e1
SCon args a
MBind :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> Whnf abt ('HMeasure b) -> m (Whnf abt ('HMeasure b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HMeasure b) -> m (Whnf abt ('HMeasure b)))
-> (Head abt ('HMeasure b) -> Whnf abt ('HMeasure b))
-> Head abt ('HMeasure b)
-> m (Whnf abt ('HMeasure b))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HMeasure b) -> Whnf abt ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HMeasure b) -> m (Whnf abt a))
-> Head abt ('HMeasure b) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a)
-> abt '[a] ('HMeasure b) -> Head abt ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
abt '[] ('HMeasure a)
-> abt '[a] ('HMeasure b) -> Head abt ('HMeasure b)
WMBind abt vars a
abt '[] ('HMeasure a)
e1 abt vars a
abt '[a] ('HMeasure b)
e2
SCon args a
Plate :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> Whnf abt ('HMeasure ('HArray a))
-> m (Whnf abt ('HMeasure ('HArray a)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HMeasure ('HArray a))
-> m (Whnf abt ('HMeasure ('HArray a))))
-> (Head abt ('HMeasure ('HArray a))
-> Whnf abt ('HMeasure ('HArray a)))
-> Head abt ('HMeasure ('HArray a))
-> m (Whnf abt ('HMeasure ('HArray a)))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HMeasure ('HArray a))
-> Whnf abt ('HMeasure ('HArray a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HMeasure ('HArray a)) -> m (Whnf abt a))
-> Head abt ('HMeasure ('HArray a)) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[] 'HNat
-> abt '[ 'HNat] ('HMeasure a) -> Head abt ('HMeasure ('HArray a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat
-> abt '[ 'HNat] ('HMeasure a) -> Head abt ('HMeasure ('HArray a))
WPlate abt vars a
abt '[] 'HNat
e1 abt vars a
abt '[ 'HNat] ('HMeasure a)
e2
MeasureOp_ MeasureOp typs a
o :$ SArgs abt args
es -> Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a)))
-> (Head abt ('HMeasure a) -> Whnf abt ('HMeasure a))
-> Head abt ('HMeasure a)
-> m (Whnf abt ('HMeasure a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HMeasure a) -> Whnf abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HMeasure a) -> m (Whnf abt a))
-> Head abt ('HMeasure a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ MeasureOp typs a -> SArgs abt args -> Head abt ('HMeasure a)
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
(a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a -> SArgs abt args -> Head abt ('HMeasure a)
WMeasureOp MeasureOp typs a
o SArgs abt args
es
Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes -> Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a)))
-> (Head abt ('HMeasure a) -> Whnf abt ('HMeasure a))
-> Head abt ('HMeasure a)
-> m (Whnf abt ('HMeasure a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HMeasure a) -> Whnf abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HMeasure a) -> m (Whnf abt a))
-> Head abt ('HMeasure a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Head abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Head abt ('HMeasure a)
WSuperpose NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes
Reject_ Sing ('HMeasure a)
typ -> Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt ('HMeasure a) -> m (Whnf abt ('HMeasure a)))
-> (Head abt ('HMeasure a) -> Whnf abt ('HMeasure a))
-> Head abt ('HMeasure a)
-> m (Whnf abt ('HMeasure a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt ('HMeasure a) -> Whnf abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt ('HMeasure a) -> m (Whnf abt a))
-> Head abt ('HMeasure a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ Sing ('HMeasure a) -> Head abt ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Head abt ('HMeasure a)
WReject Sing ('HMeasure a)
typ
SCon args a
Integrate :$ abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End ->
Whnf abt 'HProb -> m (Whnf abt 'HProb)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HProb -> m (Whnf abt 'HProb))
-> (Head abt 'HProb -> Whnf abt 'HProb)
-> Head abt 'HProb
-> m (Whnf abt 'HProb)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt 'HProb -> Whnf abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt 'HProb -> m (Whnf abt a))
-> Head abt 'HProb -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[] 'HReal
-> abt '[] 'HReal -> abt '[ 'HReal] 'HProb -> Head abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
abt '[] 'HReal
-> abt '[] 'HReal -> abt '[ 'HReal] 'HProb -> Head abt 'HProb
WIntegrate abt vars a
abt '[] 'HReal
e1 abt vars a
abt '[] 'HReal
e2 abt vars a
abt '[ 'HReal] 'HProb
e3
Summate HDiscrete a
_ HSemiring a
_ :$ abt vars a
_ :* abt vars a
_ :* abt vars a
_ :* SArgs abt args
End ->
Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt a)) -> abt '[] a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ 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
t
SCon args a
App_ :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> do
Whnf abt a
w1 <- abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt vars a
abt '[] a
e1
case Whnf abt a
w1 of
Neutral abt '[] a
e1' -> Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt a)) -> abt '[] a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ abt '[] (a ':-> a) -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
P.app abt '[] a
abt '[] (a ':-> a)
e1' abt vars a
abt '[] a
e2
Head_ Head abt a
v1 -> Head abt a -> m (Whnf abt a)
evaluateApp Head abt a
v1
where
evaluateApp :: Head abt a -> m (Whnf abt a)
evaluateApp (WLam abt '[a] b
f) =
abt '[a] b
-> (Variable a -> abt '[] b -> m (Whnf abt b)) -> m (Whnf abt 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 '[a] b
f ((Variable a -> abt '[] b -> m (Whnf abt b)) -> m (Whnf abt b))
-> (Variable a -> abt '[] b -> m (Whnf abt b)) -> m (Whnf abt b)
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] b
f' -> do
[Index (abt '[])]
i <- m [Index (abt '[])]
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
EvaluationMonad abt m p =>
m [Index (abt '[])]
getIndices
Statement abt Variable p -> abt '[] b -> m (abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(xs :: [Hakaru]) (a :: Hakaru).
(ABT Term abt, EvaluationMonad abt m p) =>
Statement abt Variable p -> abt xs a -> m (abt xs a)
push (Variable a
-> Lazy abt a -> [Index (abt '[])] -> Statement abt Variable p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
(v :: Hakaru -> *) (a :: Hakaru).
v a -> Lazy abt a -> [Index (abt '[])] -> Statement abt v p
SLet Variable a
x (abt '[] a -> Lazy abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Lazy abt a
Thunk abt vars a
abt '[] a
e2) [Index (abt '[])]
i) abt '[] b
f' m (abt '[] b) -> (abt '[] b -> m (Whnf abt b)) -> m (Whnf abt b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_
evaluateApp Head abt a
_ = [Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error [Char]
"evaluate{App_}: the impossible happened"
SCon args a
Let_ :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> do
[Index (abt '[])]
i <- m [Index (abt '[])]
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
EvaluationMonad abt m p =>
m [Index (abt '[])]
getIndices
abt '[a] a
-> (Variable a -> abt '[] a -> m (Whnf abt a)) -> m (Whnf abt a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> m (Whnf abt a)) -> m (Whnf abt a))
-> (Variable a -> abt '[] a -> m (Whnf abt a)) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' ->
Statement abt Variable p -> abt '[] a -> m (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(xs :: [Hakaru]) (a :: Hakaru).
(ABT Term abt, EvaluationMonad abt m p) =>
Statement abt Variable p -> abt xs a -> m (abt xs a)
push (Variable a
-> Lazy abt a -> [Index (abt '[])] -> Statement abt Variable p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
(v :: Hakaru -> *) (a :: Hakaru).
v a -> Lazy abt a -> [Index (abt '[])] -> Statement abt v p
SLet Variable a
x (abt '[] a -> Lazy abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Lazy abt a
Thunk abt vars a
abt '[] a
e1) [Index (abt '[])]
i) abt '[] a
e2' m (abt '[] a) -> (abt '[] a -> m (Whnf abt a)) -> m (Whnf abt a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_
CoerceTo_ Coercion a a
c :$ abt vars a
e1 :* SArgs abt args
End -> Coercion a a -> Whnf abt a -> Whnf abt a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion a a
c (Whnf abt a -> Whnf abt a) -> m (Whnf abt a) -> m (Whnf abt a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt vars a
abt '[] a
e1
UnsafeFrom_ Coercion a b
c :$ abt vars a
e1 :* SArgs abt args
End -> Coercion a b -> Whnf abt b -> Whnf abt a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion a b
c (Whnf abt b -> Whnf abt a) -> m (Whnf abt b) -> m (Whnf abt a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt vars a
abt '[] a
e1
NaryOp_ NaryOp a
o Seq (abt '[] a)
es -> TermEvaluator abt m
-> NaryOp a -> Seq (abt '[] a) -> m (Whnf abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(a :: Hakaru).
(ABT Term abt, EvaluationMonad abt m p) =>
TermEvaluator abt m
-> NaryOp a -> Seq (abt '[] a) -> m (Whnf abt a)
evaluateNaryOp TermEvaluator abt m
evaluate_ NaryOp a
o Seq (abt '[] a)
es
ArrayOp_ ArrayOp typs a
o :$ SArgs abt args
es -> TermEvaluator abt m
-> ArrayOp typs a -> SArgs abt args -> m (Whnf abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, EvaluationMonad abt m p, typs ~ UnLCs args,
args ~ LCs typs) =>
TermEvaluator abt m
-> ArrayOp typs a -> SArgs abt args -> m (Whnf abt a)
evaluateArrayOp TermEvaluator abt m
evaluate_ ArrayOp typs a
o SArgs abt args
es
PrimOp_ PrimOp typs a
o :$ SArgs abt args
es -> TermEvaluator abt m
-> PrimOp typs a -> SArgs abt args -> m (Whnf abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, EvaluationMonad abt m p, typs ~ UnLCs args,
args ~ LCs typs) =>
TermEvaluator abt m
-> PrimOp typs a -> SArgs abt args -> m (Whnf abt a)
evaluatePrimOp TermEvaluator abt m
evaluate_ PrimOp typs a
o SArgs abt args
es
Transform_ Transform args a
tt :$ SArgs abt args
_ -> [Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error ([Char] -> m (Whnf abt a)) -> [Char] -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"TODO: evaluate{", Transform args a -> [Char]
forall a. Show a => a -> [Char]
show Transform args a
tt, [Char]
"}"
,[Char]
": cannot evaluate transforms; expand them first"]
Case_ abt '[] a
e [Branch a abt a]
bs -> abt '[] a -> [Branch a abt a] -> m (Whnf abt a)
CaseEvaluator abt m
evaluateCase_ abt '[] a
e [Branch a abt a]
bs
SCon args a
_ :$ SArgs abt args
_ -> [Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error [Char]
"evaluate: the impossible happened"
class Interp a a' | a -> a' where
reify :: (ABT Term abt) => Head abt a -> a'
reflect :: (ABT Term abt) => a' -> Head abt a
instance Interp 'HNat Natural where
reflect :: Natural -> Head abt 'HNat
reflect = Literal 'HNat -> Head abt 'HNat
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal 'HNat -> Head abt 'HNat)
-> (Natural -> Literal 'HNat) -> Natural -> Head abt 'HNat
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Natural -> Literal 'HNat
LNat
reify :: Head abt 'HNat -> Natural
reify (WLiteral (LNat Natural
n)) = Natural
n
reify (WCoerceTo Coercion a 'HNat
_ Head abt a
_) = [Char] -> Natural
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WCoerceTo}"
reify (WUnsafeFrom Coercion 'HNat b
_ Head abt b
_) = [Char] -> Natural
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WUnsafeFrom}"
instance Interp 'HInt Integer where
reflect :: Integer -> Head abt 'HInt
reflect = Literal 'HInt -> Head abt 'HInt
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal 'HInt -> Head abt 'HInt)
-> (Integer -> Literal 'HInt) -> Integer -> Head abt 'HInt
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Literal 'HInt
LInt
reify :: Head abt 'HInt -> Integer
reify (WLiteral (LInt Integer
i)) = Integer
i
reify (WCoerceTo Coercion a 'HInt
_ Head abt a
_) = [Char] -> Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WCoerceTo}"
reify (WUnsafeFrom Coercion 'HInt b
_ Head abt b
_) = [Char] -> Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WUnsafeFrom}"
instance Interp 'HProb NonNegativeRational where
reflect :: NonNegativeRational -> Head abt 'HProb
reflect = Literal 'HProb -> Head abt 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal 'HProb -> Head abt 'HProb)
-> (NonNegativeRational -> Literal 'HProb)
-> NonNegativeRational
-> Head abt 'HProb
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. NonNegativeRational -> Literal 'HProb
LProb
reify :: Head abt 'HProb -> NonNegativeRational
reify (WLiteral (LProb NonNegativeRational
p)) = NonNegativeRational
p
reify (WCoerceTo Coercion a 'HProb
_ Head abt a
_) = [Char] -> NonNegativeRational
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WCoerceTo}"
reify (WUnsafeFrom Coercion 'HProb b
_ Head abt b
_) = [Char] -> NonNegativeRational
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WUnsafeFrom}"
reify (WIntegrate abt '[] 'HReal
_ abt '[] 'HReal
_ abt '[ 'HReal] 'HProb
_) = [Char] -> NonNegativeRational
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WIntegrate}"
instance Interp 'HReal Rational where
reflect :: Rational -> Head abt 'HReal
reflect = Literal 'HReal -> Head abt 'HReal
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal 'HReal -> Head abt 'HReal)
-> (Rational -> Literal 'HReal) -> Rational -> Head abt 'HReal
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Rational -> Literal 'HReal
LReal
reify :: Head abt 'HReal -> Rational
reify (WLiteral (LReal Rational
r)) = Rational
r
reify (WCoerceTo Coercion a 'HReal
_ Head abt a
_) = [Char] -> Rational
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WCoerceTo}"
reify (WUnsafeFrom Coercion 'HReal b
_ Head abt b
_) = [Char] -> Rational
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: reify{WUnsafeFrom}"
identifyDatum :: (ABT Term abt) => DatumEvaluator (abt '[]) Identity
identifyDatum :: DatumEvaluator (abt '[]) Identity
identifyDatum = Maybe (Datum (abt '[]) ('HData t (Code t)))
-> Identity (Maybe (Datum (abt '[]) ('HData t (Code t))))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Datum (abt '[]) ('HData t (Code t)))
-> Identity (Maybe (Datum (abt '[]) ('HData t (Code t)))))
-> (abt '[] ('HData t (Code t))
-> Maybe (Datum (abt '[]) ('HData t (Code t))))
-> abt '[] ('HData t (Code t))
-> Identity (Maybe (Datum (abt '[]) ('HData t (Code t))))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Whnf abt ('HData t (Code t))
-> Maybe (Datum (abt '[]) ('HData t (Code t)))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
ABT Term abt =>
Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
viewWhnfDatum (Whnf abt ('HData t (Code t))
-> Maybe (Datum (abt '[]) ('HData t (Code t))))
-> (abt '[] ('HData t (Code t))
-> Maybe (Whnf abt ('HData t (Code t))))
-> abt '[] ('HData t (Code t))
-> Maybe (Datum (abt '[]) ('HData t (Code t)))
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< abt '[] ('HData t (Code t)) -> Maybe (Whnf abt ('HData t (Code t)))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Maybe (Whnf abt a)
toWhnf)
instance Interp HUnit () where
reflect :: () -> Head abt HUnit
reflect () = Datum (abt '[]) (HData' ('TyCon "Unit"))
-> Head abt (HData' ('TyCon "Unit"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Unit"))
forall (ast :: Hakaru -> *). Datum ast HUnit
dUnit
reify :: Head abt HUnit -> ()
reify Head abt HUnit
v = Identity () -> ()
forall a. Identity a -> a
runIdentity (Identity () -> ()) -> Identity () -> ()
forall a b. (a -> b) -> a -> b
$ do
Maybe (MatchState (abt '[]) '[])
match <- DatumEvaluator (abt '[]) Identity
-> abt '[] HUnit
-> Pattern '[] HUnit
-> List1 Variable '[]
-> Identity (Maybe (MatchState (abt '[]) '[]))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
(vars :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable vars
-> m (Maybe (MatchState ast '[]))
matchTopPattern DatumEvaluator (abt '[]) Identity
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
DatumEvaluator (abt '[]) Identity
identifyDatum (Head abt HUnit -> abt '[] HUnit
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt HUnit
v) Pattern '[] HUnit
pUnit List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1
case Maybe (MatchState (abt '[]) '[])
match of
Just (Matched_ DList (Assoc (abt '[]))
_ss List1 Variable '[]
Nil1) -> () -> Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe (MatchState (abt '[]) '[])
_ -> [Char] -> Identity ()
forall a. HasCallStack => [Char] -> a
error [Char]
"reify{HUnit}: the impossible happened"
instance Interp HBool Bool where
reflect :: Bool -> Head abt HBool
reflect = Datum (abt '[]) HBool -> Head abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum (Datum (abt '[]) HBool -> Head abt HBool)
-> (Bool -> Datum (abt '[]) HBool) -> Bool -> Head abt HBool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (\Bool
b -> if Bool
b then Datum (abt '[]) HBool
forall (ast :: Hakaru -> *). Datum ast HBool
dTrue else Datum (abt '[]) HBool
forall (ast :: Hakaru -> *). Datum ast HBool
dFalse)
reify :: Head abt HBool -> Bool
reify Head abt HBool
v = Identity Bool -> Bool
forall a. Identity a -> a
runIdentity (Identity Bool -> Bool) -> Identity Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
Maybe (MatchState (abt '[]) '[])
matchT <- DatumEvaluator (abt '[]) Identity
-> abt '[] HBool
-> Pattern '[] HBool
-> List1 Variable '[]
-> Identity (Maybe (MatchState (abt '[]) '[]))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
(vars :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable vars
-> m (Maybe (MatchState ast '[]))
matchTopPattern DatumEvaluator (abt '[]) Identity
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
DatumEvaluator (abt '[]) Identity
identifyDatum (Head abt HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt HBool
v) Pattern '[] HBool
pTrue List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1
case Maybe (MatchState (abt '[]) '[])
matchT of
Just (Matched_ DList (Assoc (abt '[]))
_ss List1 Variable '[]
Nil1) -> Bool -> Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just MatchState (abt '[]) '[]
GotStuck_ -> [Char] -> Identity Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"reify{HBool}: the impossible happened"
Maybe (MatchState (abt '[]) '[])
Nothing -> do
Maybe (MatchState (abt '[]) '[])
matchF <- DatumEvaluator (abt '[]) Identity
-> abt '[] HBool
-> Pattern '[] HBool
-> List1 Variable '[]
-> Identity (Maybe (MatchState (abt '[]) '[]))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
(vars :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable vars
-> m (Maybe (MatchState ast '[]))
matchTopPattern DatumEvaluator (abt '[]) Identity
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
DatumEvaluator (abt '[]) Identity
identifyDatum (Head abt HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt HBool
v) Pattern '[] HBool
pFalse List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1
case Maybe (MatchState (abt '[]) '[])
matchF of
Just (Matched_ DList (Assoc (abt '[]))
_ss List1 Variable '[]
Nil1) -> Bool -> Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Maybe (MatchState (abt '[]) '[])
_ -> [Char] -> Identity Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"reify{HBool}: the impossible happened"
reifyPair
:: (ABT Term abt) => Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair :: Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt (HPair a b)
v =
let impossible :: a
impossible = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"reifyPair: the impossible happened"
e0 :: abt '[] (HPair a b)
e0 = Head abt (HPair a b) -> abt '[] (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt (HPair a b)
v
n :: Nat
n = abt '[] (HPair a b) -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFree abt '[] (HPair a b)
e0
(Sing a
a,Sing b
b) = Sing (HPair a b) -> (Sing a, Sing b)
forall (a :: Hakaru) (b :: Hakaru).
Sing (HPair a b) -> (Sing a, Sing b)
sUnPair (Sing (HPair a b) -> (Sing a, Sing b))
-> Sing (HPair a b) -> (Sing a, Sing b)
forall a b. (a -> b) -> a -> b
$ abt '[] (HPair a b) -> Sing (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] (HPair a b)
e0
x :: Variable a
x = Text -> Nat -> Sing a -> Variable a
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
Text.empty Nat
n Sing a
a
y :: Variable b
y = Text -> Nat -> Sing b -> Variable b
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
Text.empty (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n) Sing b
b
in Identity (abt '[] a, abt '[] b) -> (abt '[] a, abt '[] b)
forall a. Identity a -> a
runIdentity (Identity (abt '[] a, abt '[] b) -> (abt '[] a, abt '[] b))
-> Identity (abt '[] a, abt '[] b) -> (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ do
Maybe (MatchState (abt '[]) '[])
match <- DatumEvaluator (abt '[]) Identity
-> abt '[] (HPair a b)
-> Pattern '[a, b] (HPair a b)
-> List1 Variable '[a, b]
-> Identity (Maybe (MatchState (abt '[]) '[]))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
(vars :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable vars
-> m (Maybe (MatchState ast '[]))
matchTopPattern DatumEvaluator (abt '[]) Identity
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
DatumEvaluator (abt '[]) Identity
identifyDatum abt '[] (HPair a b)
e0 (Pattern '[a] a
-> Pattern '[b] b -> Pattern ('[a] ++ '[b]) (HPair a b)
forall (vars1 :: [Hakaru]) (a :: Hakaru) (vars2 :: [Hakaru])
(b :: Hakaru).
Pattern vars1 a
-> Pattern vars2 b -> Pattern (vars1 ++ vars2) (HPair a b)
pPair Pattern '[a] a
forall (a :: Hakaru). Pattern '[a] a
PVar Pattern '[b] b
forall (a :: Hakaru). Pattern '[a] a
PVar) (Variable a -> List1 Variable '[b] -> List1 Variable '[a, b]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 Variable a
x (Variable b -> List1 Variable '[] -> List1 Variable '[b]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 Variable b
y List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1))
case Maybe (MatchState (abt '[]) '[])
match of
Just (Matched_ DList (Assoc (abt '[]))
ss List1 Variable '[]
Nil1) ->
case DList (Assoc (abt '[]))
ss [] of
[Assoc Variable a
x' abt '[] a
e1, Assoc Variable a
y' abt '[] a
e2] ->
Identity (abt '[] a, abt '[] b)
-> (Identity (abt '[] a, abt '[] b)
-> Identity (abt '[] a, abt '[] b))
-> Maybe (Identity (abt '[] a, abt '[] b))
-> Identity (abt '[] a, abt '[] b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Identity (abt '[] a, abt '[] b)
forall a. a
impossible Identity (abt '[] a, abt '[] b) -> Identity (abt '[] a, abt '[] b)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Maybe (Identity (abt '[] a, abt '[] b))
-> Identity (abt '[] a, abt '[] b))
-> Maybe (Identity (abt '[] a, abt '[] b))
-> Identity (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ do
TypeEq a a
Refl <- Variable a -> Variable a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable a
x Variable a
x'
TypeEq b a
Refl <- Variable b -> Variable a -> Maybe (TypeEq b a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable b
y Variable a
y'
Identity (abt '[] a, abt '[] a)
-> Maybe (Identity (abt '[] a, abt '[] a))
forall a. a -> Maybe a
Just (Identity (abt '[] a, abt '[] a)
-> Maybe (Identity (abt '[] a, abt '[] a)))
-> Identity (abt '[] a, abt '[] a)
-> Maybe (Identity (abt '[] a, abt '[] a))
forall a b. (a -> b) -> a -> b
$ (abt '[] a, abt '[] a) -> Identity (abt '[] a, abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] a
e1, abt '[] a
e2)
[Assoc (abt '[])]
_ -> Identity (abt '[] a, abt '[] b)
forall a. a
impossible
Maybe (MatchState (abt '[]) '[])
_ -> Identity (abt '[] a, abt '[] b)
forall a. a
impossible
impl, diff, nand, nor :: Bool -> Bool -> Bool
impl :: Bool -> Bool -> Bool
impl Bool
x Bool
y = Bool -> Bool
not Bool
x Bool -> Bool -> Bool
|| Bool
y
diff :: Bool -> Bool -> Bool
diff Bool
x Bool
y = Bool
x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
y
nand :: Bool -> Bool -> Bool
nand Bool
x Bool
y = Bool -> Bool
not (Bool
x Bool -> Bool -> Bool
&& Bool
y)
nor :: Bool -> Bool -> Bool
nor Bool
x Bool
y = Bool -> Bool
not (Bool
x Bool -> Bool -> Bool
|| Bool
y)
evaluateNaryOp
:: (ABT Term abt, EvaluationMonad abt m p)
=> TermEvaluator abt m
-> NaryOp a
-> Seq (abt '[] a)
-> m (Whnf abt a)
evaluateNaryOp :: TermEvaluator abt m
-> NaryOp a -> Seq (abt '[] a) -> m (Whnf abt a)
evaluateNaryOp TermEvaluator abt m
evaluate_ = \NaryOp a
o Seq (abt '[] a)
es -> NaryOp a
-> (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a)
-> Seq (abt '[] a)
-> m (Whnf abt a)
mainLoop NaryOp a
o (NaryOp a -> Head abt a -> Head abt a -> Head abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NaryOp a -> Head abt a -> Head abt a -> Head abt a
evalOp NaryOp a
o) Seq (Whnf abt a)
forall a. Seq a
Seq.empty Seq (abt '[] a)
es
where
mainLoop :: NaryOp a
-> (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a)
-> Seq (abt '[] a)
-> m (Whnf abt a)
mainLoop NaryOp a
o Head abt a -> Head abt a -> Head abt a
op Seq (Whnf abt a)
ws Seq (abt '[] a)
es =
case Seq (abt '[] a) -> ViewL (abt '[] a)
forall a. Seq a -> ViewL a
Seq.viewl Seq (abt '[] a)
es of
ViewL (abt '[] a)
Seq.EmptyL -> Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a)) -> Whnf abt a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$
case Seq (Whnf abt a) -> ViewL (Whnf abt a)
forall a. Seq a -> ViewL a
Seq.viewl Seq (Whnf abt a)
ws of
ViewL (Whnf abt a)
Seq.EmptyL -> NaryOp a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NaryOp a -> Whnf abt a
identityElement NaryOp a
o
Whnf abt a
w Seq.:< Seq (Whnf abt a)
ws'
| Seq (Whnf abt a) -> Bool
forall a. Seq a -> Bool
Seq.null Seq (Whnf abt a)
ws' -> Whnf abt a
w
| Bool
otherwise ->
abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> Whnf abt a)
-> (Seq (abt '[] a) -> abt '[] a) -> Seq (abt '[] a) -> Whnf abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 -> abt '[] a)
-> (Seq (abt '[] a) -> Term abt a) -> Seq (abt '[] a) -> abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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
o (Seq (abt '[] a) -> Whnf abt a) -> Seq (abt '[] a) -> Whnf abt a
forall a b. (a -> b) -> a -> b
$ (Whnf abt a -> abt '[] a) -> Seq (Whnf abt a) -> Seq (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Whnf abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Seq (Whnf abt a)
ws
abt '[] a
e Seq.:< Seq (abt '[] a)
es' -> do
Whnf abt a
w <- abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt '[] a
e
case NaryOp a -> Whnf abt a -> Maybe (Seq (abt '[] a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NaryOp a -> Whnf abt a -> Maybe (Seq (abt '[] a))
matchNaryOp NaryOp a
o Whnf abt a
w of
Maybe (Seq (abt '[] a))
Nothing -> NaryOp a
-> (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a)
-> Seq (abt '[] a)
-> m (Whnf abt a)
mainLoop NaryOp a
o Head abt a -> Head abt a -> Head abt a
op ((Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a) -> Whnf abt a -> Seq (Whnf abt a)
forall (syn :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)
(abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT syn abt =>
(Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a) -> Whnf abt a -> Seq (Whnf abt a)
snocLoop Head abt a -> Head abt a -> Head abt a
op Seq (Whnf abt a)
ws Whnf abt a
w) Seq (abt '[] a)
es'
Just Seq (abt '[] a)
es2 -> NaryOp a
-> (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a)
-> Seq (abt '[] a)
-> m (Whnf abt a)
mainLoop NaryOp a
o Head abt a -> Head abt a -> Head abt a
op Seq (Whnf abt a)
ws (Seq (abt '[] a)
es2 Seq (abt '[] a) -> Seq (abt '[] a) -> Seq (abt '[] a)
forall a. Seq a -> Seq a -> Seq a
Seq.>< Seq (abt '[] a)
es')
snocLoop
:: (ABT syn abt)
=> (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a)
-> Whnf abt a
-> Seq (Whnf abt a)
snocLoop :: (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a) -> Whnf abt a -> Seq (Whnf abt a)
snocLoop Head abt a -> Head abt a -> Head abt a
op Seq (Whnf abt a)
ws Whnf abt a
w1 =
case Seq (Whnf abt a) -> ViewR (Whnf abt a)
forall a. Seq a -> ViewR a
Seq.viewr Seq (Whnf abt a)
ws of
ViewR (Whnf abt a)
Seq.EmptyR -> Whnf abt a -> Seq (Whnf abt a)
forall a. a -> Seq a
Seq.singleton Whnf abt a
w1
Seq (Whnf abt a)
ws' Seq.:> Whnf abt a
w2 ->
case (Whnf abt a
w1,Whnf abt a
w2) of
(Head_ Head abt a
v1, Head_ Head abt a
v2) -> (Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a) -> Whnf abt a -> Seq (Whnf abt a)
forall (syn :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)
(abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT syn abt =>
(Head abt a -> Head abt a -> Head abt a)
-> Seq (Whnf abt a) -> Whnf abt a -> Seq (Whnf abt a)
snocLoop Head abt a -> Head abt a -> Head abt a
op Seq (Whnf abt a)
ws' (Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt a -> Head abt a -> Head abt a
op Head abt a
v1 Head abt a
v2))
(Whnf abt a, Whnf abt a)
_ -> Seq (Whnf abt a)
ws Seq (Whnf abt a) -> Whnf abt a -> Seq (Whnf abt a)
forall a. Seq a -> a -> Seq a
Seq.|> Whnf abt a
w1
matchNaryOp
:: (ABT Term abt)
=> NaryOp a
-> Whnf abt a
-> Maybe (Seq (abt '[] a))
matchNaryOp :: NaryOp a -> Whnf abt a -> Maybe (Seq (abt '[] a))
matchNaryOp NaryOp a
o Whnf abt a
w =
case Whnf abt a
w of
Head_ Head abt a
_ -> Maybe (Seq (abt '[] a))
forall a. Maybe a
Nothing
Neutral abt '[] a
e ->
abt '[] a
-> (Variable a -> Maybe (Seq (abt '[] a)))
-> (Term abt a -> Maybe (Seq (abt '[] a)))
-> Maybe (Seq (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
e (Maybe (Seq (abt '[] a)) -> Variable a -> Maybe (Seq (abt '[] a))
forall a b. a -> b -> a
const Maybe (Seq (abt '[] a))
forall a. Maybe a
Nothing) ((Term abt a -> Maybe (Seq (abt '[] a)))
-> Maybe (Seq (abt '[] a)))
-> (Term abt a -> Maybe (Seq (abt '[] a)))
-> Maybe (Seq (abt '[] a))
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
case Term abt a
t of
NaryOp_ NaryOp a
o' Seq (abt '[] a)
es | NaryOp a
o' NaryOp a -> NaryOp a -> Bool
forall a. Eq a => a -> a -> Bool
== NaryOp a
o -> Seq (abt '[] a) -> Maybe (Seq (abt '[] a))
forall a. a -> Maybe a
Just Seq (abt '[] a)
es
Term abt a
_ -> Maybe (Seq (abt '[] a))
forall a. Maybe a
Nothing
identityElement :: (ABT Term abt) => NaryOp a -> Whnf abt a
identityElement :: NaryOp a -> Whnf abt a
identityElement NaryOp a
o =
case NaryOp a
o of
NaryOp a
And -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Datum (abt '[]) (HData' ('TyCon "Bool"))
-> Head abt (HData' ('TyCon "Bool"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Bool"))
forall (ast :: Hakaru -> *). Datum ast HBool
dTrue)
NaryOp a
Or -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Datum (abt '[]) (HData' ('TyCon "Bool"))
-> Head abt (HData' ('TyCon "Bool"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Bool"))
forall (ast :: Hakaru -> *). Datum ast HBool
dFalse)
NaryOp a
Xor -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Datum (abt '[]) (HData' ('TyCon "Bool"))
-> Head abt (HData' ('TyCon "Bool"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Bool"))
forall (ast :: Hakaru -> *). Datum ast HBool
dFalse)
NaryOp a
Iff -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Datum (abt '[]) (HData' ('TyCon "Bool"))
-> Head abt (HData' ('TyCon "Bool"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Bool"))
forall (ast :: Hakaru -> *). Datum ast HBool
dTrue)
Min HOrd a
_ -> abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (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 (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
o Seq (abt '[] a)
forall a. Seq a
Seq.empty))
Max HOrd a
_ -> abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (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 (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
o Seq (abt '[] a)
forall a. Seq a
Seq.empty))
Sum HSemiring a
HSemiring_Nat -> Head abt 'HNat -> Whnf abt 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HNat -> Head abt 'HNat
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Natural -> Literal 'HNat
LNat Natural
0))
Sum HSemiring a
HSemiring_Int -> Head abt 'HInt -> Whnf abt 'HInt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HInt -> Head abt 'HInt
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Integer -> Literal 'HInt
LInt Integer
0))
Sum HSemiring a
HSemiring_Prob -> Head abt 'HProb -> Whnf abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HProb -> Head abt 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (NonNegativeRational -> Literal 'HProb
LProb NonNegativeRational
0))
Sum HSemiring a
HSemiring_Real -> Head abt 'HReal -> Whnf abt 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HReal -> Head abt 'HReal
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Rational -> Literal 'HReal
LReal Rational
0))
Prod HSemiring a
HSemiring_Nat -> Head abt 'HNat -> Whnf abt 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HNat -> Head abt 'HNat
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Natural -> Literal 'HNat
LNat Natural
1))
Prod HSemiring a
HSemiring_Int -> Head abt 'HInt -> Whnf abt 'HInt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HInt -> Head abt 'HInt
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Integer -> Literal 'HInt
LInt Integer
1))
Prod HSemiring a
HSemiring_Prob -> Head abt 'HProb -> Whnf abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HProb -> Head abt 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (NonNegativeRational -> Literal 'HProb
LProb NonNegativeRational
1))
Prod HSemiring a
HSemiring_Real -> Head abt 'HReal -> Whnf abt 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Literal 'HReal -> Head abt 'HReal
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Rational -> Literal 'HReal
LReal Rational
1))
evalOp
:: (ABT Term abt)
=> NaryOp a
-> Head abt a
-> Head abt a
-> Head abt a
evalOp :: NaryOp a -> Head abt a -> Head abt a -> Head abt a
evalOp NaryOp a
And = \Head abt a
v1 Head abt a
v2 -> Bool -> Head abt a
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
a' -> Head abt a
reflect (Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v1 Bool -> Bool -> Bool
&& Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v2)
evalOp NaryOp a
Or = \Head abt a
v1 Head abt a
v2 -> Bool -> Head abt a
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
a' -> Head abt a
reflect (Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v1 Bool -> Bool -> Bool
|| Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v2)
evalOp NaryOp a
Xor = \Head abt a
v1 Head abt a
v2 -> Bool -> Head abt a
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
a' -> Head abt a
reflect (Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v2)
evalOp NaryOp a
Iff = \Head abt a
v1 Head abt a
v2 -> Bool -> Head abt a
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
a' -> Head abt a
reflect (Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Head abt a -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt a
v2)
evalOp (Min HOrd a
_) = [Char] -> Head abt a -> Head abt a -> Head abt a
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: evalOp{Min}"
evalOp (Max HOrd a
_) = [Char] -> Head abt a -> Head abt a -> Head abt a
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: evalOp{Max}"
evalOp (Sum HSemiring a
theSemi) =
\(WLiteral Literal a
v1) (WLiteral Literal a
v2) -> Literal a -> Head abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal a -> Head abt a) -> Literal a -> Head abt a
forall a b. (a -> b) -> a -> b
$ HSemiring a -> Literal a -> Literal a -> Literal a
forall (a :: Hakaru).
HSemiring a -> Literal a -> Literal a -> Literal a
evalSum HSemiring a
theSemi Literal a
v1 Literal a
v2
evalOp (Prod HSemiring a
theSemi) =
\(WLiteral Literal a
v1) (WLiteral Literal a
v2) -> Literal a -> Head abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal a -> Head abt a) -> Literal a -> Head abt a
forall a b. (a -> b) -> a -> b
$ HSemiring a -> Literal a -> Literal a -> Literal a
forall (a :: Hakaru).
HSemiring a -> Literal a -> Literal a -> Literal a
evalProd HSemiring a
theSemi Literal a
v1 Literal a
v2
evalSum, evalProd :: HSemiring a -> Literal a -> Literal a -> Literal a
evalSum :: HSemiring a -> Literal a -> Literal a -> Literal a
evalSum HSemiring a
HSemiring_Nat = \(LNat Natural
n1) (LNat Natural
n2) -> Natural -> Literal 'HNat
LNat (Natural
n1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n2)
evalSum HSemiring a
HSemiring_Int = \(LInt Integer
i1) (LInt Integer
i2) -> Integer -> Literal 'HInt
LInt (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i2)
evalSum HSemiring a
HSemiring_Prob = \(LProb NonNegativeRational
p1) (LProb NonNegativeRational
p2) -> NonNegativeRational -> Literal 'HProb
LProb (NonNegativeRational
p1 NonNegativeRational -> NonNegativeRational -> NonNegativeRational
forall a. Num a => a -> a -> a
+ NonNegativeRational
p2)
evalSum HSemiring a
HSemiring_Real = \(LReal Rational
r1) (LReal Rational
r2) -> Rational -> Literal 'HReal
LReal (Rational
r1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
r2)
evalProd :: HSemiring a -> Literal a -> Literal a -> Literal a
evalProd HSemiring a
HSemiring_Nat = \(LNat Natural
n1) (LNat Natural
n2) -> Natural -> Literal 'HNat
LNat (Natural
n1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
n2)
evalProd HSemiring a
HSemiring_Int = \(LInt Integer
i1) (LInt Integer
i2) -> Integer -> Literal 'HInt
LInt (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i2)
evalProd HSemiring a
HSemiring_Prob = \(LProb NonNegativeRational
p1) (LProb NonNegativeRational
p2) -> NonNegativeRational -> Literal 'HProb
LProb (NonNegativeRational
p1 NonNegativeRational -> NonNegativeRational -> NonNegativeRational
forall a. Num a => a -> a -> a
* NonNegativeRational
p2)
evalProd HSemiring a
HSemiring_Real = \(LReal Rational
r1) (LReal Rational
r2) -> Rational -> Literal 'HReal
LReal (Rational
r1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
r2)
evaluateArrayOp
:: ( ABT Term abt, EvaluationMonad abt m p
, typs ~ UnLCs args, args ~ LCs typs)
=> TermEvaluator abt m
-> ArrayOp typs a
-> SArgs abt args
-> m (Whnf abt a)
evaluateArrayOp :: TermEvaluator abt m
-> ArrayOp typs a -> SArgs abt args -> m (Whnf abt a)
evaluateArrayOp TermEvaluator abt m
evaluate_ = ArrayOp typs a -> SArgs abt args -> m (Whnf abt a)
go
where
go :: ArrayOp typs a -> SArgs abt args -> m (Whnf abt a)
go o :: ArrayOp typs a
o@(Index Sing a
_) = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> do
let
Whnf abt a
w1 <- abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt vars a
abt '[] a
e1
case Whnf abt a
w1 of
Neutral abt '[] a
e1' ->
Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt a)) -> abt '[] a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ 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 (ArrayOp typs a -> SCon '[ '( '[], a), '(vars, a)] a
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
(a :: Hakaru).
(typs ~ UnLCs args, args ~ LCs typs) =>
ArrayOp typs a -> SCon args a
ArrayOp_ ArrayOp typs a
o SCon '[ '( '[], a), '(vars, a)] a
-> SArgs abt '[ '( '[], a), '(vars, a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
e1' abt '[] a
-> SArgs abt '[ '(vars, a)] -> SArgs abt '[ '( '[], a), '(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)
Head_ (WArray abt '[] 'HNat
_ abt '[ 'HNat] a
b) ->
abt '[ 'HNat] a
-> (Variable 'HNat -> abt '[] a -> m (Whnf abt a))
-> m (Whnf abt a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt '[ 'HNat] a
b ((Variable 'HNat -> abt '[] a -> m (Whnf abt a)) -> m (Whnf abt a))
-> (Variable 'HNat -> abt '[] a -> m (Whnf abt a))
-> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ \Variable 'HNat
x abt '[] a
body -> Variable 'HNat -> abt '[] 'HNat -> abt '[] a -> m (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(xs :: [Hakaru]) (b :: Hakaru) (m :: * -> *) (p :: Purity).
EvaluationMonad abt m p =>
Variable a -> abt '[] a -> abt xs b -> m (abt xs b)
extSubst Variable 'HNat
x abt vars a
abt '[] 'HNat
e2 abt '[] a
body m (abt '[] a) -> (abt '[] a -> m (Whnf abt a)) -> m (Whnf abt a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_
Head_ (WEmpty Sing ('HArray a)
_) ->
[Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: evaluateArrayOp{Index}{Head_ (WEmpty _)}"
Head_ (WArrayLiteral [abt '[] a]
arr) ->
do Whnf abt a
w2 <- abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt vars a
abt '[] a
e2
case Whnf abt a
w2 of
Head_ (WLiteral (LNat Natural
n)) -> Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt a)) -> abt '[] a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$
[abt '[] a]
arr [abt '[] a] -> Int -> abt '[] a
forall a. [a] -> Int -> a
!! Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Natural -> Integer
fromNatural Natural
n)
Whnf abt a
_ -> Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt a)) -> abt '[] a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$
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 (ArrayOp typs a -> SCon '[ '( '[], a), '( '[], a)] a
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
(a :: Hakaru).
(typs ~ UnLCs args, args ~ LCs typs) =>
ArrayOp typs a -> SCon args a
ArrayOp_ ArrayOp typs a
o SCon '[ '( '[], a), '( '[], a)] a
-> SArgs abt '[ '( '[], a), '( '[], a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Whnf abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt a
w1 abt '[] a
-> SArgs abt '[ '( '[], a)] -> SArgs abt '[ '( '[], a), '( '[], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Whnf abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt a
w2 abt '[] a -> SArgs abt '[] -> SArgs abt '[ '( '[], 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)
Whnf abt a
_ -> [Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error [Char]
"evaluateArrayOp{Index}: uknown whnf of array type"
go o :: ArrayOp typs a
o@(Size Sing a
_) = \(abt vars a
e1 :* SArgs abt args
End) -> do
Whnf abt a
w1 <- abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_ abt vars a
abt '[] a
e1
case Whnf abt a
w1 of
Neutral abt '[] a
e1' -> Whnf abt 'HNat -> m (Whnf abt 'HNat)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HNat -> m (Whnf abt 'HNat))
-> (abt '[] 'HNat -> Whnf abt 'HNat)
-> abt '[] 'HNat
-> m (Whnf abt 'HNat)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] 'HNat -> Whnf abt 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt 'HNat))
-> abt '[] a -> m (Whnf abt 'HNat)
forall a b. (a -> b) -> a -> b
$ 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 (ArrayOp typs a -> SCon '[ '( '[], a)] a
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
(a :: Hakaru).
(typs ~ UnLCs args, args ~ LCs typs) =>
ArrayOp typs a -> SCon args a
ArrayOp_ ArrayOp typs a
o SCon '[ '( '[], a)] a -> SArgs abt '[ '( '[], a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
e1' abt '[] a -> SArgs abt '[] -> SArgs abt '[ '( '[], 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)
Head_ (WEmpty Sing ('HArray a)
_) -> Whnf abt 'HNat -> m (Whnf abt 'HNat)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HNat -> m (Whnf abt 'HNat))
-> (Head abt 'HNat -> Whnf abt 'HNat)
-> Head abt 'HNat
-> m (Whnf abt 'HNat)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt 'HNat -> Whnf abt 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt 'HNat -> m (Whnf abt 'HNat))
-> Head abt 'HNat -> m (Whnf abt 'HNat)
forall a b. (a -> b) -> a -> b
$ Literal 'HNat -> Head abt 'HNat
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Natural -> Literal 'HNat
LNat Natural
0)
Head_ (WArray abt '[] 'HNat
e2 abt '[ 'HNat] a
_) -> abt '[] 'HNat -> m (Whnf abt 'HNat)
TermEvaluator abt m
evaluate_ abt '[] 'HNat
e2
Head_ (WArrayLiteral [abt '[] a]
es) -> Whnf abt 'HNat -> m (Whnf abt 'HNat)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HNat -> m (Whnf abt 'HNat))
-> (Int -> Whnf abt 'HNat) -> Int -> m (Whnf abt 'HNat)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Head abt 'HNat -> Whnf abt 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt 'HNat -> Whnf abt 'HNat)
-> (Int -> Head abt 'HNat) -> Int -> Whnf abt 'HNat
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Literal 'HNat -> Head abt 'HNat
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Literal 'HNat -> Head abt 'HNat)
-> (Int -> Literal 'HNat) -> Int -> Head abt 'HNat
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
PrimCoercion 'HNat 'HInt -> Literal 'HInt -> Literal 'HNat
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom (HRing 'HInt -> PrimCoercion (NonNegative 'HInt) 'HInt
forall (a :: Hakaru). HRing a -> PrimCoercion (NonNegative a) a
Signed HRing 'HInt
HRing_Int) (Literal 'HInt -> Literal 'HNat)
-> (Int -> Literal 'HInt) -> Int -> Literal 'HNat
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Integer -> Literal 'HInt
LInt (Integer -> Literal 'HInt)
-> (Int -> Integer) -> Int -> Literal 'HInt
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> m (Whnf abt 'HNat)) -> Int -> m (Whnf abt 'HNat)
forall a b. (a -> b) -> a -> b
$ [abt '[] a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [abt '[] a]
es
Head_ Head abt a
_ -> [Char] -> m (Whnf abt 'HNat)
forall a. HasCallStack => [Char] -> a
error [Char]
"Got something odd when evaluating an array"
go (Reduce Sing a
_) = \(abt vars a
_ :* abt vars a
_ :* abt vars a
_ :* SArgs abt args
End) ->
[Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: evaluateArrayOp{Reduce}"
evaluatePrimOp
:: forall abt m p typs args a
. ( ABT Term abt, EvaluationMonad abt m p
, typs ~ UnLCs args, args ~ LCs typs)
=> TermEvaluator abt m
-> PrimOp typs a
-> SArgs abt args
-> m (Whnf abt a)
evaluatePrimOp :: TermEvaluator abt m
-> PrimOp typs a -> SArgs abt args -> m (Whnf abt a)
evaluatePrimOp TermEvaluator abt m
evaluate_ = PrimOp typs a -> SArgs abt args -> m (Whnf abt a)
go
where
neu1 :: forall b c
. (abt '[] b -> abt '[] c)
-> abt '[] b
-> m (Whnf abt c)
neu1 :: (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] b -> abt '[] c
f abt '[] b
e = (abt '[] c -> Whnf abt c
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] c -> Whnf abt c)
-> (Whnf abt b -> abt '[] c) -> Whnf abt b -> Whnf abt c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] b -> abt '[] c
f (abt '[] b -> abt '[] c)
-> (Whnf abt b -> abt '[] b) -> Whnf abt b -> abt '[] c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Whnf abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf) (Whnf abt b -> Whnf abt c) -> m (Whnf abt b) -> m (Whnf abt c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e
neu2 :: forall b c d
. (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
neu2 :: (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b -> abt '[] c -> m (Whnf abt d)
neu2 abt '[] b -> abt '[] c -> abt '[] d
f abt '[] b
e1 abt '[] c
e2 = do abt '[] b
e1' <- Whnf abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf (Whnf abt b -> abt '[] b) -> m (Whnf abt b) -> m (abt '[] b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e1
abt '[] c
e2' <- Whnf abt c -> abt '[] c
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf (Whnf abt c -> abt '[] c) -> m (Whnf abt c) -> m (abt '[] c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] c -> m (Whnf abt c)
TermEvaluator abt m
evaluate_ abt '[] c
e2
Whnf abt d -> m (Whnf abt d)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt d -> m (Whnf abt d))
-> (abt '[] d -> Whnf abt d) -> abt '[] d -> m (Whnf abt d)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] d -> Whnf abt d
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] d -> m (Whnf abt d)) -> abt '[] d -> m (Whnf abt d)
forall a b. (a -> b) -> a -> b
$ abt '[] b -> abt '[] c -> abt '[] d
f abt '[] b
e1' abt '[] c
e2'
rr1 :: forall b b' c c'
. (Interp b b', Interp c c')
=> (b' -> c')
-> (abt '[] b -> abt '[] c)
-> abt '[] b
-> m (Whnf abt c)
rr1 :: (b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 b' -> c'
f' abt '[] b -> abt '[] c
f abt '[] b
e = do
Whnf abt b
w <- abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e
Whnf abt c -> m (Whnf abt c)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt c -> m (Whnf abt c)) -> Whnf abt c -> m (Whnf abt c)
forall a b. (a -> b) -> a -> b
$
case Whnf abt b
w of
Neutral abt '[] b
e' -> abt '[] c -> Whnf abt c
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] c -> Whnf abt c) -> abt '[] c -> Whnf abt c
forall a b. (a -> b) -> a -> b
$ abt '[] b -> abt '[] c
f abt '[] b
e'
Head_ Head abt b
v -> Head abt c -> Whnf abt c
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt c -> Whnf abt c)
-> (c' -> Head abt c) -> c' -> Whnf abt c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c' -> Head abt c
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
a' -> Head abt a
reflect (c' -> Whnf abt c) -> c' -> Whnf abt c
forall a b. (a -> b) -> a -> b
$ b' -> c'
f' (Head abt b -> b'
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt b
v)
rr2 :: forall b b' c c' d d'
. (Interp b b', Interp c c', Interp d d')
=> (b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 :: (b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 b' -> c' -> d'
f' abt '[] b -> abt '[] c -> abt '[] d
f abt '[] b
e1 abt '[] c
e2 = do
Whnf abt b
w1 <- abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e1
Whnf abt c
w2 <- abt '[] c -> m (Whnf abt c)
TermEvaluator abt m
evaluate_ abt '[] c
e2
Whnf abt d -> m (Whnf abt d)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt d -> m (Whnf abt d)) -> Whnf abt d -> m (Whnf abt d)
forall a b. (a -> b) -> a -> b
$
case Whnf abt b
w1 of
Neutral abt '[] b
e1' -> abt '[] d -> Whnf abt d
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] d -> Whnf abt d) -> abt '[] d -> Whnf abt d
forall a b. (a -> b) -> a -> b
$ abt '[] b -> abt '[] c -> abt '[] d
f abt '[] b
e1' (Whnf abt c -> abt '[] c
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt c
w2)
Head_ Head abt b
v1 ->
case Whnf abt c
w2 of
Neutral abt '[] c
e2' -> abt '[] d -> Whnf abt d
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] d -> Whnf abt d) -> abt '[] d -> Whnf abt d
forall a b. (a -> b) -> a -> b
$ abt '[] b -> abt '[] c -> abt '[] d
f (Whnf abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt b
w1) abt '[] c
e2'
Head_ Head abt c
v2 -> Head abt d -> Whnf abt d
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt d -> Whnf abt d)
-> (d' -> Head abt d) -> d' -> Whnf abt d
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d' -> Head abt d
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
a' -> Head abt a
reflect (d' -> Whnf abt d) -> d' -> Whnf abt d
forall a b. (a -> b) -> a -> b
$ b' -> c' -> d'
f' (Head abt b -> b'
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt b
v1) (Head abt c -> c'
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt c
v2)
primOp2_
:: forall b c d
. PrimOp '[ b, c ] d -> abt '[] b -> abt '[] c -> abt '[] d
primOp2_ :: PrimOp '[b, c] d -> abt '[] b -> abt '[] c -> abt '[] d
primOp2_ PrimOp '[b, c] d
o abt '[] b
e1 abt '[] c
e2 = Term abt d -> abt '[] d
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (PrimOp '[b, c] d -> SCon '[ '( '[], b), '( '[], c)] d
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
(a :: Hakaru).
(typs ~ UnLCs args, args ~ LCs typs) =>
PrimOp typs a -> SCon args a
PrimOp_ PrimOp '[b, c] d
o SCon '[ '( '[], b), '( '[], c)] d
-> SArgs abt '[ '( '[], b), '( '[], c)] -> Term abt d
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] b
e1 abt '[] b
-> SArgs abt '[ '( '[], c)] -> SArgs abt '[ '( '[], b), '( '[], c)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[] c
e2 abt '[] c -> SArgs abt '[] -> SArgs abt '[ '( '[], c)]
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)
go :: PrimOp typs a -> SArgs abt args -> m (Whnf abt a)
go PrimOp typs a
Not (e1 :* End) = (Bool -> Bool)
-> (abt '[] HBool -> abt '[] HBool)
-> abt '[] HBool
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 Bool -> Bool
not abt '[] HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] HBool -> abt '[] HBool
P.not abt vars a
abt '[] HBool
e1
go PrimOp typs a
Impl (e1 :* e2 :* End) = (Bool -> Bool -> Bool)
-> (abt '[] HBool -> abt '[] HBool -> abt '[] HBool)
-> abt '[] HBool
-> abt '[] HBool
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Bool -> Bool -> Bool
impl (PrimOp '[HBool, HBool] HBool
-> abt '[] HBool -> abt '[] HBool -> abt '[] HBool
forall (b :: Hakaru) (c :: Hakaru) (d :: Hakaru).
PrimOp '[b, c] d -> abt '[] b -> abt '[] c -> abt '[] d
primOp2_ PrimOp '[HBool, HBool] HBool
Impl) abt vars a
abt '[] HBool
e1 abt vars a
abt '[] HBool
e2
go PrimOp typs a
Diff (e1 :* e2 :* End) = (Bool -> Bool -> Bool)
-> (abt '[] HBool -> abt '[] HBool -> abt '[] HBool)
-> abt '[] HBool
-> abt '[] HBool
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Bool -> Bool -> Bool
diff (PrimOp '[HBool, HBool] HBool
-> abt '[] HBool -> abt '[] HBool -> abt '[] HBool
forall (b :: Hakaru) (c :: Hakaru) (d :: Hakaru).
PrimOp '[b, c] d -> abt '[] b -> abt '[] c -> abt '[] d
primOp2_ PrimOp '[HBool, HBool] HBool
Diff) abt vars a
abt '[] HBool
e1 abt vars a
abt '[] HBool
e2
go PrimOp typs a
Nand (e1 :* e2 :* End) = (Bool -> Bool -> Bool)
-> (abt '[] HBool -> abt '[] HBool -> abt '[] HBool)
-> abt '[] HBool
-> abt '[] HBool
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Bool -> Bool -> Bool
nand abt '[] HBool -> abt '[] HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] HBool -> abt '[] HBool -> abt '[] HBool
P.nand abt vars a
abt '[] HBool
e1 abt vars a
abt '[] HBool
e2
go PrimOp typs a
Nor (e1 :* e2 :* End) = (Bool -> Bool -> Bool)
-> (abt '[] HBool -> abt '[] HBool -> abt '[] HBool)
-> abt '[] HBool
-> abt '[] HBool
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Bool -> Bool -> Bool
nor abt '[] HBool -> abt '[] HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] HBool -> abt '[] HBool -> abt '[] HBool
P.nor abt vars a
abt '[] HBool
e1 abt vars a
abt '[] HBool
e2
go PrimOp typs a
Pi SArgs abt args
End = Whnf abt 'HProb -> m (Whnf abt 'HProb)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HProb -> m (Whnf abt 'HProb))
-> Whnf abt 'HProb -> m (Whnf abt 'HProb)
forall a b. (a -> b) -> a -> b
$ abt '[] 'HProb -> Whnf abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(RealProb a, ABT Term abt) =>
abt '[] a
P.pi
go PrimOp typs a
Sin (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.sin abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Cos (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.cos abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Tan (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.tan abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Asin (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.asin abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Acos (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.acos abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Atan (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.atan abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Sinh (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.sinh abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Cosh (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.cosh abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Tanh (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.tanh abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Asinh (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.asinh abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Acosh (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.acosh abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Atanh (e1 :* End) = (abt '[] 'HReal -> abt '[] 'HReal)
-> abt '[] 'HReal -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal
P.atanh abt vars a
abt '[] 'HReal
e1
go PrimOp typs a
Floor (e1 :* End) = (abt '[] 'HProb -> abt '[] 'HNat)
-> abt '[] 'HProb -> m (Whnf abt 'HNat)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HProb -> abt '[] 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HNat
P.floor abt vars a
abt '[] 'HProb
e1
go PrimOp typs a
RealPow (e1 :* e2 :* End) = (abt '[] 'HProb -> abt '[] a -> abt '[] 'HProb)
-> abt '[] 'HProb -> abt '[] a -> m (Whnf abt 'HProb)
forall (b :: Hakaru) (c :: Hakaru) (d :: Hakaru).
(abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b -> abt '[] c -> m (Whnf abt d)
neu2 abt '[] 'HProb -> abt '[] a -> abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(RealProb a, ABT Term abt) =>
abt '[] 'HProb -> abt '[] a -> abt '[] 'HProb
(P.**) abt vars a
abt '[] 'HProb
e1 abt vars a
abt '[] a
e2
go PrimOp typs a
Choose (e1 :* e2 :* End) = (abt '[] 'HNat -> abt '[] 'HNat -> abt '[] 'HNat)
-> abt '[] 'HNat -> abt '[] 'HNat -> m (Whnf abt 'HNat)
forall (b :: Hakaru) (c :: Hakaru) (d :: Hakaru).
(abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b -> abt '[] c -> m (Whnf abt d)
neu2 (abt '[] 'HNat -> abt '[] 'HNat -> abt '[] 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HNat -> abt '[] 'HNat -> abt '[] 'HNat
P.choose) abt vars a
abt '[] 'HNat
e1 abt vars a
abt '[] 'HNat
e2
go PrimOp typs a
Exp (e1 :* End) = (abt '[] a -> abt '[] 'HProb) -> abt '[] a -> m (Whnf abt 'HProb)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] a -> abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(RealProb a, ABT Term abt) =>
abt '[] a -> abt '[] 'HProb
P.exp abt vars a
abt '[] a
e1
go PrimOp typs a
Log (e1 :* End) = (abt '[] 'HProb -> abt '[] 'HReal)
-> abt '[] 'HProb -> m (Whnf abt 'HReal)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
P.log abt vars a
abt '[] 'HProb
e1
go (Infinity HIntegrable a
h) SArgs abt args
End =
case HIntegrable a
h of
HIntegrable a
HIntegrable_Nat -> Whnf abt 'HNat -> m (Whnf abt 'HNat)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HNat -> m (Whnf abt 'HNat))
-> (abt '[] 'HNat -> Whnf abt 'HNat)
-> abt '[] 'HNat
-> m (Whnf abt 'HNat)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] 'HNat -> Whnf abt 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> m (Whnf abt a)) -> abt '[] a -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ PrimOp '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
PrimOp '[] a -> abt '[] a
P.primOp0_ (HIntegrable a -> PrimOp '[] a
forall (a :: Hakaru). HIntegrable a -> PrimOp '[] a
Infinity HIntegrable a
h)
HIntegrable a
HIntegrable_Prob -> Whnf abt 'HProb -> m (Whnf abt 'HProb)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt 'HProb -> m (Whnf abt 'HProb))
-> Whnf abt 'HProb -> m (Whnf abt 'HProb)
forall a b. (a -> b) -> a -> b
$ abt '[] 'HProb -> Whnf abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(Integrable a, ABT Term abt) =>
abt '[] a
P.infinity
go PrimOp typs a
GammaFunc (e1 :* End) = (abt '[] a -> abt '[] 'HProb) -> abt '[] a -> m (Whnf abt 'HProb)
forall (b :: Hakaru) (c :: Hakaru).
(abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
neu1 abt '[] a -> abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(RealProb a, ABT Term abt) =>
abt '[] a -> abt '[] 'HProb
P.gammaFunc abt vars a
abt '[] a
e1
go PrimOp typs a
BetaFunc (e1 :* e2 :* End) = (abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb)
-> abt '[] 'HProb -> abt '[] 'HProb -> m (Whnf abt 'HProb)
forall (b :: Hakaru) (c :: Hakaru) (d :: Hakaru).
(abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b -> abt '[] c -> m (Whnf abt d)
neu2 abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
P.betaFunc abt vars a
abt '[] 'HProb
e1 abt vars a
abt '[] 'HProb
e2
go (Equal HEq a
theEq) (e1 :* e2 :* End) = HEq a -> abt '[] a -> abt '[] a -> m (Whnf abt HBool)
forall (b :: Hakaru).
HEq b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrEqual HEq a
theEq abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
go (Less HOrd a
theOrd) (e1 :* e2 :* End) = HOrd a -> abt '[] a -> abt '[] a -> m (Whnf abt HBool)
forall (b :: Hakaru).
HOrd b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrLess HOrd a
theOrd abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
go (NatPow HSemiring a
theSemi) (e1 :* e2 :* End) =
case HSemiring a
theSemi of
HSemiring a
HSemiring_Nat -> (Natural -> Natural -> Natural)
-> (abt '[] a -> abt '[] 'HNat -> abt '[] a)
-> abt '[] a
-> abt '[] 'HNat
-> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 (\Natural
v1 Natural
v2 -> Natural
v1 Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural -> Integer
fromNatural Natural
v2) abt '[] a -> abt '[] 'HNat -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] 'HNat -> abt '[] a
(P.^) abt vars a
abt '[] a
e1 abt vars a
abt '[] 'HNat
e2
HSemiring a
HSemiring_Int -> (Integer -> Natural -> Integer)
-> (abt '[] a -> abt '[] 'HNat -> abt '[] a)
-> abt '[] a
-> abt '[] 'HNat
-> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 (\Integer
v1 Natural
v2 -> Integer
v1 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural -> Integer
fromNatural Natural
v2) abt '[] a -> abt '[] 'HNat -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] 'HNat -> abt '[] a
(P.^) abt vars a
abt '[] a
e1 abt vars a
abt '[] 'HNat
e2
HSemiring a
HSemiring_Prob -> (NonNegativeRational -> Natural -> NonNegativeRational)
-> (abt '[] a -> abt '[] 'HNat -> abt '[] a)
-> abt '[] a
-> abt '[] 'HNat
-> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 (\NonNegativeRational
v1 Natural
v2 -> NonNegativeRational
v1 NonNegativeRational -> Integer -> NonNegativeRational
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural -> Integer
fromNatural Natural
v2) abt '[] a -> abt '[] 'HNat -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] 'HNat -> abt '[] a
(P.^) abt vars a
abt '[] a
e1 abt vars a
abt '[] 'HNat
e2
HSemiring a
HSemiring_Real -> (Rational -> Natural -> Rational)
-> (abt '[] a -> abt '[] 'HNat -> abt '[] a)
-> abt '[] a
-> abt '[] 'HNat
-> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 (\Rational
v1 Natural
v2 -> Rational
v1 Rational -> Integer -> Rational
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural -> Integer
fromNatural Natural
v2) abt '[] a -> abt '[] 'HNat -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] 'HNat -> abt '[] a
(P.^) abt vars a
abt '[] a
e1 abt vars a
abt '[] 'HNat
e2
go (Negate HRing a
theRing) (e1 :* End) =
case HRing a
theRing of
HRing a
HRing_Int -> (Integer -> Integer)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 Integer -> Integer
forall a. Num a => a -> a
negate abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a
P.negate abt vars a
abt '[] a
e1
HRing a
HRing_Real -> (Rational -> Rational)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 Rational -> Rational
forall a. Num a => a -> a
negate abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a
P.negate abt vars a
abt '[] a
e1
go (Abs HRing a
theRing) (e1 :* End) =
case HRing a
theRing of
HRing a
HRing_Int -> (Integer -> Natural)
-> (abt '[] a -> abt '[] 'HNat) -> abt '[] a -> m (Whnf abt 'HNat)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 (Integer -> Natural
unsafeNatural (Integer -> Natural) -> (Integer -> Integer) -> Integer -> Natural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Integer
forall a. Num a => a -> a
abs) abt '[] a -> abt '[] 'HNat
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] (NonNegative a)
P.abs_ abt vars a
abt '[] a
e1
HRing a
HRing_Real -> (Rational -> NonNegativeRational)
-> (abt '[] a -> abt '[] 'HProb)
-> abt '[] a
-> m (Whnf abt 'HProb)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 (Rational -> NonNegativeRational
unsafeNonNegativeRational (Rational -> NonNegativeRational)
-> (Rational -> Rational) -> Rational -> NonNegativeRational
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Rational -> Rational
forall a. Num a => a -> a
abs) abt '[] a -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] (NonNegative a)
P.abs_ abt vars a
abt '[] a
e1
go (Signum HRing a
theRing) (e1 :* End) =
case HRing a
theRing of
HRing a
HRing_Int -> (Integer -> Integer)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 Integer -> Integer
forall a. Num a => a -> a
signum abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a
P.signum abt vars a
abt '[] a
e1
HRing a
HRing_Real -> (Rational -> Rational)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 Rational -> Rational
forall a. Num a => a -> a
signum abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a
P.signum abt vars a
abt '[] a
e1
go (Recip HFractional a
theFractional) (e1 :* End) =
case HFractional a
theFractional of
HFractional a
HFractional_Prob -> (NonNegativeRational -> NonNegativeRational)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 NonNegativeRational -> NonNegativeRational
forall a. Fractional a => a -> a
recip abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a
P.recip abt vars a
abt '[] a
e1
HFractional a
HFractional_Real -> (Rational -> Rational)
-> (abt '[] a -> abt '[] a) -> abt '[] a -> m (Whnf abt a)
forall (b :: Hakaru) b' (c :: Hakaru) c'.
(Interp b b', Interp c c') =>
(b' -> c')
-> (abt '[] b -> abt '[] c) -> abt '[] b -> m (Whnf abt c)
rr1 Rational -> Rational
forall a. Fractional a => a -> a
recip abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a
P.recip abt vars a
abt '[] a
e1
go (NatRoot HRadical a
theRadical) (e1 :* e2 :* End) =
case HRadical a
theRadical of
HRadical a
HRadical_Prob -> (abt '[] a -> abt '[] 'HNat -> abt '[] a)
-> abt '[] a -> abt '[] 'HNat -> m (Whnf abt a)
forall (b :: Hakaru) (c :: Hakaru) (d :: Hakaru).
(abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b -> abt '[] c -> m (Whnf abt d)
neu2 ((abt '[] 'HNat -> abt '[] a -> abt '[] a)
-> abt '[] a -> abt '[] 'HNat -> abt '[] a
forall a b c. (a -> b -> c) -> b -> a -> c
flip abt '[] 'HNat -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRadical_ a) =>
abt '[] 'HNat -> abt '[] a -> abt '[] a
P.thRootOf) abt vars a
abt '[] a
e1 abt vars a
abt '[] 'HNat
e2
go PrimOp typs a
op SArgs abt args
_ = [Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error ([Char] -> m (Whnf abt a)) -> [Char] -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO: evaluatePrimOp{" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PrimOp typs a -> [Char]
forall a. Show a => a -> [Char]
show PrimOp typs a
op [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"}"
rrEqual
:: forall b. HEq b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrEqual :: HEq b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrEqual HEq b
theEq =
case HEq b
theEq of
HEq b
HEq_Nat -> (Natural -> Natural -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
(==) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HEq_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.==)
HEq b
HEq_Int -> (Integer -> Integer -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HEq_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.==)
HEq b
HEq_Prob -> (NonNegativeRational -> NonNegativeRational -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 NonNegativeRational -> NonNegativeRational -> Bool
forall a. Eq a => a -> a -> Bool
(==) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HEq_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.==)
HEq b
HEq_Real -> (Rational -> Rational -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
(==) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HEq_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.==)
HEq_Array HEq a
_ -> [Char] -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: rrEqual{HEq_Array}"
HEq b
HEq_Bool -> (Bool -> Bool -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HEq_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.==)
HEq b
HEq_Unit -> (() -> () -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 () -> () -> Bool
forall a. Eq a => a -> a -> Bool
(==) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HEq_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.==)
HEq_Pair HEq a
aEq HEq b
bEq ->
\abt '[] b
e1 abt '[] b
e2 -> do
Whnf abt b
w1 <- abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e1
Whnf abt b
w2 <- abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e2
case Whnf abt b
w1 of
Neutral abt '[] b
e1' ->
Whnf abt HBool -> m (Whnf abt HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt HBool -> m (Whnf abt HBool))
-> (abt '[] HBool -> Whnf abt HBool)
-> abt '[] HBool
-> m (Whnf abt HBool)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral
(abt '[] HBool -> m (Whnf abt HBool))
-> abt '[] HBool -> m (Whnf abt HBool)
forall a b. (a -> b) -> a -> b
$ PrimOp '[b, b] HBool -> abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
PrimOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] c
P.primOp2_ (HEq b -> PrimOp '[b, b] HBool
forall (a :: Hakaru). HEq a -> PrimOp '[a, a] HBool
Equal HEq b
theEq) abt '[] b
e1' (Whnf abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt b
w2)
Head_ Head abt b
v1 ->
case Whnf abt b
w2 of
Neutral abt '[] b
e2' ->
Whnf abt HBool -> m (Whnf abt HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt HBool -> m (Whnf abt HBool))
-> (abt '[] HBool -> Whnf abt HBool)
-> abt '[] HBool
-> m (Whnf abt HBool)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral
(abt '[] HBool -> m (Whnf abt HBool))
-> abt '[] HBool -> m (Whnf abt HBool)
forall a b. (a -> b) -> a -> b
$ PrimOp '[b, b] HBool -> abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
PrimOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] c
P.primOp2_ (HEq b -> PrimOp '[b, b] HBool
forall (a :: Hakaru). HEq a -> PrimOp '[a, a] HBool
Equal HEq b
theEq) (Head abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt b
v1) abt '[] b
e2'
Head_ Head abt b
v2 -> do
let (abt '[] a
v1a, abt '[] b
v1b) = Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt b
Head abt (HPair a b)
v1
let (abt '[] a
v2a, abt '[] b
v2b) = Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt b
Head abt (HPair a b)
v2
Whnf abt HBool
wa <- HEq a -> abt '[] a -> abt '[] a -> m (Whnf abt HBool)
forall (b :: Hakaru).
HEq b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrEqual HEq a
aEq abt '[] a
v1a abt '[] a
v2a
Whnf abt HBool
wb <- HEq b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
forall (b :: Hakaru).
HEq b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrEqual HEq b
bEq abt '[] b
v1b abt '[] b
v2b
Whnf abt HBool -> m (Whnf abt HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt HBool -> m (Whnf abt HBool))
-> Whnf abt HBool -> m (Whnf abt HBool)
forall a b. (a -> b) -> a -> b
$
case Whnf abt HBool
wa of
Neutral abt '[] HBool
ea ->
case Whnf abt HBool
wb of
Neutral abt '[] HBool
eb -> abt '[] HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] HBool
ea abt '[] HBool -> abt '[] HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] HBool -> abt '[] HBool -> abt '[] HBool
P.&& abt '[] HBool
eb)
Head_ Head abt HBool
vb
| Head abt HBool -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt HBool
vb -> Whnf abt HBool
wa
| Bool
otherwise -> Head abt HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt HBool -> Whnf abt HBool)
-> Head abt HBool -> Whnf abt HBool
forall a b. (a -> b) -> a -> b
$ Datum (abt '[]) (HData' ('TyCon "Bool"))
-> Head abt (HData' ('TyCon "Bool"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Bool"))
forall (ast :: Hakaru -> *). Datum ast HBool
dFalse
Head_ Head abt HBool
va
| Head abt HBool -> Bool
forall (a :: Hakaru) a' (abt :: [Hakaru] -> Hakaru -> *).
(Interp a a', ABT Term abt) =>
Head abt a -> a'
reify Head abt HBool
va -> Whnf abt HBool
wb
| Bool
otherwise -> Head abt HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt HBool -> Whnf abt HBool)
-> Head abt HBool -> Whnf abt HBool
forall a b. (a -> b) -> a -> b
$ Datum (abt '[]) (HData' ('TyCon "Bool"))
-> Head abt (HData' ('TyCon "Bool"))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' ('TyCon "Bool"))
forall (ast :: Hakaru -> *). Datum ast HBool
dFalse
HEq_Either HEq a
_ HEq b
_ -> [Char] -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: rrEqual{HEq_Either}"
rrLess
:: forall b. HOrd b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrLess :: HOrd b -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
rrLess HOrd b
theOrd =
case HOrd b
theOrd of
HOrd b
HOrd_Nat -> (Natural -> Natural -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
(<) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.<)
HOrd b
HOrd_Int -> (Integer -> Integer -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.<)
HOrd b
HOrd_Prob -> (NonNegativeRational -> NonNegativeRational -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 NonNegativeRational -> NonNegativeRational -> Bool
forall a. Ord a => a -> a -> Bool
(<) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.<)
HOrd b
HOrd_Real -> (Rational -> Rational -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
(<) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.<)
HOrd_Array HOrd a
_ -> [Char] -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: rrLess{HOrd_Array}"
HOrd b
HOrd_Bool -> (Bool -> Bool -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.<)
HOrd b
HOrd_Unit -> (() -> () -> Bool)
-> (abt '[] b -> abt '[] b -> abt '[] HBool)
-> abt '[] b
-> abt '[] b
-> m (Whnf abt HBool)
forall (b :: Hakaru) b' (c :: Hakaru) c' (d :: Hakaru) d'.
(Interp b b', Interp c c', Interp d d') =>
(b' -> c' -> d')
-> (abt '[] b -> abt '[] c -> abt '[] d)
-> abt '[] b
-> abt '[] c
-> m (Whnf abt d)
rr2 () -> () -> Bool
forall a. Ord a => a -> a -> Bool
(<) abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
(P.<)
HOrd_Pair HOrd a
_ HOrd b
_ ->
\abt '[] b
e1 abt '[] b
e2 -> do
Whnf abt b
w1 <- abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e1
Whnf abt b
w2 <- abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_ abt '[] b
e2
case Whnf abt b
w1 of
Neutral abt '[] b
e1' ->
Whnf abt HBool -> m (Whnf abt HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt HBool -> m (Whnf abt HBool))
-> (abt '[] HBool -> Whnf abt HBool)
-> abt '[] HBool
-> m (Whnf abt HBool)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral
(abt '[] HBool -> m (Whnf abt HBool))
-> abt '[] HBool -> m (Whnf abt HBool)
forall a b. (a -> b) -> a -> b
$ PrimOp '[b, b] HBool -> abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
PrimOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] c
P.primOp2_ (HOrd b -> PrimOp '[b, b] HBool
forall (a :: Hakaru). HOrd a -> PrimOp '[a, a] HBool
Less HOrd b
theOrd) abt '[] b
e1' (Whnf abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt b
w2)
Head_ Head abt b
v1 ->
case Whnf abt b
w2 of
Neutral abt '[] b
e2' ->
Whnf abt HBool -> m (Whnf abt HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt HBool -> m (Whnf abt HBool))
-> (abt '[] HBool -> Whnf abt HBool)
-> abt '[] HBool
-> m (Whnf abt HBool)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] HBool -> Whnf abt HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral
(abt '[] HBool -> m (Whnf abt HBool))
-> abt '[] HBool -> m (Whnf abt HBool)
forall a b. (a -> b) -> a -> b
$ PrimOp '[b, b] HBool -> abt '[] b -> abt '[] b -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
PrimOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] c
P.primOp2_ (HOrd b -> PrimOp '[b, b] HBool
forall (a :: Hakaru). HOrd a -> PrimOp '[a, a] HBool
Less HOrd b
theOrd) (Head abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt b
v1) abt '[] b
e2'
Head_ Head abt b
v2 -> do
let (abt '[] a
_, abt '[] b
_) = Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt b
Head abt (HPair a b)
v1
let (abt '[] a
_, abt '[] b
_) = Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt b
Head abt (HPair a b)
v2
[Char] -> m (Whnf abt HBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: rrLess{HOrd_Pair}"
HOrd_Either HOrd a
_ HOrd b
_ -> [Char] -> abt '[] b -> abt '[] b -> m (Whnf abt HBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: rrLess{HOrd_Either}"