{-# LANGUAGE CPP
           , OverloadedStrings
           , DataKinds
           , KindSignatures
           , GADTs
           , LambdaCase
           , PolyKinds
           , RankNTypes
           #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Parser.SymbolResolve
    (
      resolveAST, resolveAST', makeName, fromVarSet
    ) where

import Data.Text hiding (concat, map, maximum, foldr1, singleton)
#if __GLASGOW_HASKELL__ < 710
import Data.Functor                     ((<$>))
import Control.Applicative              ((<*>))
#endif
import Control.Monad.Trans.State.Strict (State, state, evalState)
import Control.Monad (join)

import qualified Data.Number.Nat                 as N
import qualified Data.IntMap                     as IM
import           Data.Foldable                   as F
import           Data.Ratio
import           Data.Proxy                      (KProxy(..))
import           Data.List.NonEmpty              as L (NonEmpty(..), fromList)
import           Language.Hakaru.Types.Sing
import           Language.Hakaru.Types.Coercion
import           Language.Hakaru.Types.DataKind  hiding (Symbol)
import           Language.Hakaru.Types.HClasses
import qualified Language.Hakaru.Syntax.AST      as T
import           Language.Hakaru.Syntax.ABT      hiding (fromVarSet)
import           Language.Hakaru.Syntax.IClasses
import           Language.Hakaru.Syntax.Variable ()
import qualified Language.Hakaru.Parser.AST   as U
import           Language.Hakaru.Evaluation.Coalesce (coalesce)
import qualified Language.Hakaru.Syntax.Prelude  as P

data Symbol a
    = TLam (a -> Symbol a)
    | TNeu a

data Symbol' a
    = TLam' ([a] -> a)
    | TNeu' a

singleton :: a -> L.NonEmpty a
singleton :: a -> NonEmpty a
singleton a
x = a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| []

primPat :: [(Text, Symbol' U.Pattern)]
primPat :: [(Text, Symbol' Pattern)]
primPat =
    [ (Text
"left",    ([Pattern] -> Pattern) -> Symbol' Pattern
forall a. ([a] -> a) -> Symbol' a
TLam' (([Pattern] -> Pattern) -> Symbol' Pattern)
-> ([Pattern] -> Pattern) -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ \ [Pattern
a] ->
        Text -> PCode -> Pattern
U.PDatum Text
"left" (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Pattern) -> PStruct -> Pattern
forall a b. (a -> b) -> a -> b
$
            Pattern -> PFun
U.PKonst Pattern
a PFun -> PStruct -> PStruct
`U.PEt` PStruct
U.PDone)
    , (Text
"right",   ([Pattern] -> Pattern) -> Symbol' Pattern
forall a. ([a] -> a) -> Symbol' a
TLam' (([Pattern] -> Pattern) -> Symbol' Pattern)
-> ([Pattern] -> Pattern) -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ \ [Pattern
b] ->
        Text -> PCode -> Pattern
U.PDatum Text
"right" (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PCode -> PCode
U.PInr (PCode -> PCode) -> (PStruct -> PCode) -> PStruct -> PCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Pattern) -> PStruct -> Pattern
forall a b. (a -> b) -> a -> b
$
            Pattern -> PFun
U.PKonst Pattern
b PFun -> PStruct -> PStruct
`U.PEt` PStruct
U.PDone)
    , (Text
"true",    Pattern -> Symbol' Pattern
forall a. a -> Symbol' a
TNeu' (Pattern -> Symbol' Pattern)
-> (PStruct -> Pattern) -> PStruct -> Symbol' Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> PCode -> Pattern
U.PDatum Text
"true"  (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Symbol' Pattern) -> PStruct -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ PStruct
U.PDone)
    , (Text
"false",   Pattern -> Symbol' Pattern
forall a. a -> Symbol' a
TNeu' (Pattern -> Symbol' Pattern)
-> (PStruct -> Pattern) -> PStruct -> Symbol' Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> PCode -> Pattern
U.PDatum Text
"false" (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PCode -> PCode
U.PInr (PCode -> PCode) -> (PStruct -> PCode) -> PStruct -> PCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Symbol' Pattern) -> PStruct -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ PStruct
U.PDone)
    , (Text
"unit",    Pattern -> Symbol' Pattern
forall a. a -> Symbol' a
TNeu' (Pattern -> Symbol' Pattern)
-> (PStruct -> Pattern) -> PStruct -> Symbol' Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> PCode -> Pattern
U.PDatum Text
"unit"  (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Symbol' Pattern) -> PStruct -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ PStruct
U.PDone)
    , (Text
"pair",    ([Pattern] -> Pattern) -> Symbol' Pattern
forall a. ([a] -> a) -> Symbol' a
TLam' (([Pattern] -> Pattern) -> Symbol' Pattern)
-> ([Pattern] -> Pattern) -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ \[Pattern]
es -> (Pattern -> Pattern -> Pattern) -> [Pattern] -> Pattern
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
F.foldr1 Pattern -> Pattern -> Pattern
pairPat [Pattern]
es)
    , (Text
"just",    ([Pattern] -> Pattern) -> Symbol' Pattern
forall a. ([a] -> a) -> Symbol' a
TLam' (([Pattern] -> Pattern) -> Symbol' Pattern)
-> ([Pattern] -> Pattern) -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ \ [Pattern
a] ->
        Text -> PCode -> Pattern
U.PDatum Text
"just" (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PCode -> PCode
U.PInr (PCode -> PCode) -> (PStruct -> PCode) -> PStruct -> PCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Pattern) -> PStruct -> Pattern
forall a b. (a -> b) -> a -> b
$
            Pattern -> PFun
U.PKonst Pattern
a PFun -> PStruct -> PStruct
`U.PEt` PStruct
U.PDone)
    , (Text
"nothing", ([Pattern] -> Pattern) -> Symbol' Pattern
forall a. ([a] -> a) -> Symbol' a
TLam' (([Pattern] -> Pattern) -> Symbol' Pattern)
-> ([Pattern] -> Pattern) -> Symbol' Pattern
forall a b. (a -> b) -> a -> b
$ \ [] ->
        Text -> PCode -> Pattern
U.PDatum Text
"nothing" (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct -> PCode
U.PInl (PStruct -> Pattern) -> PStruct -> Pattern
forall a b. (a -> b) -> a -> b
$ PStruct
U.PDone)
    ]

pairPat :: U.Pattern -> U.Pattern -> U.Pattern
pairPat :: Pattern -> Pattern -> Pattern
pairPat Pattern
a Pattern
b =
    Text -> PCode -> Pattern
U.PDatum Text
"pair" (PCode -> Pattern) -> (PStruct -> PCode) -> PStruct -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  PStruct -> PCode
U.PInl (PStruct -> Pattern) -> PStruct -> Pattern
forall a b. (a -> b) -> a -> b
$
    Pattern -> PFun
U.PKonst Pattern
a PFun -> PStruct -> PStruct
`U.PEt` Pattern -> PFun
U.PKonst Pattern
b PFun -> PStruct -> PStruct
`U.PEt` PStruct
U.PDone

primTypes :: [(Text, Symbol' U.SSing)]
primTypes :: [(Text, Symbol' SSing)]
primTypes =
    [ (Text
"nat",     SSing -> Symbol' SSing
forall a. a -> Symbol' a
TNeu' (SSing -> Symbol' SSing) -> SSing -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ Sing 'HNat -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing 'HNat
SNat)
    , (Text
"int",     SSing -> Symbol' SSing
forall a. a -> Symbol' a
TNeu' (SSing -> Symbol' SSing) -> SSing -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ Sing 'HInt -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing 'HInt
SInt)
    , (Text
"prob",    SSing -> Symbol' SSing
forall a. a -> Symbol' a
TNeu' (SSing -> Symbol' SSing) -> SSing -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ Sing 'HProb -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing 'HProb
SProb)
    , (Text
"real",    SSing -> Symbol' SSing
forall a. a -> Symbol' a
TNeu' (SSing -> Symbol' SSing) -> SSing -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ Sing 'HReal -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing 'HReal
SReal)
    , (Text
"unit",    SSing -> Symbol' SSing
forall a. a -> Symbol' a
TNeu' (SSing -> Symbol' SSing) -> SSing -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ Sing HUnit -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing HUnit
sUnit)
    , (Text
"bool",    SSing -> Symbol' SSing
forall a. a -> Symbol' a
TNeu' (SSing -> Symbol' SSing) -> SSing -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ Sing HBool -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing HBool
sBool)
    , (Text
"array",   ([SSing] -> SSing) -> Symbol' SSing
forall a. ([a] -> a) -> Symbol' a
TLam' (([SSing] -> SSing) -> Symbol' SSing)
-> ([SSing] -> SSing) -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ \ [U.SSing Sing a
a] -> Sing ('HArray a) -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing (Sing ('HArray a) -> SSing) -> Sing ('HArray a) -> SSing
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray Sing a
a)
    , (Text
"measure", ([SSing] -> SSing) -> Symbol' SSing
forall a. ([a] -> a) -> Symbol' a
TLam' (([SSing] -> SSing) -> Symbol' SSing)
-> ([SSing] -> SSing) -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ \ [U.SSing Sing a
a] -> Sing ('HMeasure a) -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing (Sing ('HMeasure a) -> SSing) -> Sing ('HMeasure a) -> SSing
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing ('HMeasure a)
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure Sing a
a)
    , (Text
"either",  ([SSing] -> SSing) -> Symbol' SSing
forall a. ([a] -> a) -> Symbol' a
TLam' (([SSing] -> SSing) -> Symbol' SSing)
-> ([SSing] -> SSing) -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ \ [U.SSing Sing a
a, U.SSing Sing a
b] -> Sing (HEither a a) -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing (Sing (HEither a a) -> SSing) -> Sing (HEither a a) -> SSing
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> Sing (HEither a a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HEither a b)
sEither Sing a
a Sing a
b)
    , (Text
"pair",    ([SSing] -> SSing) -> Symbol' SSing
forall a. ([a] -> a) -> Symbol' a
TLam' (([SSing] -> SSing) -> Symbol' SSing)
-> ([SSing] -> SSing) -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ \ [U.SSing Sing a
a, U.SSing Sing a
b] -> Sing (HPair a a) -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing (Sing (HPair a a) -> SSing) -> Sing (HPair a a) -> SSing
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> Sing (HPair a a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HPair a b)
sPair Sing a
a Sing a
b)
    , (Text
"maybe",   ([SSing] -> SSing) -> Symbol' SSing
forall a. ([a] -> a) -> Symbol' a
TLam' (([SSing] -> SSing) -> Symbol' SSing)
-> ([SSing] -> SSing) -> Symbol' SSing
forall a b. (a -> b) -> a -> b
$ \ [U.SSing Sing a
a] -> Sing (HMaybe a) -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing (Sing (HMaybe a) -> SSing) -> Sing (HMaybe a) -> SSing
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing (HMaybe a)
forall (a :: Hakaru). Sing a -> Sing (HMaybe a)
sMaybe Sing a
a)
    ]

t2 :: (U.AST -> U.AST -> U.AST) -> Symbol U.AST
t2 :: (AST -> AST -> AST) -> Symbol AST
t2 AST -> AST -> AST
f = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
a -> (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
b -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> AST -> AST
f AST
a AST
b)

