{-# LANGUAGE CPP
           , GADTs
           , DataKinds
           , KindSignatures
           , MultiParamTypeClasses
           , FunctionalDependencies
           , ScopedTypeVariables
           , FlexibleContexts
           , Rank2Types
           , TypeSynonymInstances
           , FlexibleInstances
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.04.28
-- |
-- Module      :  Language.Hakaru.Evaluation.Lazy
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Lazy partial evaluation.
--
-- BUG: completely gave up on structure sharing. Need to add that
-- back in. cf., @gvidal-lopstr07lncs.pdf@ for an approach much
-- like my old one.
----------------------------------------------------------------
module Language.Hakaru.Evaluation.Lazy
    ( evaluate
    -- ** Helper functions
    , evaluateNaryOp
    , evaluatePrimOp
    , evaluateArrayOp
    -- ** Helpers that should really go away
    , 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
{-
-- BUG: can't import this because of cyclic dependency
import qualified Language.Hakaru.Expect         as E
-}

#ifdef __TRACE_DISINTEGRATE__
import Language.Hakaru.Pretty.Haskell (pretty)
import Debug.Trace (trace)
#endif

----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: (eventually) accept an argument dictating the evaluation
-- strategy (HNF, WHNF, full-beta NF,...). The strategy value should
-- probably be a family of singletons, where the type-level strategy
-- @s@ is also an index on the 'Context' and (the renamed) 'Whnf'.
-- That way we don't need to define a bunch of variant 'Context',
-- 'Statement', and 'Whnf' data types; but rather can use indexing
-- to select out subtypes of the generic versions.


-- | Lazy partial evaluation with some given \"perform\" and
-- \"evaluateCase\" functions. N.B., if @p ~ 'Pure@ then the
-- \"perform\" function will never be called.
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
        -- Things which are already WHNFs
        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
        -- We don't bother evaluating these, even though we could...
        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
            --return . Head_ $ WSummate   e1 e2 e3


        -- Everything else needs some evaluation

        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)   =
                -- call-by-name:
                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

        -- TODO: will maybe clean up the code to map 'evaluate' over @es@ before calling the evaluateFooOp helpers?
        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
        -- Bucket_ _ _ _ _ -> error "What oh what to do with a Bucket here?"

        SCon args a
_ :$ SArgs abt args
_ -> [Char] -> m (Whnf abt a)
forall a. HasCallStack => [Char] -> a
error [Char]
"evaluate: the impossible happened"


----------------------------------------------------------------
-- BUG: need to improve the types so they can capture polymorphic data types
-- BUG: this is a **really gross** hack. If we can avoid it, we should!!!
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}"
    --reify (WSummate    _ _ _) = error "TODO: reify{WSummate}"

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)

-- HACK: this requires -XTypeSynonymInstances and -XFlexibleInstances
-- This instance does seem to work; albeit it's trivial...
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"

-- HACK: this requires -XTypeSynonymInstances and -XFlexibleInstances
-- This instance also seems to work...
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"


-- TODO: can't we just use 'viewHeadDatum' and match on that?
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
{-
instance Interp (HPair a b) (abt '[] a, abt '[] b) where
    reflect (a,b) = P.pair a b
    reify = reifyPair

instance Interp (HEither a b) (Either (abt '[] a) (abt '[] b)) where
    reflect (Left  a) = P.left  a
    reflect (Right b) = P.right b
    reify =

instance Interp (HMaybe a) (Maybe (abt '[] a)) where
    reflect Nothing  = P.nothing
    reflect (Just a) = P.just a
    reify =

data ListHead (a :: Hakaru)
    = NilHead
    | ConsHead (abt '[] a) (abt '[] (HList a)) -- modulo scoping of @abt@

instance Interp (HList a) (ListHead a) where
    reflect []     = P.nil
    reflect (x:xs) = P.cons x xs
    reify =
-}


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)

-- BUG: no Floating instance for LogFloat (nor NonNegativeRational), so can't actually use this...
-- natRoot :: (Floating a) => a -> Nat -> a
-- natRoot x y = x ** recip (fromIntegral (fromNat 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
    -- TODO: there's got to be a more efficient way to do this...
    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 -- Avoid empty naryOps
            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 -- Avoid singleton naryOps
                | 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 =
        -- TODO: immediately return @ws@ if @w1 == identityElement o@ (whenever identityElement is defined)
        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

    -- TODO: move this off to Prelude.hs or somewhere...
    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)) -- no identity in general (but we could do it by cases...)
        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)) -- no identity in general (but we could do it by cases...)
        -- TODO: figure out how to reuse 'P.zero_' and 'P.one_' here; requires converting thr @(syn . Literal_)@ into @(Head_ . WLiteral)@. Maybe we should change 'P.zero_' and 'P.one_' so they just return the 'Literal' itself rather than the @abt@?
        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))

    -- | The evaluation interpretation of each NaryOp
    evalOp
        :: (ABT Term abt)
        => NaryOp a
        -> Head abt a
        -> Head abt a
        -> Head abt a
    -- TODO: something more efficient\/direct if we can...
    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 (Min  _) = \v1 v2 -> reflect (reify v1 `min` reify v2)
    evalOp (Max  _) = \v1 v2 -> reflect (reify v1 `max` reify v2)
    evalOp (Sum  _) = \v1 v2 -> reflect (reify v1 + reify v2)
    evalOp (Prod _) = \v1 v2 -> reflect (reify v1 * reify v2)
    -}
    -- HACK: this is just to have something to test. We really should reduce\/remove all this boilerplate...
    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

    -- TODO: even if only one of the arguments is a literal, if that literal is zero\/one, then we can still partially evaluate it. (As is done in the old finally-tagless code)
    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 -- idxCode :: abt '[] ('HArray a) -> abt '[] 'HNat -> abt '[] a
            -- idxCode a i = Neutral $ syn (ArrayOp_ o :$ a :* i :* End)
        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}"

----------------------------------------------------------------
-- TODO: maybe we should adjust 'Whnf' to have a third option for
-- closed terms of the atomic\/literal types, so that we can avoid
-- reducing them just yet. Of course, we'll have to reduce them
-- eventually, but we can leave that for the runtime evaluation or
-- Maple or whatever. These are called \"annotated\" terms in Fischer
-- et al 2008 (though they allow anything to be annotated, not just
-- closed terms of atomic type).
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
    -- HACK: we don't have any way of saying these functions haven't reduced even though it's not actually a neutral term.
    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)

    -- TODO: something more efficient\/direct if we can...
    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

    -- HACK: we don't have a way of saying that 'Pi' (or 'Infinity',...) is in fact a head; so we're forced to call it neutral which is a lie. We should add constructor(s) to 'Head' to cover these magic constants; probably grouped together under a single constructor called something like @Constant@. Maybe should group them like that in the AST as well?
    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

    -- We treat trig functions as strict, thus forcing their
    -- arguments; however, to avoid fuzz issues we don't actually
    -- evaluate the trig functions.
    --
    -- HACK: we might should have some other way to make these
    -- 'Whnf' rather than calling them neutral terms; since they
    -- aren't, in fact, neutral!
    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

    -- TODO: deal with how we have better types for these three ops than Haskell does...
    -- go RealPow   (e1 :* e2 :* End) = rr2 (**) (P.**) e1 e2
    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

    -- HACK: these aren't actually neutral!
    -- BUG: we should try to cancel out @(exp . log)@ and @(log . exp)@
    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

    -- HACK: these aren't actually neutral!
    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 (NatRoot theRadical) (e1 :* e2 :* End) =
        case theRadical of
        HRadical_Prob -> rr2 natRoot (flip P.thRootOf) e1 e2
    go (Erf theContinuous) (e1 :* End) =
        case theContinuous of
        HContinuous_Prob -> rr1 erf P.erf e1
        HContinuous_Real -> rr1 erf P.erf e1
    -}
    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}"
                            -- BUG: The obvious recursion won't work because we need to know when the first components are equal before recursing (to implement lexicographic ordering). We really need a ternary comparison operator like 'compare'.
        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}"


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