t3 :: (U.AST -> U.AST -> U.AST -> U.AST) -> Symbol U.AST
t3 :: (AST -> AST -> AST -> AST) -> Symbol AST
t3 AST -> AST -> AST -> AST
f = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
a -> (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
b -> (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
c -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> AST -> AST -> AST
f AST
a AST
b AST
c)

type SymbolTable = [(Text, Symbol U.AST)]

primTable :: SymbolTable
primTable :: SymbolTable
primTable =
    [-- Datatype constructors
     (Text
"left",        Symbol AST
primLeft)
    ,(Text
"right",       Symbol AST
primRight)
    ,(Text
"just",        Symbol AST
primJust)
    ,(Text
"nothing",     Symbol AST
primNothing)
    ,(Text
"true",        AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> AST -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST
true_)
    ,(Text
"false",       AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> AST -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST
false_)
     -- Coercions
    ,(Text
"int2nat",     Coercion 'HNat 'HInt -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primUnsafe Coercion 'HNat 'HInt
cNat2Int)  -- unsafe, wrong direction
    ,(Text
"int2real",    Coercion 'HInt 'HReal -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primCoerce Coercion 'HInt 'HReal
cInt2Real)
    ,(Text
"prob2real",   Coercion 'HProb 'HReal -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primCoerce Coercion 'HProb 'HReal
cProb2Real)
    ,(Text
"real2prob",   Coercion 'HProb 'HReal -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primUnsafe Coercion 'HProb 'HReal
cProb2Real) -- unsafe, wrong direction
    ,(Text
"nat2real",    Coercion 'HNat 'HReal -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primCoerce Coercion 'HNat 'HReal
cNat2Real)
    ,(Text
"nat2prob",    Coercion 'HNat 'HProb -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primCoerce Coercion 'HNat 'HProb
cNat2Prob)
    ,(Text
"nat2int",     Coercion 'HNat 'HInt -> Symbol AST
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Symbol AST
primCoerce Coercion 'HNat 'HInt
cNat2Int)
     -- Measures
    ,(Text
"lebesgue",    SomeOp MeasureOp -> Symbol AST
primMeasure2 (MeasureOp '[ 'HReal, 'HReal] 'HReal -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HReal, 'HReal] 'HReal
T.Lebesgue))
    ,(Text
"counting",    AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> AST -> Symbol AST
forall a b. (a -> b) -> a -> b
$ Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SomeOp MeasureOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SomeOp MeasureOp -> [abt '[] 'U] -> Term abt 'U
U.MeasureOp_ (MeasureOp '[] 'HInt -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[] 'HInt
T.Counting) [])
    ,(Text
"uniform",     SomeOp MeasureOp -> Symbol AST
primMeasure2 (MeasureOp '[ 'HReal, 'HReal] 'HReal -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HReal, 'HReal] 'HReal
T.Uniform))
    ,(Text
"normal",      SomeOp MeasureOp -> Symbol AST
primMeasure2 (MeasureOp '[ 'HReal, 'HProb] 'HReal -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HReal, 'HProb] 'HReal
T.Normal))
    ,(Text
"poisson",     SomeOp MeasureOp -> Symbol AST
primMeasure1 (MeasureOp '[ 'HProb] 'HNat -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HProb] 'HNat
T.Poisson))
    ,(Text
"gamma",       SomeOp MeasureOp -> Symbol AST
primMeasure2 (MeasureOp '[ 'HProb, 'HProb] 'HProb -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HProb, 'HProb] 'HProb
T.Gamma))
    ,(Text
"beta",        SomeOp MeasureOp -> Symbol AST
primMeasure2 (MeasureOp '[ 'HProb, 'HProb] 'HProb -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HProb, 'HProb] 'HProb
T.Beta))
    ,(Text
"categorical", SomeOp MeasureOp -> Symbol AST
primMeasure1 (MeasureOp '[ 'HArray 'HProb] 'HNat -> SomeOp MeasureOp
forall k (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (op :: [Hakaru] -> k -> *) (a :: k).
(typs ~ UnLCs args, args ~ LCs typs) =>
op typs a -> SomeOp op
U.SomeOp MeasureOp '[ 'HArray 'HProb] 'HNat
T.Categorical))
    ,(Text
"factor",      Symbol AST
primFactor)
    ,(Text
"weight",      Symbol AST
primWeight)
    ,(Text
"dirac",       (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> (AST -> AST) -> AST -> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> Term abt 'U
U.Dirac_)
    ,(Text
"reject",      AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> AST -> Symbol AST
forall a b. (a -> b) -> a -> b
$ Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Term abt 'U
U.Reject_)
    -- PrimOps
    ,(Text
"not",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Not)
    ,(Text
"impl",        PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Impl)
    ,(Text
"diff",        PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Diff)
    ,(Text
"nand",        PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Nand)
    ,(Text
"nor",         PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Nor)
    ,(Text
"pi",          PrimOp -> Symbol AST
primPrimOp0 PrimOp
U.Pi)
    ,(Text
"**",          PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.RealPow)
    ,(Text
"choose",      PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Choose)
    ,(Text
"cos",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Cos)
    ,(Text
"exp",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Exp)
    ,(Text
"log",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Log)
    ,(Text
"inf",         PrimOp -> Symbol AST
primPrimOp0 PrimOp
U.Infinity)
    ,(Text
"gammaFunc",   PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.GammaFunc)
    ,(Text
"betaFunc",    PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.BetaFunc)
    ,(Text
"equal",       PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Equal)
    ,(Text
"less",        PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.Less)
    ,(Text
"negate",      PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Negate)
    ,(Text
"abs",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Abs)
    ,(Text
"signum",      PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Signum)
    ,(Text
"recip",       PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Recip)
    ,(Text
"^",           PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.NatPow)
    ,(Text
"natroot",     PrimOp -> Symbol AST
primPrimOp2 PrimOp
U.NatRoot)
    ,(Text
"sqrt",        (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> Symbol AST)
-> Term (MetaABT SourceSpan Term) 'U -> Symbol AST
forall a b. (a -> b) -> a -> b
$ PrimOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
PrimOp -> [abt '[] 'U] -> Term abt 'U
U.PrimOp_ PrimOp
U.NatRoot [AST
x, AST
two])
    ,(Text
"erf",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Erf)
    ,(Text
"sin",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Sin)
    ,(Text
"cos",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Cos)
    ,(Text
"tan",         PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Tan)
    ,(Text
"asin",        PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Asin)
    ,(Text
"acos",        PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Acos)
    ,(Text
"atan",        PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Atan)
    ,(Text
"sinh",        PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Sinh)
    ,(Text
"cosh",        PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Cosh)
    ,(Text
"tanh",        PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Tanh)
    ,(Text
"asinh",       PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Asinh)
    ,(Text
"acosh",       PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Acosh)
    ,(Text
"atanh",       PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Atanh)
    ,(Text
"floor",       PrimOp -> Symbol AST
primPrimOp1 PrimOp
U.Floor)
    -- ArrayOps
    ,(Text
"size",        (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> Symbol AST)
-> Term (MetaABT SourceSpan Term) 'U -> Symbol AST
forall a b. (a -> b) -> a -> b
$ ArrayOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
ArrayOp -> [abt '[] 'U] -> Term abt 'U
U.ArrayOp_ ArrayOp
U.Size [AST
x])
    ,(Text
"reduce",      (AST -> AST -> AST -> AST) -> Symbol AST
t3 ((AST -> AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y AST
z -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ ArrayOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
ArrayOp -> [abt '[] 'U] -> Term abt 'U
U.ArrayOp_ ArrayOp
U.Reduce [AST
x, AST
y, AST
z])
    -- NaryOps
    ,(Text
"xor",         (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NaryOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NaryOp -> [abt '[] 'U] -> Term abt 'U
U.NaryOp_ NaryOp
U.Xor [AST
x, AST
y])
    ,(Text
"iff",         (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NaryOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NaryOp -> [abt '[] 'U] -> Term abt 'U
U.NaryOp_ NaryOp
U.Iff [AST
x, AST
y])
    ,(Text
"min",         (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NaryOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NaryOp -> [abt '[] 'U] -> Term abt 'U
U.NaryOp_ NaryOp
U.Min [AST
x, AST
y])
    ,(Text
"max",         (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NaryOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NaryOp -> [abt '[] 'U] -> Term abt 'U
U.NaryOp_ NaryOp
U.Max [AST
x, AST
y])

    -- Macros
    ,(Text
"weibull",     AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> AST -> Symbol AST
forall a b. (a -> b) -> a -> b
$ Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ (forall (abt' :: [Hakaru] -> Hakaru -> *).
 ABT Term abt' =>
 abt' '[] ('HProb ':-> ('HProb ':-> 'HMeasure 'HProb)))
-> Term (MetaABT SourceSpan Term) 'U
forall (x :: Hakaru) (abt :: [Untyped] -> Untyped -> *).
(forall (abt' :: [Hakaru] -> Hakaru -> *).
 ABT Term abt' =>
 abt' '[] x)
-> Term abt 'U
U.InjTyped ((forall (abt' :: [Hakaru] -> Hakaru -> *).
  ABT Term abt' =>
  abt' '[] ('HProb ':-> ('HProb ':-> 'HMeasure 'HProb)))
 -> Term (MetaABT SourceSpan Term) 'U)
-> (forall (abt' :: [Hakaru] -> Hakaru -> *).
    ABT Term abt' =>
    abt' '[] ('HProb ':-> ('HProb ':-> 'HMeasure 'HProb)))
-> Term (MetaABT SourceSpan Term) 'U
forall a b. (a -> b) -> a -> b
$
                     (abt' '[] 'HProb -> abt' '[] ('HProb ':-> 'HMeasure 'HProb))
-> abt' '[] ('HProb ':-> ('HProb ':-> 'HMeasure 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
P.lam ((abt' '[] 'HProb -> abt' '[] ('HProb ':-> 'HMeasure 'HProb))
 -> abt' '[] ('HProb ':-> ('HProb ':-> 'HMeasure 'HProb)))
-> (abt' '[] 'HProb -> abt' '[] ('HProb ':-> 'HMeasure 'HProb))
-> abt' '[] ('HProb ':-> ('HProb ':-> 'HMeasure 'HProb))
forall a b. (a -> b) -> a -> b
$ \abt' '[] 'HProb
x -> (abt' '[] 'HProb -> abt' '[] ('HMeasure 'HProb))
-> abt' '[] ('HProb ':-> 'HMeasure 'HProb)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
P.lam ((abt' '[] 'HProb -> abt' '[] ('HMeasure 'HProb))
 -> abt' '[] ('HProb ':-> 'HMeasure 'HProb))
-> (abt' '[] 'HProb -> abt' '[] ('HMeasure 'HProb))
-> abt' '[] ('HProb ':-> 'HMeasure 'HProb)
forall a b. (a -> b) -> a -> b
$ \abt' '[] 'HProb
y -> abt' '[] 'HProb -> abt' '[] 'HProb -> abt' '[] ('HMeasure 'HProb)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HProb -> abt '[] ('HMeasure 'HProb)
P.weibull abt' '[] 'HProb
x abt' '[] 'HProb
y)
    ]

primPrimOp0, primPrimOp1, primPrimOp2 :: U.PrimOp -> Symbol U.AST
primPrimOp0 :: PrimOp -> Symbol AST
primPrimOp0 PrimOp
a = AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> Symbol AST)
-> Term (MetaABT SourceSpan Term) 'U -> Symbol AST
forall a b. (a -> b) -> a -> b
$ PrimOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
PrimOp -> [abt '[] 'U] -> Term abt 'U
U.PrimOp_ PrimOp
a []
primPrimOp1 :: PrimOp -> Symbol AST
primPrimOp1 PrimOp
a = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> Symbol AST)
-> Term (MetaABT SourceSpan Term) 'U -> Symbol AST
forall a b. (a -> b) -> a -> b
$ PrimOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
PrimOp -> [abt '[] 'U] -> Term abt 'U
U.PrimOp_ PrimOp
a [AST
x]
primPrimOp2 :: PrimOp -> Symbol AST
primPrimOp2 PrimOp
a = (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y ->        Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ PrimOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
PrimOp -> [abt '[] 'U] -> Term abt 'U
U.PrimOp_ PrimOp
a [AST
x, AST
y]

primMeasure1 :: U.SomeOp T.MeasureOp -> Symbol U.AST
primMeasure1 :: SomeOp MeasureOp -> Symbol AST
primMeasure1 SomeOp MeasureOp
m = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> Symbol AST)
-> Term (MetaABT SourceSpan Term) 'U -> Symbol AST
forall a b. (a -> b) -> a -> b
$ SomeOp MeasureOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SomeOp MeasureOp -> [abt '[] 'U] -> Term abt 'U
U.MeasureOp_ SomeOp MeasureOp
m [AST
x]

primMeasure2 :: U.SomeOp T.MeasureOp -> Symbol U.AST
primMeasure2 :: SomeOp MeasureOp -> Symbol AST
primMeasure2 SomeOp MeasureOp
m = (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
x AST
y -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SomeOp MeasureOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SomeOp MeasureOp -> [abt '[] 'U] -> Term abt 'U
U.MeasureOp_ SomeOp MeasureOp
m [AST
x, AST
y]

primCoerce :: Coercion a b -> Symbol U.AST
primCoerce :: Coercion a b -> Symbol AST
primCoerce Coercion a b
c = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> (AST -> AST) -> AST -> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some2 Coercion -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
Some2 Coercion -> abt '[] 'U -> Term abt 'U
U.CoerceTo_  (Coercion a b -> Some2 Coercion
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Coercion a b
c)

primUnsafe :: Coercion a b -> Symbol U.AST
primUnsafe :: Coercion a b -> Symbol AST
primUnsafe Coercion a b
c = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> (AST -> AST) -> AST -> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some2 Coercion -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
Some2 Coercion -> abt '[] 'U -> Term abt 'U
U.UnsafeTo_  (Coercion a b -> Some2 Coercion
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Coercion a b
c)

cProb2Real :: Coercion 'HProb 'HReal
cProb2Real :: Coercion 'HProb 'HReal
cProb2Real = Coercion 'HProb 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed

cNat2Prob :: Coercion 'HNat 'HProb
cNat2Prob :: Coercion 'HNat 'HProb
cNat2Prob = Coercion 'HNat 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous

cNat2Int  :: Coercion 'HNat 'HInt
cNat2Int :: Coercion 'HNat 'HInt
cNat2Int  = Coercion 'HNat 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed

cInt2Real  :: Coercion 'HInt 'HReal
cInt2Real :: Coercion 'HInt 'HReal
cInt2Real  = Coercion 'HInt 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous

cNat2Real :: Coercion 'HNat 'HReal
cNat2Real :: Coercion 'HNat 'HReal
cNat2Real = PrimCoercion 'HNat 'HInt
-> Coercion 'HInt 'HReal -> Coercion 'HNat 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons (HRing 'HInt -> PrimCoercion (NonNegative 'HInt) 'HInt
forall (a :: Hakaru). HRing a -> PrimCoercion (NonNegative a) a
Signed HRing 'HInt
HRing_Int) Coercion 'HInt 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous

unit_ :: U.AST
unit_ :: AST
unit_ =
    Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SSing -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SSing -> abt '[] 'U -> Term abt 'U
U.Ann_ (Sing HUnit -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing HUnit
sUnit)
                 (Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"unit" (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (DStruct (MetaABT SourceSpan Term)
    -> DCode (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall a b. (a -> b) -> a -> b
$ DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done))

true_, false_ :: U.AST
true_ :: AST
true_  =
    Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SSing -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SSing -> abt '[] 'U -> Term abt 'U
U.Ann_ (Sing HBool -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing HBool
sBool)
                 (Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Datum (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> (DStruct (MetaABT SourceSpan Term)
    -> Datum (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"true"  (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (DStruct (MetaABT SourceSpan Term)
    -> DCode (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> DStruct (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall a b. (a -> b) -> a -> b
$ DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done)

false_ :: AST
false_ =
    Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SSing -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SSing -> abt '[] 'U -> Term abt 'U
U.Ann_ (Sing HBool -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing Sing HBool
sBool)
                 (Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Datum (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> (DStruct (MetaABT SourceSpan Term)
    -> Datum (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"false" (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (DStruct (MetaABT SourceSpan Term)
    -> DCode (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DCode (MetaABT SourceSpan Term) -> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DCode abt -> DCode abt
U.Inr (DCode (MetaABT SourceSpan Term)
 -> DCode (MetaABT SourceSpan Term))
-> (DStruct (MetaABT SourceSpan Term)
    -> DCode (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> DStruct (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall a b. (a -> b) -> a -> b
$ DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done)

unsafeFrom_ :: U.AST -> U.AST
unsafeFrom_ :: AST -> AST
unsafeFrom_ = Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some2 Coercion -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
Some2 Coercion -> abt '[] 'U -> Term abt 'U
U.UnsafeTo_ (Coercion 'HProb 'HReal -> Some2 Coercion
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 (Coercion 'HProb 'HReal -> Some2 Coercion)
-> Coercion 'HProb 'HReal -> Some2 Coercion
forall a b. (a -> b) -> a -> b
$ PrimCoercion 'HProb 'HReal
-> Coercion 'HReal 'HReal -> Coercion 'HProb 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons (HRing 'HReal -> PrimCoercion (NonNegative 'HReal) 'HReal
forall (a :: Hakaru). HRing a -> PrimCoercion (NonNegative a) a
Signed HRing 'HReal
HRing_Real) Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil)

primLeft, primRight :: Symbol U.AST
primLeft :: Symbol AST
primLeft =
    (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> (AST -> AST) -> AST -> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Datum (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> (AST -> Datum (MetaABT SourceSpan Term))
-> AST
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"left" (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (AST -> DCode (MetaABT SourceSpan Term))
-> AST
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term)
 -> DCode (MetaABT SourceSpan Term))
-> (AST -> DStruct (MetaABT SourceSpan Term))
-> AST
-> DCode (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DFun (MetaABT SourceSpan Term)
-> DStruct (MetaABT SourceSpan Term)
-> DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
DFun abt -> DStruct abt -> DStruct abt
`U.Et` DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done) (DFun (MetaABT SourceSpan Term)
 -> DStruct (MetaABT SourceSpan Term))
-> (AST -> DFun (MetaABT SourceSpan Term))
-> AST
-> DStruct (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST -> DFun (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). abt '[] 'U -> DFun abt
U.Konst
primRight :: Symbol AST
primRight =
    (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> (AST -> AST) -> AST -> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Datum (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> (AST -> Datum (MetaABT SourceSpan Term))
-> AST
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"right" (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (AST -> DCode (MetaABT SourceSpan Term))
-> AST
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DCode (MetaABT SourceSpan Term) -> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DCode abt -> DCode abt
U.Inr (DCode (MetaABT SourceSpan Term)
 -> DCode (MetaABT SourceSpan Term))
-> (AST -> DCode (MetaABT SourceSpan Term))
-> AST
-> DCode (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term)
 -> DCode (MetaABT SourceSpan Term))
-> (AST -> DStruct (MetaABT SourceSpan Term))
-> AST
-> DCode (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DFun (MetaABT SourceSpan Term)
-> DStruct (MetaABT SourceSpan Term)
-> DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
DFun abt -> DStruct abt -> DStruct abt
`U.Et` DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done) (DFun (MetaABT SourceSpan Term)
 -> DStruct (MetaABT SourceSpan Term))
-> (AST -> DFun (MetaABT SourceSpan Term))
-> AST
-> DStruct (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST -> DFun (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). abt '[] 'U -> DFun abt
U.Konst

primJust, primNothing :: Symbol U.AST
primJust :: Symbol AST
primJust =
    (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> (AST -> AST) -> AST -> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (AST -> Term (MetaABT SourceSpan Term) 'U) -> AST -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Datum (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> (AST -> Datum (MetaABT SourceSpan Term))
-> AST
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"just" (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (AST -> DCode (MetaABT SourceSpan Term))
-> AST
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DCode (MetaABT SourceSpan Term) -> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DCode abt -> DCode abt
U.Inr (DCode (MetaABT SourceSpan Term)
 -> DCode (MetaABT SourceSpan Term))
-> (AST -> DCode (MetaABT SourceSpan Term))
-> AST
-> DCode (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term)
 -> DCode (MetaABT SourceSpan Term))
-> (AST -> DStruct (MetaABT SourceSpan Term))
-> AST
-> DCode (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DFun (MetaABT SourceSpan Term)
-> DStruct (MetaABT SourceSpan Term)
-> DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
DFun abt -> DStruct abt -> DStruct abt
`U.Et` DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done) (DFun (MetaABT SourceSpan Term)
 -> DStruct (MetaABT SourceSpan Term))
-> (AST -> DFun (MetaABT SourceSpan Term))
-> AST
-> DStruct (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST -> DFun (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). abt '[] 'U -> DFun abt
U.Konst
primNothing :: Symbol AST
primNothing =
    AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (DStruct (MetaABT SourceSpan Term) -> AST)
-> DStruct (MetaABT SourceSpan Term)
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (DStruct (MetaABT SourceSpan Term)
    -> Term (MetaABT SourceSpan Term) 'U)
-> DStruct (MetaABT SourceSpan Term)
-> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Datum (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *). Datum abt -> Term abt 'U
U.Datum_ (Datum (MetaABT SourceSpan Term)
 -> Term (MetaABT SourceSpan Term) 'U)
-> (DStruct (MetaABT SourceSpan Term)
    -> Datum (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Text
-> DCode (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *).
Text -> DCode abt -> Datum abt
U.Datum Text
"nothing" (DCode (MetaABT SourceSpan Term)
 -> Datum (MetaABT SourceSpan Term))
-> (DStruct (MetaABT SourceSpan Term)
    -> DCode (MetaABT SourceSpan Term))
-> DStruct (MetaABT SourceSpan Term)
-> Datum (MetaABT SourceSpan Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DStruct (MetaABT SourceSpan Term)
-> DCode (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt -> DCode abt
U.Inl (DStruct (MetaABT SourceSpan Term) -> Symbol AST)
-> DStruct (MetaABT SourceSpan Term) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ DStruct (MetaABT SourceSpan Term)
forall k (abt :: [k] -> Untyped -> *). DStruct abt
U.Done

primWeight, primFactor :: Symbol U.AST
primWeight :: Symbol AST
primWeight = (AST -> AST -> AST) -> Symbol AST
t2 ((AST -> AST -> AST) -> Symbol AST)
-> (AST -> AST -> AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
w AST
m -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NonEmpty (AST, AST) -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NonEmpty (abt '[] 'U, abt '[] 'U) -> Term abt 'U
U.Superpose_ ((AST, AST) -> NonEmpty (AST, AST)
forall a. a -> NonEmpty a
singleton (AST
w, AST
m))
primFactor :: Symbol AST
primFactor = (AST -> Symbol AST) -> Symbol AST
forall a. (a -> Symbol a) -> Symbol a
TLam ((AST -> Symbol AST) -> Symbol AST)
-> (AST -> Symbol AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$ \AST
w -> AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST)
-> (NonEmpty (AST, AST) -> AST)
-> NonEmpty (AST, AST)
-> Symbol AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (NonEmpty (AST, AST) -> Term (MetaABT SourceSpan Term) 'U)
-> NonEmpty (AST, AST)
-> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (AST, AST) -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NonEmpty (abt '[] 'U, abt '[] 'U) -> Term abt 'U
U.Superpose_ (NonEmpty (AST, AST) -> Symbol AST)
-> NonEmpty (AST, AST) -> Symbol AST
forall a b. (a -> b) -> a -> b
$
              (AST, AST) -> NonEmpty (AST, AST)
forall a. a -> NonEmpty a
singleton (AST
w, Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> Term abt 'U
U.Dirac_ AST
unit_)

two :: U.AST
two :: AST
two = Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (Integer -> Term (MetaABT SourceSpan Term) 'U) -> Integer -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some1 Literal -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
Some1 Literal -> Term abt 'U
U.Literal_ (Some1 Literal -> Term (MetaABT SourceSpan Term) 'U)
-> (Integer -> Some1 Literal)
-> Integer
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal' -> Some1 Literal
U.val (Literal' -> Some1 Literal)
-> (Integer -> Literal') -> Integer -> Some1 Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal'
U.Nat (Integer -> AST) -> Integer -> AST
forall a b. (a -> b) -> a -> b
$ Integer
2

gensym :: Text -> State Int U.Name
gensym :: Text -> State Int Name
gensym Text
s = (Int -> (Name, Int)) -> State Int Name
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state ((Int -> (Name, Int)) -> State Int Name)
-> (Int -> (Name, Int)) -> State Int Name
forall a b. (a -> b) -> a -> b
$ \Int
i -> (Nat -> Text -> Name
U.Name (Int -> Nat
N.unsafeNat Int
i) Text
s, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

mkSym  :: U.Name -> Symbol U.AST
mkSym :: Name -> Symbol AST
mkSym (U.Name Nat
i Text
t) = AST -> Symbol AST
forall a. a -> Symbol a
TNeu (AST -> Symbol AST) -> AST -> Symbol AST
forall a b. (a -> b) -> a -> b
$ Variable 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var (Text -> Nat -> Sing 'U -> Variable 'U
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
t Nat
i Sing 'U
U.SU)

insertSymbol :: U.Name -> SymbolTable -> SymbolTable
insertSymbol :: Name -> SymbolTable -> SymbolTable
insertSymbol n :: Name
n@(U.Name Nat
_ Text
name) SymbolTable
sym = (Text
name, Name -> Symbol AST
mkSym Name
n) (Text, Symbol AST) -> SymbolTable -> SymbolTable
forall a. a -> [a] -> [a]
: SymbolTable
sym

insertSymbols :: [U.Name] -> SymbolTable -> SymbolTable
insertSymbols :: [Name] -> SymbolTable -> SymbolTable
insertSymbols []     SymbolTable
sym = SymbolTable
sym
insertSymbols (Name
n:[Name]
ns) SymbolTable
sym = [Name] -> SymbolTable -> SymbolTable
insertSymbols [Name]
ns (Name -> SymbolTable -> SymbolTable
insertSymbol Name
n SymbolTable
sym)


resolveBinder
    :: SymbolTable
    -> Text
    -> U.AST' Text
    -> U.AST' Text
    -> (Symbol U.AST
        -> U.AST' (Symbol U.AST)
        -> U.AST' (Symbol U.AST)
        -> U.AST' (Symbol U.AST))
    -> State Int (U.AST' (Symbol U.AST))
resolveBinder :: SymbolTable
-> Text
-> AST' Text
-> AST' Text
-> (Symbol AST
    -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
resolveBinder SymbolTable
symbols Text
name AST' Text
e1 AST' Text
e2 Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
f = do
    Name
name' <- Text -> State Int Name
gensym Text
name
    Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
f (Name -> Symbol AST
mkSym Name
name')
        (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
        StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) AST' Text
e2

resolveTransform
    :: SymbolTable
    -> U.Transform'
    -> U.SArgs' Text
    -> State Int (U.AST' (Symbol U.AST))
resolveTransform :: SymbolTable
-> Transform' -> SArgs' Text -> State Int (AST' (Symbol AST))
resolveTransform SymbolTable
symbols Transform'
tr (U.SArgs' [([Text], AST' Text)]
es) =
    Transform' -> SArgs' (Symbol AST) -> AST' (Symbol AST)
forall a. Transform' -> SArgs' a -> AST' a
U.Transform Transform'
tr (SArgs' (Symbol AST) -> AST' (Symbol AST))
-> ([([Symbol AST], AST' (Symbol AST))] -> SArgs' (Symbol AST))
-> [([Symbol AST], AST' (Symbol AST))]
-> AST' (Symbol AST)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([Symbol AST], AST' (Symbol AST))] -> SArgs' (Symbol AST)
forall a. [([a], AST' a)] -> SArgs' a
U.SArgs' ([([Symbol AST], AST' (Symbol AST))] -> AST' (Symbol AST))
-> StateT Int Identity [([Symbol AST], AST' (Symbol AST))]
-> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Text], AST' Text)
 -> StateT Int Identity ([Symbol AST], AST' (Symbol AST)))
-> [([Text], AST' Text)]
-> StateT Int Identity [([Symbol AST], AST' (Symbol AST))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Text], AST' Text)
-> StateT Int Identity ([Symbol AST], AST' (Symbol AST))
go [([Text], AST' Text)]
es where
      go :: ([Text], U.AST' Text)
         -> State Int ([Symbol U.AST], U.AST' (Symbol U.AST))
      go :: ([Text], AST' Text)
-> StateT Int Identity ([Symbol AST], AST' (Symbol AST))
go ([Text]
nms,AST' Text
x) = do
        [Name]
nms' <- (Text -> State Int Name) -> [Text] -> StateT Int Identity [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Text -> State Int Name
gensym [Text]
nms
        (,) ((Name -> Symbol AST) -> [Name] -> [Symbol AST]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Symbol AST
mkSym [Name]
nms') (AST' (Symbol AST) -> ([Symbol AST], AST' (Symbol AST)))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity ([Symbol AST], AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution ([Name] -> SymbolTable -> SymbolTable
insertSymbols [Name]
nms' SymbolTable
symbols) AST' Text
x

-- TODO: clean up by merging the @Reader (SymbolTable)@ and @State Int@ monads
-- | Figure out symbols and types.
symbolResolution
    :: SymbolTable
    -> U.AST' Text
    -> State Int (U.AST' (Symbol U.AST))
symbolResolution :: SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
ast =
    case AST' Text
ast of
    U.Var Text
name ->
        case Text -> SymbolTable -> Maybe (Symbol AST)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
name SymbolTable
symbols of
        Maybe (Symbol AST)
Nothing -> (Symbol AST -> AST' (Symbol AST)
forall a. a -> AST' a
U.Var (Symbol AST -> AST' (Symbol AST))
-> (Name -> Symbol AST) -> Name -> AST' (Symbol AST)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Symbol AST
mkSym) (Name -> AST' (Symbol AST))
-> State Int Name -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> State Int Name
gensym Text
name
        Just Symbol AST
a  -> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall (m :: * -> *) a. Monad m => a -> m a
return (AST' (Symbol AST) -> State Int (AST' (Symbol AST)))
-> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall a b. (a -> b) -> a -> b
$ Symbol AST -> AST' (Symbol AST)
forall a. a -> AST' a
U.Var Symbol AST
a

    U.Lam Text
name TypeAST'
typ AST' Text
x -> do
        Name
name' <- Text -> State Int Name
gensym Text
name
        Symbol AST -> TypeAST' -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> TypeAST' -> AST' a -> AST' a
U.Lam (Name -> Symbol AST
mkSym Name
name') TypeAST'
typ
            (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) AST' Text
x

    U.App AST' Text
f AST' Text
x -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a
U.App
        (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
f
        StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
x

    U.Let Text
name AST' Text
e1 AST' Text
e2    -> SymbolTable
-> Text
-> AST' Text
-> AST' Text
-> (Symbol AST
    -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
resolveBinder SymbolTable
symbols Text
name AST' Text
e1 AST' Text
e2 Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Let
    U.If AST' Text
e1 AST' Text
e2 AST' Text
e3       -> AST' (Symbol AST)
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a -> AST' a
U.If
        (AST' (Symbol AST)
 -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
        StateT
  Int
  Identity
  (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
        StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e3

    U.Ann AST' Text
e TypeAST'
typ         -> (AST' (Symbol AST) -> TypeAST' -> AST' (Symbol AST)
forall a. AST' a -> TypeAST' -> AST' a
`U.Ann` TypeAST'
typ) (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e
    AST' Text
U.Infinity'         -> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall (m :: * -> *) a. Monad m => a -> m a
return (AST' (Symbol AST) -> State Int (AST' (Symbol AST)))
-> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST)
forall a. AST' a
U.Infinity'
    U.ULiteral Literal'
v        -> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall (m :: * -> *) a. Monad m => a -> m a
return (AST' (Symbol AST) -> State Int (AST' (Symbol AST)))
-> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall a b. (a -> b) -> a -> b
$ Literal' -> AST' (Symbol AST)
forall a. Literal' -> AST' a
U.ULiteral Literal'
v

    U.Integrate  Text
name AST' Text
e1 AST' Text
e2 AST' Text
e3 -> do
        Name
name' <- Text -> State Int Name
gensym Text
name
        Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Integrate (Name -> Symbol AST
mkSym Name
name')
            (AST' (Symbol AST)
 -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
            StateT
  Int
  Identity
  (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
            StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) AST' Text
e3

    U.Summate    Text
name AST' Text
e1 AST' Text
e2 AST' Text
e3 -> do
        Name
name' <- Text -> State Int Name
gensym Text
name
        Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Summate (Name -> Symbol AST
mkSym Name
name')
            (AST' (Symbol AST)
 -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
            StateT
  Int
  Identity
  (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
            StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) AST' Text
e3

    U.Product    Text
name AST' Text
e1 AST' Text
e2 AST' Text
e3 -> do
        Name
name' <- Text -> State Int Name
gensym Text
name
        Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Product (Name -> Symbol AST
mkSym Name
name')
            (AST' (Symbol AST)
 -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
            StateT
  Int
  Identity
  (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
            StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) AST' Text
e3

    U.Bucket     Text
name AST' Text
e1 AST' Text
e2 Reducer' Text
e3 -> do
        Name
name' <- Text -> State Int Name
gensym Text
name
        Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> Reducer' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> Reducer' a -> AST' a
U.Bucket (Name -> Symbol AST
mkSym Name
name')
            (AST' (Symbol AST)
 -> AST' (Symbol AST) -> Reducer' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST) -> Reducer' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
            StateT
  Int
  Identity
  (AST' (Symbol AST) -> Reducer' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
            StateT Int Identity (Reducer' (Symbol AST) -> AST' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
-> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) Reducer' Text
e3

    U.NaryOp NaryOp
op [AST' Text]
es      -> NaryOp -> [AST' (Symbol AST)] -> AST' (Symbol AST)
forall a. NaryOp -> [AST' a] -> AST' a
U.NaryOp NaryOp
op
        ([AST' (Symbol AST)] -> AST' (Symbol AST))
-> StateT Int Identity [AST' (Symbol AST)]
-> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AST' Text -> State Int (AST' (Symbol AST)))
-> [AST' Text] -> StateT Int Identity [AST' (Symbol AST)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols) [AST' Text]
es

    AST' Text
U.Unit              -> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall (m :: * -> *) a. Monad m => a -> m a
return (AST' (Symbol AST) -> State Int (AST' (Symbol AST)))
-> AST' (Symbol AST) -> State Int (AST' (Symbol AST))
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST)
forall a. AST' a
U.Unit
    U.Pair AST' Text
e1 AST' Text
e2        -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a
U.Pair
        (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
        StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2

    U.Array Text
name AST' Text
e1 AST' Text
e2  -> SymbolTable
-> Text
-> AST' Text
-> AST' Text
-> (Symbol AST
    -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
resolveBinder SymbolTable
symbols Text
name AST' Text
e1 AST' Text
e2 Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Array

    U.ArrayLiteral [AST' Text]
es   -> [AST' (Symbol AST)] -> AST' (Symbol AST)
forall a. [AST' a] -> AST' a
U.ArrayLiteral ([AST' (Symbol AST)] -> AST' (Symbol AST))
-> StateT Int Identity [AST' (Symbol AST)]
-> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AST' Text -> State Int (AST' (Symbol AST)))
-> [AST' Text] -> StateT Int Identity [AST' (Symbol AST)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols) [AST' Text]
es

    U.Index AST' Text
a AST' Text
i -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a
U.Index
        (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
a
        StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
i

    U.Case AST' Text
e1 [Branch' Text]
bs -> AST' (Symbol AST) -> [Branch' (Symbol AST)] -> AST' (Symbol AST)
forall a. AST' a -> [Branch' a] -> AST' a
U.Case
        (AST' (Symbol AST) -> [Branch' (Symbol AST)] -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int Identity ([Branch' (Symbol AST)] -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
        StateT Int Identity ([Branch' (Symbol AST)] -> AST' (Symbol AST))
-> StateT Int Identity [Branch' (Symbol AST)]
-> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Branch' Text -> StateT Int Identity (Branch' (Symbol AST)))
-> [Branch' Text] -> StateT Int Identity [Branch' (Symbol AST)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SymbolTable
-> Branch' Text -> StateT Int Identity (Branch' (Symbol AST))
symbolResolveBranch SymbolTable
symbols) [Branch' Text]
bs

    U.Bind   Text
name AST' Text
e1 AST' Text
e2    -> SymbolTable
-> Text
-> AST' Text
-> AST' Text
-> (Symbol AST
    -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
resolveBinder SymbolTable
symbols Text
name AST' Text
e1 AST' Text
e2 Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Bind
    U.Plate  Text
name AST' Text
e1 AST' Text
e2    -> SymbolTable
-> Text
-> AST' Text
-> AST' Text
-> (Symbol AST
    -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
resolveBinder SymbolTable
symbols Text
name AST' Text
e1 AST' Text
e2 Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Plate
    U.Transform Transform'
tr SArgs' Text
es      -> SymbolTable
-> Transform' -> SArgs' Text -> State Int (AST' (Symbol AST))
resolveTransform SymbolTable
symbols Transform'
tr SArgs' Text
es
    U.Chain  Text
name AST' Text
e1 AST' Text
e2 AST' Text
e3 -> do
        Name
name' <- Text -> State Int Name
gensym Text
name
        Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Chain (Name -> Symbol AST
mkSym Name
name')
            (AST' (Symbol AST)
 -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
            StateT
  Int
  Identity
  (AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
            StateT Int Identity (AST' (Symbol AST) -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST)) -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) AST' Text
e3

    U.Msum [AST' Text]
es -> [AST' (Symbol AST)] -> AST' (Symbol AST)
forall a. [AST' a] -> AST' a
U.Msum ([AST' (Symbol AST)] -> AST' (Symbol AST))
-> StateT Int Identity [AST' (Symbol AST)]
-> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AST' Text -> State Int (AST' (Symbol AST)))
-> [AST' Text] -> StateT Int Identity [AST' (Symbol AST)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols) [AST' Text]
es

    U.Data Text
name [Text]
tvars [TypeAST']
typ AST' Text
e -> [Char] -> State Int (AST' (Symbol AST))
forall a. HasCallStack => [Char] -> a
error ([Char] -> State Int (AST' (Symbol AST)))
-> [Char] -> State Int (AST' (Symbol AST))
forall a b. (a -> b) -> a -> b
$ ([Char]
"TODO: symbolResolution{U.Data} " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                        Text -> [Char]
forall a. Show a => a -> [Char]
show Text
name  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" with " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                        [Text] -> [Char]
forall a. Show a => a -> [Char]
show [Text]
tvars [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [TypeAST'] -> [Char]
forall a. Show a => a -> [Char]
show [TypeAST']
typ)
    U.WithMeta AST' Text
a SourceSpan
meta -> AST' (Symbol AST) -> SourceSpan -> AST' (Symbol AST)
forall a. AST' a -> SourceSpan -> AST' a
U.WithMeta
        (AST' (Symbol AST) -> SourceSpan -> AST' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (SourceSpan -> AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
a
        StateT Int Identity (SourceSpan -> AST' (Symbol AST))
-> StateT Int Identity SourceSpan -> State Int (AST' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SourceSpan -> StateT Int Identity SourceSpan
forall (m :: * -> *) a. Monad m => a -> m a
return SourceSpan
meta

symbolResolutionReducer
    :: SymbolTable
    -> U.Reducer' Text
    -> State Int (U.Reducer' (Symbol U.AST))
symbolResolutionReducer :: SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer SymbolTable
symbols Reducer' Text
ast =
    case Reducer' Text
ast of
    U.R_Fanout Reducer' Text
e1 Reducer' Text
e2        -> Reducer' (Symbol AST)
-> Reducer' (Symbol AST) -> Reducer' (Symbol AST)
forall a. Reducer' a -> Reducer' a -> Reducer' a
U.R_Fanout
                               (Reducer' (Symbol AST)
 -> Reducer' (Symbol AST) -> Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
-> StateT
     Int Identity (Reducer' (Symbol AST) -> Reducer' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer SymbolTable
symbols Reducer' Text
e1
                               StateT
  Int Identity (Reducer' (Symbol AST) -> Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer SymbolTable
symbols Reducer' Text
e2

    U.R_Index Text
name AST' Text
e1 AST' Text
e2 Reducer' Text
e3 -> do
      Name
name' <- Text -> State Int Name
gensym Text
name
      Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> Reducer' (Symbol AST)
-> Reducer' (Symbol AST)
forall a. a -> AST' a -> AST' a -> Reducer' a -> Reducer' a
U.R_Index (Name -> Symbol AST
mkSym Name
name')
           (AST' (Symbol AST)
 -> AST' (Symbol AST)
 -> Reducer' (Symbol AST)
 -> Reducer' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (AST' (Symbol AST)
      -> Reducer' (Symbol AST) -> Reducer' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
           StateT
  Int
  Identity
  (AST' (Symbol AST)
   -> Reducer' (Symbol AST) -> Reducer' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int Identity (Reducer' (Symbol AST) -> Reducer' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e2
           StateT
  Int Identity (Reducer' (Symbol AST) -> Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer (Name -> SymbolTable -> SymbolTable
insertSymbol Name
name' SymbolTable
symbols) Reducer' Text
e3
    U.R_Split AST' Text
e1 Reducer' Text
e2 Reducer' Text
e3      -> AST' (Symbol AST)
-> Reducer' (Symbol AST)
-> Reducer' (Symbol AST)
-> Reducer' (Symbol AST)
forall a. AST' a -> Reducer' a -> Reducer' a -> Reducer' a
U.R_Split
                               (AST' (Symbol AST)
 -> Reducer' (Symbol AST)
 -> Reducer' (Symbol AST)
 -> Reducer' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT
     Int
     Identity
     (Reducer' (Symbol AST)
      -> Reducer' (Symbol AST) -> Reducer' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1
                               StateT
  Int
  Identity
  (Reducer' (Symbol AST)
   -> Reducer' (Symbol AST) -> Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
-> StateT
     Int Identity (Reducer' (Symbol AST) -> Reducer' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer SymbolTable
symbols Reducer' Text
e2
                               StateT
  Int Identity (Reducer' (Symbol AST) -> Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolTable
-> Reducer' Text -> StateT Int Identity (Reducer' (Symbol AST))
symbolResolutionReducer SymbolTable
symbols Reducer' Text
e3
    Reducer' Text
U.R_Nop                 -> Reducer' (Symbol AST)
-> StateT Int Identity (Reducer' (Symbol AST))
forall (m :: * -> *) a. Monad m => a -> m a
return Reducer' (Symbol AST)
forall a. Reducer' a
U.R_Nop
    U.R_Add   AST' Text
e1            -> AST' (Symbol AST) -> Reducer' (Symbol AST)
forall a. AST' a -> Reducer' a
U.R_Add (AST' (Symbol AST) -> Reducer' (Symbol AST))
-> State Int (AST' (Symbol AST))
-> StateT Int Identity (Reducer' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
symbols AST' Text
e1


symbolResolveBranch
    :: SymbolTable
    -> U.Branch' Text
    -> State Int (U.Branch' (Symbol U.AST))
symbolResolveBranch :: SymbolTable
-> Branch' Text -> StateT Int Identity (Branch' (Symbol AST))
symbolResolveBranch SymbolTable
symbols (U.Branch' Pattern' Text
pat AST' Text
ast) = do
    (Pattern' Name
pat', [Name]
names) <- Pattern' Text -> State Int (Pattern' Name, [Name])
symbolResolvePat Pattern' Text
pat
    AST' (Symbol AST)
ast' <- SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution ([Name] -> SymbolTable -> SymbolTable
insertSymbols [Name]
names SymbolTable
symbols) AST' Text
ast
    Branch' (Symbol AST) -> StateT Int Identity (Branch' (Symbol AST))
forall (m :: * -> *) a. Monad m => a -> m a
return (Branch' (Symbol AST)
 -> StateT Int Identity (Branch' (Symbol AST)))
-> Branch' (Symbol AST)
-> StateT Int Identity (Branch' (Symbol AST))
forall a b. (a -> b) -> a -> b
$ Pattern' Name -> AST' (Symbol AST) -> Branch' (Symbol AST)
forall a. Pattern' Name -> AST' a -> Branch' a
U.Branch'' Pattern' Name
pat' AST' (Symbol AST)
ast'
symbolResolveBranch SymbolTable
_ Branch' Text
_ =
    [Char] -> StateT Int Identity (Branch' (Symbol AST))
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: symbolResolveBranch{U.Branch''}"


symbolResolvePat
    :: U.Pattern' Text
    -> State Int (U.Pattern' U.Name, [U.Name])
symbolResolvePat :: Pattern' Text -> State Int (Pattern' Name, [Name])
symbolResolvePat (U.PVar' Text
"true") =
    (Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (PDatum Name -> Pattern' Name
forall a. PDatum a -> Pattern' a
U.PData' (Text -> [Pattern' Name] -> PDatum Name
forall a. Text -> [Pattern' a] -> PDatum a
U.DV Text
"true" []), [])
symbolResolvePat (U.PVar' Text
"false") =
    (Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (PDatum Name -> Pattern' Name
forall a. PDatum a -> Pattern' a
U.PData' (Text -> [Pattern' Name] -> PDatum Name
forall a. Text -> [Pattern' a] -> PDatum a
U.DV Text
"false" []), [])
symbolResolvePat (U.PVar' Text
name)  = do
    Name
name' <- Text -> State Int Name
gensym Text
name
    (Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Pattern' Name
forall a. a -> Pattern' a
U.PVar' Name
name', [Name
name'])
symbolResolvePat Pattern' Text
U.PWild' =
    (Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Name
forall a. Pattern' a
U.PWild', [])
symbolResolvePat (U.PData' (U.DV Text
name [Pattern' Text]
args)) = do
    [(Pattern' Name, [Name])]
args' <- (Pattern' Text -> State Int (Pattern' Name, [Name]))
-> [Pattern' Text] -> StateT Int Identity [(Pattern' Name, [Name])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Pattern' Text -> State Int (Pattern' Name, [Name])
symbolResolvePat [Pattern' Text]
args
    let ([Pattern' Name]
args'', [[Name]]
names) = [(Pattern' Name, [Name])] -> ([Pattern' Name], [[Name]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Pattern' Name, [Name])]
args'
    (Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name]))
-> (Pattern' Name, [Name]) -> State Int (Pattern' Name, [Name])
forall a b. (a -> b) -> a -> b
$ (PDatum Name -> Pattern' Name
forall a. PDatum a -> Pattern' a
U.PData' (Text -> [Pattern' Name] -> PDatum Name
forall a. Text -> [Pattern' a] -> PDatum a
U.DV Text
name [Pattern' Name]
args''), [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
F.concat [[Name]]
names)


-- | Make AST and give unique names for variables.
--
-- The logic here is to do normalization by evaluation for our
-- primitives. App inspects its first argument to see if it should
-- do something special. Otherwise App behaves as normal.
normAST :: U.AST' (Symbol U.AST) -> U.AST' (Symbol U.AST)
normAST :: AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
ast =
    case AST' (Symbol AST)
ast of
    U.Var Symbol AST
a           -> Symbol AST -> AST' (Symbol AST)
forall a. a -> AST' a
U.Var Symbol AST
a
    U.Lam Symbol AST
name TypeAST'
typ AST' (Symbol AST)
f  -> Symbol AST -> TypeAST' -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> TypeAST' -> AST' a -> AST' a
U.Lam Symbol AST
name TypeAST'
typ (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
f)
    U.App AST' (Symbol AST)
f AST' (Symbol AST)
x ->
        let x' :: AST' (Symbol AST)
x' = AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
x
            f' :: AST' (Symbol AST)
f' = AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
f in
        case AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a
U.withoutMeta AST' (Symbol AST)
f' of
        U.Var (TLam AST -> Symbol AST
f)      -> Symbol AST -> AST' (Symbol AST)
forall a. a -> AST' a
U.Var (Symbol AST -> AST' (Symbol AST))
-> Symbol AST -> AST' (Symbol AST)
forall a b. (a -> b) -> a -> b
$ AST -> Symbol AST
f (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
x')
        AST' (Symbol AST)
_                   -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a
U.App AST' (Symbol AST)
f' AST' (Symbol AST)
x'

    U.Let Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2          -> Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Let Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2)
    U.If AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3             -> AST' (Symbol AST)
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a -> AST' a
U.If (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e3)
    U.Ann AST' (Symbol AST)
e TypeAST'
typ1              -> AST' (Symbol AST) -> TypeAST' -> AST' (Symbol AST)
forall a. AST' a -> TypeAST' -> AST' a
U.Ann (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e) TypeAST'
typ1
    AST' (Symbol AST)
U.Infinity'               -> AST' (Symbol AST)
forall a. AST' a
U.Infinity'
    U.Integrate Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 -> Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Integrate Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e3)
    U.Summate   Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 -> Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Summate   Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e3)
    U.Product   Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 -> Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Product   Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e3)
    U.Bucket    Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 Reducer' (Symbol AST)
e3 -> Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> Reducer' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> Reducer' a -> AST' a
U.Bucket    Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
e3)
    U.ULiteral Literal'
v              -> Literal' -> AST' (Symbol AST)
forall a. Literal' -> AST' a
U.ULiteral Literal'
v
    U.NaryOp NaryOp
op [AST' (Symbol AST)]
es            -> NaryOp -> [AST' (Symbol AST)] -> AST' (Symbol AST)
forall a. NaryOp -> [AST' a] -> AST' a
U.NaryOp NaryOp
op ((AST' (Symbol AST) -> AST' (Symbol AST))
-> [AST' (Symbol AST)] -> [AST' (Symbol AST)]
forall a b. (a -> b) -> [a] -> [b]
map AST' (Symbol AST) -> AST' (Symbol AST)
normAST [AST' (Symbol AST)]
es)
    AST' (Symbol AST)
U.Unit                    -> AST' (Symbol AST)
forall a. AST' a
U.Unit
    U.Pair AST' (Symbol AST)
e1 AST' (Symbol AST)
e2              -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a
U.Pair (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2)
    U.Array  Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2       -> Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Array Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2)
    U.ArrayLiteral   [AST' (Symbol AST)]
es       -> [AST' (Symbol AST)] -> AST' (Symbol AST)
forall a. [AST' a] -> AST' a
U.ArrayLiteral ((AST' (Symbol AST) -> AST' (Symbol AST))
-> [AST' (Symbol AST)] -> [AST' (Symbol AST)]
forall a b. (a -> b) -> [a] -> [b]
map AST' (Symbol AST) -> AST' (Symbol AST)
normAST [AST' (Symbol AST)]
es)
    U.Index       AST' (Symbol AST)
e1 AST' (Symbol AST)
e2       -> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. AST' a -> AST' a -> AST' a
U.Index (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2)
    U.Case        AST' (Symbol AST)
e1 [Branch' (Symbol AST)]
e2       -> AST' (Symbol AST) -> [Branch' (Symbol AST)] -> AST' (Symbol AST)
forall a. AST' a -> [Branch' a] -> AST' a
U.Case  (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) ((Branch' (Symbol AST) -> Branch' (Symbol AST))
-> [Branch' (Symbol AST)] -> [Branch' (Symbol AST)]
forall a b. (a -> b) -> [a] -> [b]
map Branch' (Symbol AST) -> Branch' (Symbol AST)
branchNorm [Branch' (Symbol AST)]
e2)
    U.Bind   Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2       -> Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Bind   Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2)
    U.Plate  Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2       -> Symbol AST
-> AST' (Symbol AST) -> AST' (Symbol AST) -> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a
U.Plate  Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2)
    U.Chain  Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3    -> Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> AST' a -> AST' a -> AST' a -> AST' a
U.Chain  Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e3)
    U.Transform Transform'
tr SArgs' (Symbol AST)
es         -> Transform' -> SArgs' (Symbol AST) -> AST' (Symbol AST)
forall a. Transform' -> SArgs' a -> AST' a
U.Transform Transform'
tr (SArgs' (Symbol AST) -> SArgs' (Symbol AST)
normSArgs SArgs' (Symbol AST)
es)
    U.Msum [AST' (Symbol AST)]
es                 -> [AST' (Symbol AST)] -> AST' (Symbol AST)
forall a. [AST' a] -> AST' a
U.Msum ((AST' (Symbol AST) -> AST' (Symbol AST))
-> [AST' (Symbol AST)] -> [AST' (Symbol AST)]
forall a b. (a -> b) -> [a] -> [b]
map AST' (Symbol AST) -> AST' (Symbol AST)
normAST [AST' (Symbol AST)]
es)
    U.Data Symbol AST
name [Symbol AST]
tvars [TypeAST']
typs AST' (Symbol AST)
e  -> Symbol AST
-> [Symbol AST]
-> [TypeAST']
-> AST' (Symbol AST)
-> AST' (Symbol AST)
forall a. a -> [a] -> [TypeAST'] -> AST' a -> AST' a
U.Data Symbol AST
name [Symbol AST]
tvars [TypeAST']
typs AST' (Symbol AST)
e
     -- do we need to norm here? what if we try to define `true` which is already a constructor
    U.WithMeta AST' (Symbol AST)
a SourceSpan
meta         -> AST' (Symbol AST) -> SourceSpan -> AST' (Symbol AST)
forall a. AST' a -> SourceSpan -> AST' a
U.WithMeta (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
a) SourceSpan
meta

normSArgs :: U.SArgs' (Symbol U.AST) -> U.SArgs' (Symbol U.AST)
normSArgs :: SArgs' (Symbol AST) -> SArgs' (Symbol AST)
normSArgs (U.SArgs' [([Symbol AST], AST' (Symbol AST))]
es) = [([Symbol AST], AST' (Symbol AST))] -> SArgs' (Symbol AST)
forall a. [([a], AST' a)] -> SArgs' a
U.SArgs' ([([Symbol AST], AST' (Symbol AST))] -> SArgs' (Symbol AST))
-> [([Symbol AST], AST' (Symbol AST))] -> SArgs' (Symbol AST)
forall a b. (a -> b) -> a -> b
$ (([Symbol AST], AST' (Symbol AST))
 -> ([Symbol AST], AST' (Symbol AST)))
-> [([Symbol AST], AST' (Symbol AST))]
-> [([Symbol AST], AST' (Symbol AST))]
forall a b. (a -> b) -> [a] -> [b]
map ((AST' (Symbol AST) -> AST' (Symbol AST))
-> ([Symbol AST], AST' (Symbol AST))
-> ([Symbol AST], AST' (Symbol AST))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AST' (Symbol AST) -> AST' (Symbol AST)
normAST) [([Symbol AST], AST' (Symbol AST))]
es

branchNorm :: U.Branch' (Symbol U.AST) -> U.Branch' (Symbol U.AST)
branchNorm :: Branch' (Symbol AST) -> Branch' (Symbol AST)
branchNorm (U.Branch'  Pattern' Text
pat AST' (Symbol AST)
e2') = Pattern' Text -> AST' (Symbol AST) -> Branch' (Symbol AST)
forall a. Pattern' Text -> AST' a -> Branch' a
U.Branch'  Pattern' Text
pat (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2')
branchNorm (U.Branch'' Pattern' Name
pat AST' (Symbol AST)
e2') = Pattern' Name -> AST' (Symbol AST) -> Branch' (Symbol AST)
forall a. Pattern' Name -> AST' a -> Branch' a
U.Branch'' Pattern' Name
pat (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2')

redNorm :: U.Reducer' (Symbol U.AST) -> U.Reducer' (Symbol U.AST)
redNorm :: Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
ast =
    case Reducer' (Symbol AST)
ast of
     U.R_Fanout Reducer' (Symbol AST)
e1 Reducer' (Symbol AST)
e2         ->
         Reducer' (Symbol AST)
-> Reducer' (Symbol AST) -> Reducer' (Symbol AST)
forall a. Reducer' a -> Reducer' a -> Reducer' a
U.R_Fanout (Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
e1) (Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
e2)
     U.R_Index  Symbol AST
name AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 Reducer' (Symbol AST)
e3 ->
         Symbol AST
-> AST' (Symbol AST)
-> AST' (Symbol AST)
-> Reducer' (Symbol AST)
-> Reducer' (Symbol AST)
forall a. a -> AST' a -> AST' a -> Reducer' a -> Reducer' a
U.R_Index Symbol AST
name (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e2) (Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
e3)
     U.R_Split AST' (Symbol AST)
e1 Reducer' (Symbol AST)
e2 Reducer' (Symbol AST)
e3       ->
         AST' (Symbol AST)
-> Reducer' (Symbol AST)
-> Reducer' (Symbol AST)
-> Reducer' (Symbol AST)
forall a. AST' a -> Reducer' a -> Reducer' a -> Reducer' a
U.R_Split (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1) (Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
e2) (Reducer' (Symbol AST) -> Reducer' (Symbol AST)
redNorm Reducer' (Symbol AST)
e3)
     Reducer' (Symbol AST)
U.R_Nop                  -> Reducer' (Symbol AST)
forall a. Reducer' a
U.R_Nop
     U.R_Add   AST' (Symbol AST)
e1             -> AST' (Symbol AST) -> Reducer' (Symbol AST)
forall a. AST' a -> Reducer' a
U.R_Add (AST' (Symbol AST) -> AST' (Symbol AST)
normAST AST' (Symbol AST)
e1)

collapseSuperposes :: [U.AST] -> U.AST
collapseSuperposes :: [AST] -> AST
collapseSuperposes [AST]
es = Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NonEmpty (AST, AST) -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NonEmpty (abt '[] 'U, abt '[] 'U) -> Term abt 'U
U.Superpose_ ([(AST, AST)] -> NonEmpty (AST, AST)
forall a. [a] -> NonEmpty a
fromList ([(AST, AST)] -> NonEmpty (AST, AST))
-> [(AST, AST)] -> NonEmpty (AST, AST)
forall a b. (a -> b) -> a -> b
$ (AST -> [(AST, AST)]) -> [AST] -> [(AST, AST)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
F.concatMap AST -> [(AST, AST)]
go [AST]
es)
    where
    go :: U.AST -> [(U.AST, U.AST)]
    go :: AST -> [(AST, AST)]
go AST
e = AST
-> (Variable 'U -> [(AST, AST)])
-> (Term (MetaABT SourceSpan Term) 'U -> [(AST, AST)])
-> [(AST, AST)]
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 AST
e (\Variable 'U
x -> [(Ratio Integer -> AST
prob_ Ratio Integer
1, Variable 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable 'U
x)]) ((Term (MetaABT SourceSpan Term) 'U -> [(AST, AST)])
 -> [(AST, AST)])
-> (Term (MetaABT SourceSpan Term) 'U -> [(AST, AST)])
-> [(AST, AST)]
forall a b. (a -> b) -> a -> b
$ \Term (MetaABT SourceSpan Term) 'U
t ->
              case Term (MetaABT SourceSpan Term) 'U
t of
              U.Superpose_ NonEmpty (AST, AST)
es' -> NonEmpty (AST, AST) -> [(AST, AST)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList NonEmpty (AST, AST)
es'
              Term (MetaABT SourceSpan Term) 'U
_                -> [(Ratio Integer -> AST
prob_ Ratio Integer
1, AST
e)]

    prob_ :: Ratio Integer -> U.AST
    prob_ :: Ratio Integer -> AST
prob_ = Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> (Ratio Integer -> Term (MetaABT SourceSpan Term) 'U)
-> Ratio Integer
-> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some1 Literal -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
Some1 Literal -> Term abt 'U
U.Literal_ (Some1 Literal -> Term (MetaABT SourceSpan Term) 'U)
-> (Ratio Integer -> Some1 Literal)
-> Ratio Integer
-> Term (MetaABT SourceSpan Term) 'U
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal' -> Some1 Literal
U.val (Literal' -> Some1 Literal)
-> (Ratio Integer -> Literal') -> Ratio Integer -> Some1 Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ratio Integer -> Literal'
U.Prob

makeType :: U.TypeAST' -> U.SSing
makeType :: TypeAST' -> SSing
makeType (U.TypeVar Text
t) =
    case Text -> [(Text, Symbol' SSing)] -> Maybe (Symbol' SSing)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
t [(Text, Symbol' SSing)]
primTypes of
    Just (TNeu' SSing
t') -> SSing
t'
    Maybe (Symbol' SSing)
_               -> [Char] -> SSing
forall a. HasCallStack => [Char] -> a
error ([Char] -> SSing) -> [Char] -> SSing
forall a b. (a -> b) -> a -> b
$ [Char]
"Type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not a primitive"
makeType (U.TypeFun TypeAST'
f TypeAST'
x) =
    case (TypeAST' -> SSing
makeType TypeAST'
f, TypeAST' -> SSing
makeType TypeAST'
x) of
    (U.SSing Sing a
f', U.SSing Sing a
x') -> Sing (a ':-> a) -> SSing
forall (a :: Hakaru). Sing a -> SSing
U.SSing (Sing (a ':-> a) -> SSing) -> Sing (a ':-> a) -> SSing
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> Sing (a ':-> a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':-> b)
SFun Sing a
f' Sing a
x'
makeType (U.TypeApp Text
f [TypeAST']
args) =
    case Text -> [(Text, Symbol' SSing)] -> Maybe (Symbol' SSing)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
f [(Text, Symbol' SSing)]
primTypes of
    Just (TLam' [SSing] -> SSing
f') -> [SSing] -> SSing
f' ((TypeAST' -> SSing) -> [TypeAST'] -> [SSing]
forall a b. (a -> b) -> [a] -> [b]
map TypeAST' -> SSing
makeType [TypeAST']
args)
    Maybe (Symbol' SSing)
_               -> [Char] -> SSing
forall a. HasCallStack => [Char] -> a
error ([Char] -> SSing) -> [Char] -> SSing
forall a b. (a -> b) -> a -> b
$ [Char]
"Type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not a primitive"


makePattern :: U.Pattern' U.Name -> U.Pattern
makePattern :: Pattern' Name -> Pattern
makePattern Pattern' Name
U.PWild'        = Pattern
U.PWild
makePattern (U.PVar' Name
name)  =
    case Text -> [(Text, Symbol' Pattern)] -> Maybe (Symbol' Pattern)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name -> Text
U.hintID Name
name) [(Text, Symbol' Pattern)]
primPat of
    Just (TLam' [Pattern] -> Pattern
_)  -> [Char] -> Pattern
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO{makePattern:PVar:TLam}"
    Just (TNeu' Pattern
p') -> Pattern
p'
    Maybe (Symbol' Pattern)
Nothing         -> Name -> Pattern
U.PVar Name
name
makePattern (U.PData' (U.DV Text
name [Pattern' Name]
args)) =
    case Text -> [(Text, Symbol' Pattern)] -> Maybe (Symbol' Pattern)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
name [(Text, Symbol' Pattern)]
primPat of
    Just (TLam' [Pattern] -> Pattern
f') -> [Pattern] -> Pattern
f' ((Pattern' Name -> Pattern) -> [Pattern' Name] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map Pattern' Name -> Pattern
makePattern [Pattern' Name]
args)
    Just (TNeu' Pattern
p') -> Pattern
p'
    Maybe (Symbol' Pattern)
Nothing -> [Char] -> Pattern
forall a. HasCallStack => [Char] -> a
error ([Char] -> Pattern) -> [Char] -> Pattern
forall a b. (a -> b) -> a -> b
$ [Char]
"Data constructor " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not found"

makeBranch :: U.Branch' (Symbol U.AST) -> U.Branch
makeBranch :: Branch' (Symbol AST) -> Branch
makeBranch (U.Branch'' Pattern' Name
pat AST' (Symbol AST)
ast) = Pattern -> AST -> Branch
forall k (abt :: [k] -> Untyped -> *).
Pattern -> abt '[] 'U -> Branch_ abt
U.Branch_ (Pattern' Name -> Pattern
makePattern Pattern' Name
pat) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
ast)
makeBranch (U.Branch'  Pattern' Text
_   AST' (Symbol AST)
_)   = [Char] -> Branch
forall a. HasCallStack => [Char] -> a
error [Char]
"branch was not symbol resolved"

makeTrue, makeFalse :: U.AST' (Symbol U.AST) -> U.Branch
makeTrue :: AST' (Symbol AST) -> Branch
makeTrue  AST' (Symbol AST)
e =
    Pattern -> AST -> Branch
forall k (abt :: [k] -> Untyped -> *).
Pattern -> abt '[] 'U -> Branch_ abt
U.Branch_ (Pattern' Name -> Pattern
makePattern (PDatum Name -> Pattern' Name
forall a. PDatum a -> Pattern' a
U.PData' (Text -> [Pattern' Name] -> PDatum Name
forall a. Text -> [Pattern' a] -> PDatum a
U.DV Text
"true"  []))) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e)
makeFalse :: AST' (Symbol AST) -> Branch
makeFalse AST' (Symbol AST)
e =
    Pattern -> AST -> Branch
forall k (abt :: [k] -> Untyped -> *).
Pattern -> abt '[] 'U -> Branch_ abt
U.Branch_ (Pattern' Name -> Pattern
makePattern (PDatum Name -> Pattern' Name
forall a. PDatum a -> Pattern' a
U.PData' (Text -> [Pattern' Name] -> PDatum Name
forall a. Text -> [Pattern' a] -> PDatum a
U.DV Text
"false" []))) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e)

makeReducerAST
    :: Variable 'U.U
    -> U.Reducer' (Symbol U.AST)
    -> List1 Variable xs
    -> U.Reducer xs U.U_ABT 'U.U
makeReducerAST :: Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
i Reducer' (Symbol AST)
r1 List1 Variable xs
bs =
    case Reducer' (Symbol AST)
r1 of
    U.R_Fanout Reducer' (Symbol AST)
r2 Reducer' (Symbol AST)
r3       -> Reducer xs (MetaABT SourceSpan Term) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]) (abt :: [Untyped] -> Untyped -> *).
Reducer xs abt 'U -> Reducer xs abt 'U -> Reducer xs abt 'U
U.R_Fanout_
                              (Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]).
Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
i Reducer' (Symbol AST)
r2 List1 Variable xs
bs)
                              (Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]).
Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
i Reducer' (Symbol AST)
r3 List1 Variable xs
bs)
    U.R_Index  Symbol AST
b  AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 Reducer' (Symbol AST)
r1 -> [Char]
-> Symbol AST
-> (Variable 'U -> Reducer xs (MetaABT SourceSpan Term) 'U)
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.R_Index" Symbol AST
b ((Variable 'U -> Reducer xs (MetaABT SourceSpan Term) 'U)
 -> Reducer xs (MetaABT SourceSpan Term) 'U)
-> (Variable 'U -> Reducer xs (MetaABT SourceSpan Term) 'U)
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall a b. (a -> b) -> a -> b
$ \Variable 'U
b' ->
                                Variable 'U
-> MetaABT SourceSpan Term xs 'U
-> MetaABT SourceSpan Term ('U : xs) 'U
-> Reducer ('U : xs) (MetaABT SourceSpan Term) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *) (xs :: [Untyped]).
Variable 'U
-> abt xs 'U
-> abt ('U : xs) 'U
-> Reducer ('U : xs) abt 'U
-> Reducer xs abt 'U
U.R_Index_
                                Variable 'U
b' -- HACK: This shouldn't be needed here
                                (List1 Variable xs -> AST -> MetaABT SourceSpan Term xs 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
bs (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1))
                                (Variable 'U
-> MetaABT SourceSpan Term xs 'U
-> MetaABT SourceSpan Term ('U : xs) 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
i (List1 Variable xs -> AST -> MetaABT SourceSpan Term xs 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
bs (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)))
                                (Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable ('U : xs)
-> Reducer ('U : xs) (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]).
Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
i Reducer' (Symbol AST)
r1 (Variable 'U -> List1 Variable xs -> List1 Variable ('U : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 Variable 'U
b' List1 Variable xs
bs))
    U.R_Split  AST' (Symbol AST)
e1 Reducer' (Symbol AST)
r2 Reducer' (Symbol AST)
r3    -> MetaABT SourceSpan Term ('U : xs) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *) (xs :: [Untyped]).
abt ('U : xs) 'U
-> Reducer xs abt 'U -> Reducer xs abt 'U -> Reducer xs abt 'U
U.R_Split_
                              (Variable 'U
-> MetaABT SourceSpan Term xs 'U
-> MetaABT SourceSpan Term ('U : xs) 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
i (List1 Variable xs -> AST -> MetaABT SourceSpan Term xs 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
bs (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1)))
                              (Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]).
Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
i Reducer' (Symbol AST)
r2 List1 Variable xs
bs)
                              (Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]).
Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
i Reducer' (Symbol AST)
r3 List1 Variable xs
bs)
    Reducer' (Symbol AST)
U.R_Nop                -> Reducer xs (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]) (abt :: [Untyped] -> Untyped -> *).
Reducer xs abt 'U
U.R_Nop_
    U.R_Add AST' (Symbol AST)
e1             -> MetaABT SourceSpan Term ('U : xs) 'U
-> Reducer xs (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *) (xs :: [Untyped]).
abt ('U : xs) 'U -> Reducer xs abt 'U
U.R_Add_ (Variable 'U
-> MetaABT SourceSpan Term xs 'U
-> MetaABT SourceSpan Term ('U : xs) 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
i (List1 Variable xs -> AST -> MetaABT SourceSpan Term xs 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
bs (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1)))

makeAST :: U.AST' (Symbol U.AST) -> U.AST
makeAST :: AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
ast =
    case AST' (Symbol AST)
ast of
    -- TODO: Add to Symbol datatype: gensymed names and types
    -- for primitives (type for arg on lam, return type in neu)
    U.Var (TLam AST -> Symbol AST
_) ->
        [Char] -> AST
forall a. HasCallStack => [Char] -> a
error [Char]
"makeAST: Passed primitive with wrong number of arguments"
    U.Var (TNeu AST
e) -> AST
e
    U.Lam Symbol AST
s TypeAST'
typ AST' (Symbol AST)
e1 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Lam" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SSing
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SSing -> abt '[ 'U] 'U -> Term abt 'U
U.Lam_ (TypeAST' -> SSing
makeType TypeAST'
typ) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1)
    U.App AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 ->
        Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[] 'U -> Term abt 'U
U.App_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)
    U.Let Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Let" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Let_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)
    U.If AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 ->
        Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST -> [Branch] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> [Branch_ abt] -> Term abt 'U
U.Case_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) [(AST' (Symbol AST) -> Branch
makeTrue AST' (Symbol AST)
e2), (AST' (Symbol AST) -> Branch
makeFalse AST' (Symbol AST)
e3)]
    U.Ann AST' (Symbol AST)
e TypeAST'
typ       -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ SSing -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
SSing -> abt '[] 'U -> Term abt 'U
U.Ann_ (TypeAST' -> SSing
makeType TypeAST'
typ) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e)
    AST' (Symbol AST)
U.Infinity'       -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ PrimOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
PrimOp -> [abt '[] 'U] -> Term abt 'U
U.PrimOp_ PrimOp
U.Infinity []
    U.ULiteral Literal'
v      -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ Some1 Literal -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
Some1 Literal -> Term abt 'U
U.Literal_  (Literal' -> Some1 Literal
U.val Literal'
v)
    U.NaryOp NaryOp
op [AST' (Symbol AST)]
es    -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ NaryOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
NaryOp -> [abt '[] 'U] -> Term abt 'U
U.NaryOp_ NaryOp
op ((AST' (Symbol AST) -> AST) -> [AST' (Symbol AST)] -> [AST]
forall a b. (a -> b) -> [a] -> [b]
map AST' (Symbol AST) -> AST
makeAST [AST' (Symbol AST)]
es)
    AST' (Symbol AST)
U.Unit            -> AST
unit_
    U.Pair AST' (Symbol AST)
e1 AST' (Symbol AST)
e2      -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST -> AST -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[] 'U -> Term abt 'U
U.Pair_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)
    U.Array Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Array" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Array_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)
    U.ArrayLiteral [AST' (Symbol AST)]
es -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
[abt '[] 'U] -> Term abt 'U
U.ArrayLiteral_ ((AST' (Symbol AST) -> AST) -> [AST' (Symbol AST)] -> [AST]
forall a b. (a -> b) -> [a] -> [b]
map AST' (Symbol AST) -> AST
makeAST [AST' (Symbol AST)]
es)
    U.Index AST' (Symbol AST)
e1 AST' (Symbol AST)
e2     -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ ArrayOp -> [AST] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
ArrayOp -> [abt '[] 'U] -> Term abt 'U
U.ArrayOp_ ArrayOp
U.Index_ [(AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1), (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)]
    U.Case AST' (Symbol AST)
e [Branch' (Symbol AST)]
bs       -> Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST -> [Branch] -> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> [Branch_ abt] -> Term abt 'U
U.Case_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e) ((Branch' (Symbol AST) -> Branch)
-> [Branch' (Symbol AST)] -> [Branch]
forall a b. (a -> b) -> [a] -> [b]
map Branch' (Symbol AST) -> Branch
makeBranch [Branch' (Symbol AST)]
bs)
    U.Bind Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Bind" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.MBind_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)
    U.Plate Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Plate" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Plate_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2)
    U.Chain Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Chain" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Chain_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e3)
    U.Integrate Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Integrate" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Integrate_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e3)
    U.Summate Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Summate" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Summate_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e3)
    U.Product Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 AST' (Symbol AST)
e3 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Product" Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> AST
-> MetaABT SourceSpan Term '[ 'U] 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *).
abt '[] 'U -> abt '[] 'U -> abt '[ 'U] 'U -> Term abt 'U
U.Product_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2) (Variable 'U -> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
name (AST -> MetaABT SourceSpan Term '[ 'U] 'U)
-> AST -> MetaABT SourceSpan Term '[ 'U] 'U
forall a b. (a -> b) -> a -> b
$ AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e3)
    U.Bucket Symbol AST
s AST' (Symbol AST)
e1 AST' (Symbol AST)
e2 Reducer' (Symbol AST)
e3 ->
        [Char] -> Symbol AST -> (Variable 'U -> AST) -> AST
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.Bucket"  Symbol AST
s ((Variable 'U -> AST) -> AST) -> (Variable 'U -> AST) -> AST
forall a b. (a -> b) -> a -> b
$ \Variable 'U
name ->
            Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Term (MetaABT SourceSpan Term) 'U -> AST
forall a b. (a -> b) -> a -> b
$ AST
-> AST
-> Reducer '[] (MetaABT SourceSpan Term) 'U
-> Term (MetaABT SourceSpan Term) 'U
forall (abt :: [Untyped] -> Untyped -> *) (xs :: [Untyped]).
abt '[] 'U -> abt '[] 'U -> Reducer xs abt 'U -> Term abt 'U
U.Bucket_ (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e1) (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e2) (Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable '[]
-> Reducer '[] (MetaABT SourceSpan Term) 'U
forall (xs :: [Untyped]).
Variable 'U
-> Reducer' (Symbol AST)
-> List1 Variable xs
-> Reducer xs (MetaABT SourceSpan Term) 'U
makeReducerAST Variable 'U
name Reducer' (Symbol AST)
e3 List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1)
    U.Transform Transform'
tr SArgs' (Symbol AST)
es -> Transform' -> SArgs' (Symbol AST) -> AST
makeTransform Transform'
tr SArgs' (Symbol AST)
es
    U.Msum [AST' (Symbol AST)]
es -> [AST] -> AST
collapseSuperposes ((AST' (Symbol AST) -> AST) -> [AST' (Symbol AST)] -> [AST]
forall a b. (a -> b) -> [a] -> [b]
map AST' (Symbol AST) -> AST
makeAST [AST' (Symbol AST)]
es)
    U.Data Symbol AST
name [Symbol AST]
tvars [TypeAST']
typs AST' (Symbol AST)
e -> [Char] -> AST
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: makeAST{U.Data}" 
    U.WithMeta AST' (Symbol AST)
a SourceSpan
meta -> SourceSpan -> AST -> AST
forall k meta (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
       (a :: k).
meta -> MetaABT meta syn xs a -> MetaABT meta syn xs a
withMetadata SourceSpan
meta (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
a)

makeTransform :: U.Transform' -> U.SArgs' (Symbol U.AST) -> U.AST
makeTransform :: Transform' -> SArgs' (Symbol AST) -> AST
makeTransform Transform'
tru SArgs' (Symbol AST)
esu =
  case Transform' -> Some2 Transform
typedTransform Transform'
tru of
    Some2 Transform i j
tr ->
      let wrongArgsErr :: AST
wrongArgsErr = [Char] -> AST
forall a. HasCallStack => [Char] -> a
error ([Char] -> AST) -> [Char] -> AST
forall a b. (a -> b) -> a -> b
$ [Char]
"Wrong number of arguments passed to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                 Transform i j -> [Char]
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
Transform args a -> [Char]
T.transformName Transform i j
tr
          res :: Maybe (Term (MetaABT SourceSpan Term) 'U)
res = Transform i j
-> SArgs (MetaABT SourceSpan Term) i
-> Term (MetaABT SourceSpan Term) 'U
forall (as :: [([Hakaru], Hakaru)]) (x :: Hakaru)
       (abt :: [Untyped] -> Untyped -> *).
Transform as x -> SArgs abt as -> Term abt 'U
U.Transform_ Transform i j
tr (SArgs (MetaABT SourceSpan Term) i
 -> Term (MetaABT SourceSpan Term) 'U)
-> Maybe (SArgs (MetaABT SourceSpan Term) i)
-> Maybe (Term (MetaABT SourceSpan Term) 'U)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SArgsSpine i
-> SArgs' (Symbol AST) -> Maybe (SArgs (MetaABT SourceSpan Term) i)
forall k (xs :: [([k], k)]).
SArgsSpine xs
-> SArgs' (Symbol AST)
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
matchSArgs (Transform i j -> SArgsSpine i
forall (xs :: [([Hakaru], Hakaru)]) (a :: Hakaru).
Transform xs a -> SArgsSpine xs
transformArgs Transform i j
tr) SArgs' (Symbol AST)
esu
      in AST
-> (Term (MetaABT SourceSpan Term) 'U -> AST)
-> Maybe (Term (MetaABT SourceSpan Term) 'U)
-> AST
forall b a. b -> (a -> b) -> Maybe a -> b
maybe AST
wrongArgsErr Term (MetaABT SourceSpan Term) 'U -> AST
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Maybe (Term (MetaABT SourceSpan Term) 'U)
res

type SVarsSpine = (List1 (Lift1 ()) :: [k] -> *)
type SArgsSpine = (List1 (PointwiseP SVarsSpine (Lift1 ())) :: [([k],k1)] -> *)

transformArgs :: T.Transform xs a -> SArgsSpine xs
transformArgs :: Transform xs a -> SArgsSpine xs
transformArgs Transform xs a
t =
  let arg0 :: PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 = List1 a '[]
-> Lift1 () y -> PointwiseP (List1 a) (Lift1 ()) '( '[], y)
forall k k (f :: k -> *) (x :: k) (g :: k -> *) (y :: k).
f x -> g y -> PointwiseP f g '(x, y)
PwP List1 a '[]
forall k (a :: k -> *). List1 a '[]
Nil1 (() -> Lift1 () y
forall k a (i :: k). a -> Lift1 a i
Lift1 ())
      arg1 :: PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[x], y)
arg1 = List1 (Lift1 ()) '[x]
-> Lift1 () y
-> PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[x], y)
forall k k (f :: k -> *) (x :: k) (g :: k -> *) (y :: k).
f x -> g y -> PointwiseP f g '(x, y)
PwP (Lift1 () x -> List1 (Lift1 ()) '[] -> List1 (Lift1 ()) '[x]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 (() -> Lift1 () x
forall k a (i :: k). a -> Lift1 a i
Lift1 ()) List1 (Lift1 ()) '[]
forall k (a :: k -> *). List1 a '[]
Nil1) (() -> Lift1 () y
forall k a (i :: k). a -> Lift1 a i
Lift1 ())
  in case Transform xs a
t of
     -- TODO: can SingI be generalized to allow things which aren't `Sing's
     -- so these right hand sides can become `sing'?
       Transform xs a
T.Observe   -> PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], 'HMeasure a), '( '[], a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 (List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
 -> List1
      (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
      '[ '( '[], 'HMeasure a), '( '[], a)])
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], 'HMeasure a), '( '[], a)]
forall a b. (a -> b) -> a -> b
$ PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       Transform xs a
T.MH        -> PointwiseP
  (List1 (Lift1 ())) (Lift1 ()) '( '[], a ':-> 'HMeasure a)
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], a ':-> 'HMeasure a), '( '[], 'HMeasure a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP
  (List1 (Lift1 ())) (Lift1 ()) '( '[], a ':-> 'HMeasure a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 (List1
   (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
 -> List1
      (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
      '[ '( '[], a ':-> 'HMeasure a), '( '[], 'HMeasure a)])
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], a ':-> 'HMeasure a), '( '[], 'HMeasure a)]
forall a b. (a -> b) -> a -> b
$ PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       Transform xs a
T.MCMC      -> PointwiseP
  (List1 (Lift1 ())) (Lift1 ()) '( '[], a ':-> 'HMeasure a)
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], a ':-> 'HMeasure a), '( '[], 'HMeasure a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP
  (List1 (Lift1 ())) (Lift1 ()) '( '[], a ':-> 'HMeasure a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 (List1
   (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
 -> List1
      (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
      '[ '( '[], a ':-> 'HMeasure a), '( '[], 'HMeasure a)])
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], a ':-> 'HMeasure a), '( '[], 'HMeasure a)]
forall a b. (a -> b) -> a -> b
$ PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], 'HMeasure a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       T.Disint TransformImpl
k  -> PointwiseP
  (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure (HPair a b))
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], 'HMeasure (HPair a b))]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP
  (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure (HPair a b))
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       Transform xs a
T.Summarize -> PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       Transform xs a
T.Simplify  -> PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       Transform xs a
T.Reparam   -> PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[], a)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
       Transform xs a
T.Expect    -> PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[a], 'HProb)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], 'HMeasure a), '( '[a], 'HProb)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[], 'HMeasure a)
forall k k (a :: k -> *) (y :: k).
PointwiseP (List1 a) (Lift1 ()) '( '[], y)
arg0 (List1
   (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[a], 'HProb)]
 -> List1
      (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
      '[ '( '[], 'HMeasure a), '( '[a], 'HProb)])
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[a], 'HProb)]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ()))
     '[ '( '[], 'HMeasure a), '( '[a], 'HProb)]
forall a b. (a -> b) -> a -> b
$ PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[a], 'HProb)
-> List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
-> List1
     (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[ '( '[a], 'HProb)]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[a], 'HProb)
forall a k (x :: a) (y :: k).
PointwiseP (List1 (Lift1 ())) (Lift1 ()) '( '[x], y)
arg1 List1 (PointwiseP (List1 (Lift1 ())) (Lift1 ())) '[]
forall k (a :: k -> *). List1 a '[]
Nil1

matchSArgs :: SArgsSpine xs -> U.SArgs' (Symbol U.AST)
           -> Maybe (U.SArgs U.U_ABT xs)
matchSArgs :: SArgsSpine xs
-> SArgs' (Symbol AST)
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
matchSArgs SArgsSpine xs
sp (U.SArgs' [([Symbol AST], AST' (Symbol AST))]
es) =
  case (SArgsSpine xs
sp, [([Symbol AST], AST' (Symbol AST))]
es) of
    ( SArgsSpine xs
Nil1, [] ) -> SArgs (MetaABT SourceSpan Term) '[]
-> Maybe (SArgs (MetaABT SourceSpan Term) '[])
forall a. a -> Maybe a
Just SArgs (MetaABT SourceSpan Term) '[]
forall k (abt :: [Untyped] -> Untyped -> *). SArgs abt '[]
U.End
    ( Cons1 (PwP SVarsSpine x
vs Lift1 () y
_) List1 (PointwiseP SVarsSpine (Lift1 ())) xs
sp', ([Symbol AST]
vs',AST' (Symbol AST)
e0):[([Symbol AST], AST' (Symbol AST))]
es' )
      -> Maybe (Maybe (SArgs (MetaABT SourceSpan Term) xs))
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (SArgs (MetaABT SourceSpan Term) xs))
 -> Maybe (SArgs (MetaABT SourceSpan Term) xs))
-> Maybe (Maybe (SArgs (MetaABT SourceSpan Term) xs))
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
forall a b. (a -> b) -> a -> b
$ SVarsSpine x
-> [Symbol AST]
-> AST' (Symbol AST)
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped x vsu
    -> U_ABT vsu 'U -> Maybe (SArgs (MetaABT SourceSpan Term) xs))
-> Maybe (Maybe (SArgs (MetaABT SourceSpan Term) xs))
forall k (vs :: [k]) r.
SVarsSpine vs
-> [Symbol AST]
-> AST' (Symbol AST)
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped vs vsu -> U_ABT vsu 'U -> r)
-> Maybe r
matchSVars SVarsSpine x
vs [Symbol AST]
vs' AST' (Symbol AST)
e0 ((forall (vsu :: [Untyped]).
  List2 ToUntyped x vsu
  -> U_ABT vsu 'U -> Maybe (SArgs (MetaABT SourceSpan Term) xs))
 -> Maybe (Maybe (SArgs (MetaABT SourceSpan Term) xs)))
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped x vsu
    -> U_ABT vsu 'U -> Maybe (SArgs (MetaABT SourceSpan Term) xs))
-> Maybe (Maybe (SArgs (MetaABT SourceSpan Term) xs))
forall a b. (a -> b) -> a -> b
$ \List2 ToUntyped x vsu
vsu U_ABT vsu 'U
e0' ->
           (List2 ToUntyped x vsu, U_ABT vsu 'U)
-> SArgs (MetaABT SourceSpan Term) xs
-> SArgs (MetaABT SourceSpan Term) ('(x, y) : xs)
forall k (vars :: [k]) (varsu :: [Untyped])
       (abt :: [Untyped] -> Untyped -> *) (args :: [([k], k)]) (a :: k).
(List2 ToUntyped vars varsu, abt varsu 'U)
-> SArgs abt args -> SArgs abt ('(vars, a) : args)
(U.:*) (List2 ToUntyped x vsu
vsu, U_ABT vsu 'U
e0') (SArgs (MetaABT SourceSpan Term) xs
 -> SArgs (MetaABT SourceSpan Term) ('(x, y) : xs))
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
-> Maybe (SArgs (MetaABT SourceSpan Term) ('(x, y) : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (PointwiseP SVarsSpine (Lift1 ())) xs
-> SArgs' (Symbol AST)
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
forall k (xs :: [([k], k)]).
SArgsSpine xs
-> SArgs' (Symbol AST)
-> Maybe (SArgs (MetaABT SourceSpan Term) xs)
matchSArgs List1 (PointwiseP SVarsSpine (Lift1 ())) xs
sp' ([([Symbol AST], AST' (Symbol AST))] -> SArgs' (Symbol AST)
forall a. [([a], AST' a)] -> SArgs' a
U.SArgs' [([Symbol AST], AST' (Symbol AST))]
es')
    (SArgsSpine xs, [([Symbol AST], AST' (Symbol AST))])
_ -> Maybe (SArgs (MetaABT SourceSpan Term) xs)
forall a. Maybe a
Nothing

matchSVars :: SVarsSpine vs -> [Symbol U.AST] -> U.AST' (Symbol U.AST)
           -> (forall vsu . List2 U.ToUntyped vs vsu
                         -> U.U_ABT vsu 'U.U
                         -> r)
           -> Maybe r
matchSVars :: SVarsSpine vs
-> [Symbol AST]
-> AST' (Symbol AST)
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped vs vsu -> U_ABT vsu 'U -> r)
-> Maybe r
matchSVars SVarsSpine vs
vs [Symbol AST]
nms AST' (Symbol AST)
e forall (vsu :: [Untyped]).
List2 ToUntyped vs vsu -> U_ABT vsu 'U -> r
k =
  case (SVarsSpine vs
vs, [Symbol AST]
nms) of
    (SVarsSpine vs
Nil1       , []     ) -> r -> Maybe r
forall a. a -> Maybe a
Just (r -> Maybe r) -> r -> Maybe r
forall a b. (a -> b) -> a -> b
$ List2 ToUntyped vs '[] -> AST -> r
forall (vsu :: [Untyped]).
List2 ToUntyped vs vsu -> U_ABT vsu 'U -> r
k List2 ToUntyped vs '[]
forall k0 k1 (f :: k0 -> k1 -> *). List2 f '[] '[]
Nil2 (AST' (Symbol AST) -> AST
makeAST AST' (Symbol AST)
e)
    (Cons1 Lift1 () x
v List1 (Lift1 ()) xs
vs', Symbol AST
nm:[Symbol AST]
nms') ->
      List1 (Lift1 ()) xs
-> [Symbol AST]
-> AST' (Symbol AST)
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped xs vsu -> U_ABT vsu 'U -> r)
-> Maybe r
forall k (vs :: [k]) r.
SVarsSpine vs
-> [Symbol AST]
-> AST' (Symbol AST)
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped vs vsu -> U_ABT vsu 'U -> r)
-> Maybe r
matchSVars List1 (Lift1 ()) xs
vs' [Symbol AST]
nms' AST' (Symbol AST)
e ((forall (vsu :: [Untyped]).
  List2 ToUntyped xs vsu -> U_ABT vsu 'U -> r)
 -> Maybe r)
-> (forall (vsu :: [Untyped]).
    List2 ToUntyped xs vsu -> U_ABT vsu 'U -> r)
-> Maybe r
forall a b. (a -> b) -> a -> b
$ \List2 ToUntyped xs vsu
vsu U_ABT vsu 'U
e' ->
        [Char] -> Symbol AST -> (Variable 'U -> r) -> r
forall r. [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
"U.SArgs" Symbol AST
nm ((Variable 'U -> r) -> r) -> (Variable 'U -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Variable 'U
nm' ->
          List2 ToUntyped vs ('U : vsu) -> U_ABT ('U : vsu) 'U -> r
forall (vsu :: [Untyped]).
List2 ToUntyped vs vsu -> U_ABT vsu 'U -> r
k (ToUntyped x 'U
-> List2 ToUntyped xs vsu -> List2 ToUntyped (x : xs) ('U : vsu)
forall a a (f :: a -> a -> *) (x :: a) (y :: a) (xs :: [a])
       (ys :: [a]).
f x y -> List2 f xs ys -> List2 f (x : xs) (y : ys)
Cons2 ToUntyped x 'U
forall k (x :: k). ToUntyped x 'U
U.ToU List2 ToUntyped xs vsu
vsu) (Variable 'U -> U_ABT vsu 'U -> U_ABT ('U : vsu) 'U
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'U
nm' U_ABT vsu 'U
e')
    (SVarsSpine vs, [Symbol AST])
_ -> Maybe r
forall a. Maybe a
Nothing

typedTransform :: U.Transform' -> Some2 T.Transform
typedTransform :: Transform' -> Some2 Transform
typedTransform = \case
  Transform'
U.Observe   -> Transform '[LC ('HMeasure Any), LC Any] ('HMeasure Any)
-> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform '[LC ('HMeasure Any), LC Any] ('HMeasure Any)
forall (a :: Hakaru).
Transform '[LC ('HMeasure a), LC a] ('HMeasure a)
T.Observe
  Transform'
U.MH        -> Transform
  '[LC (Any ':-> 'HMeasure Any), LC ('HMeasure Any)]
  (Any ':-> 'HMeasure (HPair Any 'HProb))
-> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform
  '[LC (Any ':-> 'HMeasure Any), LC ('HMeasure Any)]
  (Any ':-> 'HMeasure (HPair Any 'HProb))
forall (a :: Hakaru).
Transform
  '[LC (a ':-> 'HMeasure a), LC ('HMeasure a)]
  (a ':-> 'HMeasure (HPair a 'HProb))
T.MH
  Transform'
U.MCMC      -> Transform
  '[LC (Any ':-> 'HMeasure Any), LC ('HMeasure Any)]
  (Any ':-> 'HMeasure Any)
-> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform
  '[LC (Any ':-> 'HMeasure Any), LC ('HMeasure Any)]
  (Any ':-> 'HMeasure Any)
forall (a :: Hakaru).
Transform
  '[LC (a ':-> 'HMeasure a), LC ('HMeasure a)] (a ':-> 'HMeasure a)
T.MCMC
  U.Disint TransformImpl
k  -> Transform
  '[LC ('HMeasure (HPair Any Any))] (Any ':-> 'HMeasure Any)
-> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 (Transform
   '[LC ('HMeasure (HPair Any Any))] (Any ':-> 'HMeasure Any)
 -> Some2 Transform)
-> Transform
     '[LC ('HMeasure (HPair Any Any))] (Any ':-> 'HMeasure Any)
-> Some2 Transform
forall a b. (a -> b) -> a -> b
$ TransformImpl
-> Transform
     '[LC ('HMeasure (HPair Any Any))] (Any ':-> 'HMeasure Any)
forall (a :: Hakaru) (b :: Hakaru).
TransformImpl
-> Transform '[LC ('HMeasure (HPair a b))] (a ':-> 'HMeasure b)
T.Disint TransformImpl
k
  Transform'
U.Summarize -> Transform '[LC Any] Any -> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform '[LC Any] Any
forall (a :: Hakaru). Transform '[LC a] a
T.Summarize
  Transform'
U.Simplify  -> Transform '[LC Any] Any -> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform '[LC Any] Any
forall (a :: Hakaru). Transform '[LC a] a
T.Simplify
  Transform'
U.Reparam   -> Transform '[LC Any] Any -> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform '[LC Any] Any
forall (a :: Hakaru). Transform '[LC a] a
T.Reparam
  Transform'
U.Expect    -> Transform '[LC ('HMeasure Any), '( '[Any], 'HProb)] 'HProb
-> Some2 Transform
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 Transform '[LC ('HMeasure Any), '( '[Any], 'HProb)] 'HProb
forall (a :: Hakaru).
Transform '[LC ('HMeasure a), '( '[a], 'HProb)] 'HProb
T.Expect

withName :: String -> Symbol U.AST -> (Variable 'U.U -> r) -> r
withName :: [Char] -> Symbol AST -> (Variable 'U -> r) -> r
withName [Char]
fun Symbol AST
s Variable 'U -> r
k =
    case Symbol AST
s of
    TNeu AST
e -> AST
-> (Variable 'U -> r)
-> (Term (MetaABT SourceSpan Term) 'U -> r)
-> r
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 AST
e Variable 'U -> r
k ([Char] -> Term (MetaABT SourceSpan Term) 'U -> r
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term (MetaABT SourceSpan Term) 'U -> r)
-> [Char] -> Term (MetaABT SourceSpan Term) 'U -> r
forall a b. (a -> b) -> a -> b
$ [Char]
"makeAST: bad " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fun)
    Symbol AST
_      -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error ([Char] -> r) -> [Char] -> r
forall a b. (a -> b) -> a -> b
$ [Char]
"makeAST: bad " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fun

resolveAST :: U.AST' Text -> U.AST
resolveAST :: AST' Text -> AST
resolveAST AST' Text
ast =
    AST -> AST
coalesce (AST -> AST)
-> (AST' (Symbol AST) -> AST) -> AST' (Symbol AST) -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    AST' (Symbol AST) -> AST
makeAST  (AST' (Symbol AST) -> AST)
-> (AST' (Symbol AST) -> AST' (Symbol AST))
-> AST' (Symbol AST)
-> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    AST' (Symbol AST) -> AST' (Symbol AST)
normAST (AST' (Symbol AST) -> AST) -> AST' (Symbol AST) -> AST
forall a b. (a -> b) -> a -> b
$
    State Int (AST' (Symbol AST)) -> Int -> AST' (Symbol AST)
forall s a. State s a -> s -> a
evalState (SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution SymbolTable
primTable AST' Text
ast) Int
0

resolveAST'
    :: N.Nat
    -> [U.Name]
    -> U.AST' Text
    -> U.AST
resolveAST' :: Nat -> [Name] -> AST' Text -> AST
resolveAST' Nat
nextVar [Name]
syms AST' Text
ast =
    AST -> AST
coalesce (AST -> AST)
-> (AST' (Symbol AST) -> AST) -> AST' (Symbol AST) -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    AST' (Symbol AST) -> AST
makeAST  (AST' (Symbol AST) -> AST)
-> (AST' (Symbol AST) -> AST' (Symbol AST))
-> AST' (Symbol AST)
-> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    AST' (Symbol AST) -> AST' (Symbol AST)
normAST  (AST' (Symbol AST) -> AST) -> AST' (Symbol AST) -> AST
forall a b. (a -> b) -> a -> b
$
    State Int (AST' (Symbol AST)) -> Int -> AST' (Symbol AST)
forall s a. State s a -> s -> a
evalState (SymbolTable -> AST' Text -> State Int (AST' (Symbol AST))
symbolResolution
        ([Name] -> SymbolTable -> SymbolTable
insertSymbols [Name]
syms SymbolTable
primTable) AST' Text
ast)
        (Nat -> Int
N.fromNat (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ [Name] -> Nat
nextVarID_ [Name]
syms)
    where
    nextVarID_ :: [Name] -> Nat
nextVarID_ [] = Nat
nextVar
    nextVarID_ [Name]
xs = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
nextVar (Nat -> Nat) -> ([Nat] -> Nat) -> [Nat] -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+) (Nat -> Nat) -> ([Nat] -> Nat) -> [Nat] -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Nat] -> Nat
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
F.maximum ([Nat] -> Nat) -> [Nat] -> Nat
forall a b. (a -> b) -> a -> b
$ (Name -> Nat) -> [Name] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Nat
U.nameID [Name]
xs

makeName :: SomeVariable ('KProxy :: KProxy Hakaru) -> U.Name
makeName :: SomeVariable 'KProxy -> Name
makeName (SomeVariable (Variable Text
hint Nat
vID Sing a
_)) = Nat -> Text -> Name
U.Name Nat
vID Text
hint

fromVarSet :: VarSet ('KProxy :: KProxy Hakaru) -> [U.Name]
fromVarSet :: VarSet 'KProxy -> [Name]
fromVarSet (VarSet IntMap (SomeVariable 'KProxy)
xs) = (SomeVariable 'KProxy -> Name) -> [SomeVariable 'KProxy] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map SomeVariable 'KProxy -> Name
makeName (IntMap (SomeVariable 'KProxy) -> [SomeVariable 'KProxy]
forall a. IntMap a -> [a]
IM.elems IntMap (SomeVariable 'KProxy)
xs)