{-# LANGUAGE CPP #-}

-- | Optimize Feldspar expressions

module Feldspar.Optimize where



import Control.Monad.Reader
import Control.Monad.Writer hiding (Any (..))
import Data.Maybe
import qualified Data.Monoid as Monoid
import Data.Set (Set)
import qualified Data.Set as Set

import Data.Constraint (Dict (..))

import Language.Syntactic
import Language.Syntactic.Functional
import Language.Syntactic.Functional.Tuple
import Language.Syntactic.Functional.Sharing

import Data.Selection
import Data.TypedStruct
import Feldspar.Primitive.Representation
import Feldspar.Representation



witInteger :: ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
witInteger :: ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
witInteger ASTF FeldDomain a
a = case ASTF FeldDomain a -> TypeRepFun (DenResult (Full a))
forall (sym :: * -> *) (info :: * -> *) sig.
AST (sym :&: info) sig -> info (DenResult sig)
getDecor ASTF FeldDomain a
a of
    ValT (Single Int8T)   -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Int16T)  -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Int32T)  -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Int64T)  -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Word8T)  -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Word16T) -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Word32T) -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    ValT (Single Word64T) -> Dict (Integral a, Ord a) -> Maybe (Dict (Integral a, Ord a))
forall a. a -> Maybe a
Just Dict (Integral a, Ord a)
forall (a :: Constraint). a => Dict a
Dict
    TypeRepFun (DenResult (Full a))
_ -> Maybe (Dict (Integral a, Ord a))
forall a. Maybe a
Nothing

isExact :: ASTF FeldDomain a -> Bool
isExact :: ASTF FeldDomain a -> Bool
isExact = Maybe (Dict (Integral a, Ord a)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Dict (Integral a, Ord a)) -> Bool)
-> (ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a)))
-> ASTF FeldDomain a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
forall a. ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
witInteger

-- | 'prj' with a stronger constraint to allow using it in bidirectional
-- patterns
prj' :: (sub :<: sup) => sup sig -> Maybe (sub sig)
prj' :: sup sig -> Maybe (sub sig)
prj' = sup sig -> Maybe (sub sig)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj
  -- I think this function wouldn't be needed if one could add an appropriate
  -- type signature for such patterns, but I wan't able to do this for `SymP`
  -- (the inferred type is not accepted).

pattern $bSymP :: TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
$mSymP :: forall r (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
AST (sup :&: TypeRepFun) sig
-> (TypeRep (DenResult sig) -> sub sig -> r) -> (Void# -> r) -> r
SymP t s <- Sym ((prj' -> Just s) :&: ValT t)
  where
    SymP TypeRep (DenResult sig)
t sub sig
s = (:&:) sup TypeRepFun sig -> AST (sup :&: TypeRepFun) sig
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym ((sub sig -> sup sig
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj sub sig
s) sup sig -> TypeRepFun (DenResult sig) -> (:&:) sup TypeRepFun sig
forall (expr :: * -> *) sig (info :: * -> *).
expr sig -> info (DenResult sig) -> (:&:) expr info sig
:&: TypeRep (DenResult sig) -> TypeRepFun (DenResult sig)
forall a. TypeRep a -> TypeRepFun a
ValT TypeRep (DenResult sig)
t)

pattern $bVarP :: info (DenResult sig) -> Name -> AST (sup :&: info) sig
$mVarP :: forall r (sup :: * -> *) (info :: * -> *) sig.
(BindingT :<: sup) =>
AST (sup :&: info) sig
-> (forall a.
    (sig ~ Full a, Typeable a) =>
    info (DenResult sig) -> Name -> r)
-> (Void# -> r)
-> r
VarP t v <- Sym ((prj' -> Just (VarT v)) :&: t)
  where
    VarP info (DenResult sig)
t Name
v = (:&:) sup info (Full a) -> AST (sup :&: info) (Full a)
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (BindingT (Full a) -> sup (Full a)
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Name -> BindingT (Full a)
forall a. Typeable a => Name -> BindingT (Full a)
VarT Name
v) sup (Full a)
-> info (DenResult (Full a)) -> (:&:) sup info (Full a)
forall (expr :: * -> *) sig (info :: * -> *).
expr sig -> info (DenResult sig) -> (:&:) expr info sig
:&: info (DenResult sig)
info (DenResult (Full a))
t)

pattern $bLamP :: info (DenResult (a1 :-> sig))
-> Name -> AST (sup :&: info) (Full a1) -> AST (sup :&: info) sig
$mLamP :: forall r (sup :: * -> *) (info :: * -> *) sig.
(BindingT :<: sup) =>
AST (sup :&: info) sig
-> (forall a1 a2 b.
    ((a1 :-> sig) ~ (b :-> Full (a2 -> b)), Typeable a2) =>
    info (DenResult (a1 :-> sig))
    -> Name -> AST (sup :&: info) (Full a1) -> r)
-> (Void# -> r)
-> r
LamP t v body <- Sym ((prj' -> Just (LamT v)) :&: t) :$ body
  where
    LamP info (DenResult (a1 :-> sig))
t Name
v AST (sup :&: info) (Full a1)
body = (:&:) sup info (a1 :-> Full (a2 -> a1))
-> AST (sup :&: info) (a1 :-> Full (a2 -> a1))
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (BindingT (a1 :-> Full (a2 -> a1)) -> sup (a1 :-> Full (a2 -> a1))
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Name -> BindingT (a1 :-> Full (a2 -> a1))
forall a b. Typeable a => Name -> BindingT (b :-> Full (a -> b))
LamT Name
v) sup (a1 :-> Full (a2 -> a1))
-> info (DenResult (a1 :-> Full (a2 -> a1)))
-> (:&:) sup info (a1 :-> Full (a2 -> a1))
forall (expr :: * -> *) sig (info :: * -> *).
expr sig -> info (DenResult sig) -> (:&:) expr info sig
:&: info (DenResult (a1 :-> sig))
info (DenResult (a1 :-> Full (a2 -> a1)))
t) AST (sup :&: info) (a1 :-> Full (a2 -> a1))
-> AST (sup :&: info) (Full a1)
-> AST (sup :&: info) (Full (a2 -> a1))
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST (sup :&: info) (Full a1)
body

-- There type signatures are needed in order to use `simplifyUp` in the
-- constructor
#if __GLASGOW_HASKELL__ >= 800
pattern LitP         :: () => (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
pattern AddP         :: () => (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern SubP         :: () => (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern MulP         :: () => (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern NegP         :: () => (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern QuotP        :: () => (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern RemP         :: () => (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern DivP         :: () => (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern ModP         :: () => (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern DivBalancedP :: () => (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
#else
pattern LitP         :: (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
pattern AddP         :: (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern SubP         :: (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern MulP         :: (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern NegP         :: (Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern QuotP        :: (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern RemP         :: (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern DivP         :: (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern ModP         :: (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
pattern DivBalancedP :: (Integral a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
#endif

viewLit :: ASTF FeldDomain a -> Maybe a
viewLit :: ASTF FeldDomain a -> Maybe a
viewLit ASTF FeldDomain a
lit
    | Just (Lit a
a) <- ASTF FeldDomain a -> Maybe (Primitive (Full a))
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj ASTF FeldDomain a
lit = a -> Maybe a
forall a. a -> Maybe a
Just a
a
viewLit ASTF FeldDomain a
_ = Maybe a
forall a. Maybe a
Nothing

pattern $bLitP :: TypeRep a -> a -> ASTF FeldDomain a
$mLitP :: forall r a.
ASTF FeldDomain a
-> ((Eq a, Show a) => TypeRep a -> a -> r) -> (Void# -> r) -> r
LitP t a <- Sym ((prj -> Just (Lit a)) :&: ValT t)
  where
    LitP TypeRep a
t a
a = (:&:) FeldConstructs TypeRepFun (Full a) -> ASTF FeldDomain a
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (Primitive (Full a) -> FeldConstructs (Full a)
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (a -> Primitive (Full a)
forall a. (Eq a, Show a) => a -> Primitive (Full a)
Lit a
a) FeldConstructs (Full a)
-> TypeRepFun (DenResult (Full a))
-> (:&:) FeldConstructs TypeRepFun (Full a)
forall (expr :: * -> *) sig (info :: * -> *).
expr sig -> info (DenResult sig) -> (:&:) expr info sig
:&: TypeRep a -> TypeRepFun a
forall a. TypeRep a -> TypeRepFun a
ValT TypeRep a
t)

pattern $mNonLitP :: forall r a. ASTF FeldDomain a -> (Void# -> r) -> (Void# -> r) -> r
NonLitP <- (viewLit -> Nothing)

pattern $bAddP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mAddP :: forall r a.
ASTF FeldDomain a
-> ((Num a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
AddP t a b <- SymP t Add :$ a :$ b where AddP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a. (Num a, PrimType' a) => Primitive (a :-> (a :-> Full a))
Add AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bSubP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mSubP :: forall r a.
ASTF FeldDomain a
-> ((Num a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
SubP t a b <- SymP t Sub :$ a :$ b where SubP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a. (Num a, PrimType' a) => Primitive (a :-> (a :-> Full a))
Sub AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bMulP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mMulP :: forall r a.
ASTF FeldDomain a
-> ((Num a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
MulP t a b <- SymP t Mul :$ a :$ b where MulP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a. (Num a, PrimType' a) => Primitive (a :-> (a :-> Full a))
Mul AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bNegP :: TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mNegP :: forall r a.
ASTF FeldDomain a
-> ((Num a, PrimType' a) => TypeRep a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
NegP t a   <- SymP t Neg :$ a      where NegP TypeRep a
t ASTF FeldDomain a
a   = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a. (Num a, PrimType' a) => Primitive (a :-> Full a)
Neg AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a

pattern $bQuotP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mQuotP :: forall r a.
ASTF FeldDomain a
-> ((Integral a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
QuotP t a b         <- SymP t Quot        :$ a :$ b where QuotP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b        = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Quot        AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bRemP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mRemP :: forall r a.
ASTF FeldDomain a
-> ((Integral a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
RemP t a b          <- SymP t Rem         :$ a :$ b where RemP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b         = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Rem         AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bDivP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mDivP :: forall r a.
ASTF FeldDomain a
-> ((Integral a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
DivP t a b          <- SymP t Div         :$ a :$ b where DivP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b         = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Div         AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bModP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mModP :: forall r a.
ASTF FeldDomain a
-> ((Integral a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
ModP t a b          <- SymP t Mod         :$ a :$ b where ModP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b         = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> Primitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Mod         AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b
pattern $bDivBalancedP :: TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
$mDivBalancedP :: forall r a.
ASTF FeldDomain a
-> ((Integral a, PrimType' a) =>
    TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a -> r)
-> (Void# -> r)
-> r
DivBalancedP t a b  <- SymP t DivBalanced :$ a :$ b where DivBalancedP TypeRep a
t ASTF FeldDomain a
a ASTF FeldDomain a
b = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full a)))
-> ExtraPrimitive (a :-> (a :-> Full a))
-> AST FeldDomain (a :-> (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep a
TypeRep (DenResult (a :-> (a :-> Full a)))
t ExtraPrimitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
ExtraPrimitive (a :-> (a :-> Full a))
DivBalanced AST FeldDomain (a :-> (a :-> Full a))
-> ASTF FeldDomain a -> AST FeldDomain (a :-> Full a)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b



simplifyUp
    :: ASTF FeldDomain a
    -> ASTF FeldDomain a
simplifyUp :: ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (AddP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
b = ASTF FeldDomain a
b
simplifyUp (AddP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
0)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = ASTF FeldDomain a
a
simplifyUp (AddP TypeRep a
t a :: ASTF FeldDomain a
a@(LitP TypeRep a
_ a
_) b :: ASTF FeldDomain a
b@ASTF FeldDomain a
NonLitP) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
t ASTF FeldDomain a
b ASTF FeldDomain a
a
  -- Move literals to the right
simplifyUp (AddP TypeRep a
t (AddP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) (LitP TypeRep a
_ a
c)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a
ba -> a -> a
forall a. Num a => a -> a -> a
+a
c))
simplifyUp (AddP TypeRep a
t (SubP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) (LitP TypeRep a
_ a
c)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a
ca -> a -> a
forall a. Num a => a -> a -> a
-a
b))
simplifyUp (AddP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) | Just Dict (Integral a, Ord a)
Dict <- ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
forall a. ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
witInteger ASTF FeldDomain a
a, a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
SubP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a -> a
forall a. Num a => a -> a
negate a
b))

simplifyUp (SubP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
b = TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
NegP TypeRep a
t ASTF FeldDomain a
b
simplifyUp (SubP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
0)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = ASTF FeldDomain a
a
simplifyUp (SubP TypeRep a
t a :: ASTF FeldDomain a
a@(LitP TypeRep a
_ a
_) b :: ASTF FeldDomain a
b@ASTF FeldDomain a
NonLitP) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
t (TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
NegP TypeRep a
t ASTF FeldDomain a
b) ASTF FeldDomain a
a
  -- Move literals to the right
simplifyUp (SubP TypeRep a
t (AddP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) (LitP TypeRep a
_ a
c)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a
ba -> a -> a
forall a. Num a => a -> a -> a
-a
c))
simplifyUp (SubP TypeRep a
t (SubP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) (LitP TypeRep a
_ a
c)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
SubP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a
ba -> a -> a
forall a. Num a => a -> a -> a
+a
c))
simplifyUp (SubP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) | Just Dict (Integral a, Ord a)
Dict <- ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
forall a. ASTF FeldDomain a -> Maybe (Dict (Integral a, Ord a))
witInteger ASTF FeldDomain a
a, a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a -> a
forall a. Num a => a -> a
negate a
b))

simplifyUp (MulP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
b = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (MulP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
0)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (MulP TypeRep a
t (LitP TypeRep a
_ a
1) ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
b = ASTF FeldDomain a
b
simplifyUp (MulP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
1)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = ASTF FeldDomain a
a
simplifyUp (MulP TypeRep a
t a :: ASTF FeldDomain a
a@(LitP TypeRep a
_ a
_) b :: ASTF FeldDomain a
b@ASTF FeldDomain a
NonLitP) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
MulP TypeRep a
t ASTF FeldDomain a
b ASTF FeldDomain a
a
  -- Move literals to the right
simplifyUp (MulP TypeRep a
t (MulP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
b)) (LitP TypeRep a
_ a
c)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
MulP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a
ba -> a -> a
forall a. Num a => a -> a -> a
*a
c))

simplifyUp (NegP TypeRep a
t (NegP TypeRep a
_ ASTF FeldDomain a
a))   | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = ASTF FeldDomain a
a
simplifyUp (NegP TypeRep a
t (AddP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
SubP TypeRep a
t (TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
NegP TypeRep a
t ASTF FeldDomain a
a) ASTF FeldDomain a
b
simplifyUp (NegP TypeRep a
t (SubP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
SubP TypeRep a
t ASTF FeldDomain a
b ASTF FeldDomain a
a
simplifyUp (NegP TypeRep a
t (MulP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b)) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
a = TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
MulP TypeRep a
t ASTF FeldDomain a
a (TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
NegP TypeRep a
t ASTF FeldDomain a
b)
  -- Negate the right operand, because literals are moved to the right in
  -- multiplications

simplifyUp (QuotP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (QuotP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
1)) = ASTF FeldDomain a
a
simplifyUp (QuotP t :: TypeRep a
t@(Single PrimTypeRep a
_) ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq ASTF FeldDomain a
a ASTF FeldDomain a
b = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
1

simplifyUp (RemP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (RemP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
1)) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (RemP t :: TypeRep a
t@(Single PrimTypeRep a
_) ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq ASTF FeldDomain a
a ASTF FeldDomain a
b = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0

simplifyUp (DivP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (DivP TypeRep a
_ ASTF FeldDomain a
a (LitP TypeRep a
_ a
1)) = ASTF FeldDomain a
a
simplifyUp (DivP t :: TypeRep a
t@(Single PrimTypeRep a
_) ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq ASTF FeldDomain a
a ASTF FeldDomain a
b = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
1

simplifyUp (ModP TypeRep a
t (LitP TypeRep a
_ a
0) ASTF FeldDomain a
b) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (ModP TypeRep a
t ASTF FeldDomain a
a (LitP TypeRep a
_ a
1)) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0
simplifyUp (ModP t :: TypeRep a
t@(Single PrimTypeRep a
_) ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq ASTF FeldDomain a
a ASTF FeldDomain a
b = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
0

simplifyUp (MulP TypeRep a
_ (DivBalancedP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b) ASTF FeldDomain a
c) | ASTF FeldDomain a -> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq ASTF FeldDomain a
b ASTF FeldDomain a
c = ASTF FeldDomain a
a
simplifyUp (MulP TypeRep a
_ ASTF FeldDomain a
a (DivBalancedP TypeRep a
_ ASTF FeldDomain a
b ASTF FeldDomain a
c)) | ASTF FeldDomain a -> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq ASTF FeldDomain a
a ASTF FeldDomain a
c = ASTF FeldDomain a
b
  -- These rewrites are only correct if the assumption of `DivBalanced` is
  -- fulfilled.

simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
_ Primitive (a :-> Full a)
Not :$ (SymP TypeRep (DenResult (a :-> Full a))
_ Primitive (a :-> Full a)
Not :$ AST FeldDomain (Full a)
a)) = ASTF FeldDomain a
AST FeldDomain (Full a)
a
simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
Not :$ (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Lt :$ AST FeldDomain (Full a)
a :$ AST FeldDomain (Full a)
b)) = ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain Bool -> ASTF FeldDomain Bool)
-> ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full Bool)))
-> Primitive (a :-> (a :-> Full Bool))
-> AST FeldDomain (a :-> (a :-> Full Bool))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
TypeRep (DenResult (a :-> (a :-> Full Bool)))
t Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Ge AST FeldDomain (a :-> (a :-> Full Bool))
-> AST FeldDomain (Full a) -> AST FeldDomain (a :-> Full Bool)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
a AST FeldDomain (a :-> Full Bool)
-> AST FeldDomain (Full a) -> ASTF FeldDomain Bool
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
AST FeldDomain (Full a)
b
simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
Not :$ (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Gt :$ AST FeldDomain (Full a)
a :$ AST FeldDomain (Full a)
b)) = ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain Bool -> ASTF FeldDomain Bool)
-> ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full Bool)))
-> Primitive (a :-> (a :-> Full Bool))
-> AST FeldDomain (a :-> (a :-> Full Bool))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
TypeRep (DenResult (a :-> (a :-> Full Bool)))
t Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Le AST FeldDomain (a :-> (a :-> Full Bool))
-> AST FeldDomain (Full a) -> AST FeldDomain (a :-> Full Bool)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
a AST FeldDomain (a :-> Full Bool)
-> AST FeldDomain (Full a) -> ASTF FeldDomain Bool
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
AST FeldDomain (Full a)
b
simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
Not :$ (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Le :$ AST FeldDomain (Full a)
a :$ AST FeldDomain (Full a)
b)) = ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain Bool -> ASTF FeldDomain Bool)
-> ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full Bool)))
-> Primitive (a :-> (a :-> Full Bool))
-> AST FeldDomain (a :-> (a :-> Full Bool))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
TypeRep (DenResult (a :-> (a :-> Full Bool)))
t Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Gt AST FeldDomain (a :-> (a :-> Full Bool))
-> AST FeldDomain (Full a) -> AST FeldDomain (a :-> Full Bool)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
a AST FeldDomain (a :-> Full Bool)
-> AST FeldDomain (Full a) -> ASTF FeldDomain Bool
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
AST FeldDomain (Full a)
b
simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
Not :$ (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Ge :$ AST FeldDomain (Full a)
a :$ AST FeldDomain (Full a)
b)) = ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain Bool -> ASTF FeldDomain Bool)
-> ASTF FeldDomain Bool -> ASTF FeldDomain Bool
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult (a :-> (a :-> Full Bool)))
-> Primitive (a :-> (a :-> Full Bool))
-> AST FeldDomain (a :-> (a :-> Full Bool))
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
TypeRep (DenResult (a :-> (a :-> Full Bool)))
t Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Lt AST FeldDomain (a :-> (a :-> Full Bool))
-> AST FeldDomain (Full a) -> AST FeldDomain (a :-> Full Bool)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
a AST FeldDomain (a :-> Full Bool)
-> AST FeldDomain (Full a) -> ASTF FeldDomain Bool
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST FeldDomain (Full a)
AST FeldDomain (Full a)
b

simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
And :$ LitP TypeRep a
t a
False :$ AST FeldDomain (Full a)
_) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
Bool
False
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
And :$ AST FeldDomain (Full a)
_ :$ LitP TypeRep a
t a
False) = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
Bool
False
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
And :$ LitP TypeRep a
t a
True :$ AST FeldDomain (Full a)
b)  = ASTF FeldDomain a
AST FeldDomain (Full a)
b
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
And :$ AST FeldDomain (Full a)
a :$ LitP TypeRep a
t a
True)  = ASTF FeldDomain a
AST FeldDomain (Full a)
a

simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Or :$ LitP TypeRep a
t a
False :$ AST FeldDomain (Full a)
b) = ASTF FeldDomain a
AST FeldDomain (Full a)
b
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Or :$ AST FeldDomain (Full a)
a :$ LitP TypeRep a
t a
False) = ASTF FeldDomain a
AST FeldDomain (Full a)
a
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Or :$ LitP TypeRep a
t a
True :$ AST FeldDomain (Full a)
_)  = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
Bool
True
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Primitive (a :-> (a :-> Full a))
Or :$ AST FeldDomain (Full a)
_ :$ LitP TypeRep a
t a
True)  = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t a
Bool
True

simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> (a :-> Full a))))
_ Primitive (a :-> (a :-> (a :-> Full a)))
Cond :$ LitP TypeRep a
_ a
True  :$ AST FeldDomain (Full a)
t :$ AST FeldDomain (Full a)
_) = ASTF FeldDomain a
AST FeldDomain (Full a)
t
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> (a :-> Full a))))
_ Primitive (a :-> (a :-> (a :-> Full a)))
Cond :$ LitP TypeRep a
_ a
False :$ AST FeldDomain (Full a)
_ :$ AST FeldDomain (Full a)
f) = ASTF FeldDomain a
AST FeldDomain (Full a)
f
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> (a :-> Full a))))
_ Primitive (a :-> (a :-> (a :-> Full a)))
Cond :$ AST FeldDomain (Full a)
c :$ AST FeldDomain (Full a)
t :$ AST FeldDomain (Full a)
f) | AST FeldDomain (Full a) -> AST FeldDomain (Full a) -> Bool
forall (e :: * -> *) a b. Equality e => e a -> e b -> Bool
equal AST FeldDomain (Full a)
t AST FeldDomain (Full a)
f = ASTF FeldDomain a
AST FeldDomain (Full a)
t

simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
_ Primitive (a :-> Full a)
BitCompl :$ (SymP TypeRep (DenResult (a :-> Full a))
_ Primitive (a :-> Full a)
BitCompl :$ AST FeldDomain (Full a)
a)) = ASTF FeldDomain a
AST FeldDomain (Full a)
a

-- simplifyUp (SymP _ ForLoop :$ LitP _ 0 :$ init :$ _) = init
  -- This triggers the bug: <https://ghc.haskell.org/trac/ghc/ticket/11336>. The
  -- line below is a workaround:
simplifyUp (Sym ((FeldConstructs (a :-> (a :-> (a :-> Full a)))
-> Maybe (ForLoop (a :-> (a :-> (a :-> Full a))))
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj -> Just ForLoop (a :-> (a :-> (a :-> Full a)))
ForLoop) :&: TypeRepFun (DenResult (a :-> (a :-> (a :-> Full a))))
_) :$ LitP TypeRep a
_ a
0 :$ AST FeldDomain (Full a)
init :$ AST FeldDomain (Full a)
_) = ASTF FeldDomain a
AST FeldDomain (Full a)
init
simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> (a :-> Full a))))
_ ForLoop (a :-> (a :-> (a :-> Full a)))
ForLoop :$ AST FeldDomain (Full a)
_ :$ AST FeldDomain (Full a)
init :$ LamP TypeRepFun (DenResult (a1 :-> Full a))
_ Name
_ (LamP TypeRepFun (DenResult (a1 :-> Full a1))
_ Name
vs (VarP TypeRepFun (DenResult (Full a1))
_ Name
vs')))
    | Name
vsName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
vs' = ASTF FeldDomain a
AST FeldDomain (Full a)
init

simplifyUp (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
t Tuple (a :-> (a :-> Full a))
Pair :$ (SymP TypeRep (DenResult (a :-> Full a))
_ Tuple (a :-> Full a)
Fst :$ AST FeldDomain (Full a)
a) :$ (SymP TypeRep (DenResult (a :-> Full a))
_ Tuple (a :-> Full a)
Snd :$ AST FeldDomain (Full a)
b))
    | AST FeldDomain (Full a) -> AST FeldDomain (Full a) -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
ASTF sym a -> ASTF sym b -> Bool
alphaEq AST FeldDomain (Full a)
a AST FeldDomain (Full a)
b
    , ValT t' <- AST FeldDomain (Full a) -> TypeRepFun (DenResult (Full a))
forall (sym :: * -> *) (info :: * -> *) sig.
AST (sym :&: info) sig -> info (DenResult sig)
getDecor AST FeldDomain (Full a)
a
    , Just Dict ((a, a) ~ (a, b))
Dict <- TypeRep (a, a) -> TypeRep (a, b) -> Maybe (Dict ((a, a) ~ (a, b)))
forall a b. TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq TypeRep (a, a)
TypeRep (DenResult (a :-> (a :-> Full a)))
t TypeRep (a, b)
t' = ASTF FeldDomain a
AST FeldDomain (Full a)
a
simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
t Tuple (a :-> Full a)
Fst :$ (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Tuple (a :-> (a :-> Full a))
Pair :$ AST FeldDomain (Full a)
a :$ AST FeldDomain (Full a)
_)) = ASTF FeldDomain a
AST FeldDomain (Full a)
a
simplifyUp (SymP TypeRep (DenResult (a :-> Full a))
t Tuple (a :-> Full a)
Snd :$ (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ Tuple (a :-> (a :-> Full a))
Pair :$ AST FeldDomain (Full a)
_ :$ AST FeldDomain (Full a)
a)) = ASTF FeldDomain a
AST FeldDomain (Full a)
a
  -- The cases for pairs don't affect the generated code, but they improve the
  -- output of functions like `drawAST`

simplifyUp ASTF FeldDomain a
a = ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
constFold ASTF FeldDomain a
a
  -- `constFold` here ensures that `simplifyUp` does not produce any expressions
  -- that can be statically constant folded. This property is needed, e.g. to
  -- fully simplify the expression `negate (2*x)`. The simplification should go
  -- as follows:
  --
  --     negate (2*x)  ->  negate (x*2)  ->  x * negate 2  ->  x*(-2)
  --
  -- There is no explicit rule for the last step; it is done by `constFold`.
  -- Furthermore, this constant folding would not be performed by `simplifyM`
  -- since it never sees the sub-expression `negate 2`. (Note that the constant
  -- folding in `simplifyM` is still needed, because constructs such as
  -- `ForLoop` cannot be folded by simple literal propagation.)
  --
  -- In order to see that `simplifyUp` doesn't produce any "junk"
  -- (sub-expressions that can be folded by `constFold`), we reason as follows:
  --
  --   * Assume that the arguments of the top-level node are junk-free
  --   * `simplifyUp` will either apply an explicit rewrite or apply `constFold`
  --   * In the latter case, the result will be junk-free
  --   * In case of an explicit rewrite, the resulting expression is constructed
  --     by applying `simplifyUp` to each newly introduced node; thus the
  --     resulting expression must be junk-free



-- | Reduce an expression to a literal if the following conditions are met:
--
-- * The top-most symbol can be evaluated statically (i.g. not a variable or a
--   lifted side-effecting program)
-- * All immediate sub-terms are literals
-- * The type of the expression is an allowed type for literals (e.g. not a
--   function)
--
-- Note that this function only folds the top-level node of an expressions (if
-- possible). It does not reduce an expression like @1+(2+3)@ where the
-- sub-expression @2+3@ is not a literal.
constFold :: ASTF FeldDomain a -> ASTF FeldDomain a
constFold :: ASTF FeldDomain a -> ASTF FeldDomain a
constFold ASTF FeldDomain a
e
    | ASTF FeldDomain a -> Bool
forall sig. AST FeldDomain sig -> Bool
constArgs ASTF FeldDomain a
e
    , ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
canFold ASTF FeldDomain a
e
    , ValT t@(Single _) <- ASTF FeldDomain a -> TypeRepFun (DenResult (Full a))
forall (sym :: * -> *) (info :: * -> *) sig.
AST (sym :&: info) sig -> info (DenResult sig)
getDecor ASTF FeldDomain a
e
    = TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t (a -> ASTF FeldDomain a) -> a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ ASTF FeldDomain a -> a
forall (sym :: * -> *) a. EvalEnv sym RunEnv => ASTF sym a -> a
evalClosed ASTF FeldDomain a
e
  where
    canFold :: ASTF FeldDomain a -> Bool
    canFold :: ASTF FeldDomain a -> Bool
canFold ASTF FeldDomain a
e = (forall sig.
 (a ~ DenResult sig) =>
 FeldDomain sig -> Args (AST FeldDomain) sig -> Bool)
-> ASTF FeldDomain a -> Bool
forall (sym :: * -> *) a b.
(forall sig.
 (a ~ DenResult sig) =>
 sym sig -> Args (AST sym) sig -> b)
-> ASTF sym a -> b
simpleMatch
      (\FeldDomain sig
s Args (AST FeldDomain) sig
_ -> case () of
          ()
_ | SymP TypeRep (DenResult (Full a))
_ (FreeVar String
_) <- ASTF FeldDomain a
e -> Bool
False
          ()
_ | SymP TypeRep (DenResult (a :-> Full a))
_ (ArrIx IArr Index a
_) :$ AST FeldDomain (Full a)
_ <- ASTF FeldDomain a
e -> Bool
False
                -- Don't fold array indexing
          ()
_ | SymP TypeRep (DenResult (Full a))
_ Primitive (Full a)
Pi            <- ASTF FeldDomain a
e -> Bool
False
          ()
_ | MulP TypeRep a
_ ASTF FeldDomain a
_ (SymP TypeRep (DenResult (Full a))
_ Primitive (Full a)
Pi) <- ASTF FeldDomain a
e -> Bool
False
                -- Don't fold expressions like `2*pi`
          ()
_ | Just (BindingT sig
_ :: BindingT sig) <- FeldDomain sig -> Maybe (BindingT sig)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj FeldDomain sig
s -> Bool
False
          ()
_ | Just (Unsafe sig
_ :: Unsafe sig)   <- FeldDomain sig -> Maybe (Unsafe sig)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj FeldDomain sig
s -> Bool
False
          ()
_ -> Bool
True
      )
      ASTF FeldDomain a
e
constFold ASTF FeldDomain a
e = ASTF FeldDomain a
e

-- | Check whether all arguments of a symbol are literals
constArgs :: AST FeldDomain sig -> Bool
constArgs :: AST FeldDomain sig -> Bool
constArgs (Sym FeldDomain sig
_)         = Bool
True
constArgs (AST FeldDomain (a :-> sig)
s :$ LitP TypeRep a
_ a
_) = AST FeldDomain (a :-> sig) -> Bool
forall sig. AST FeldDomain sig -> Bool
constArgs AST FeldDomain (a :-> sig)
s
constArgs AST FeldDomain sig
_               = Bool
False



type OptEnv = Selection AssertionLabel

type Opt = ReaderT OptEnv (Writer (Set Name, Monoid.Any))

tellVar :: Name -> Opt ()
tellVar :: Name -> Opt ()
tellVar Name
v = (Set Name, Any) -> Opt ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Name -> Set Name
forall a. a -> Set a
Set.singleton Name
v, Any
forall a. Monoid a => a
mempty)

deleteVar :: Name -> Opt a -> Opt a
deleteVar :: Name -> Opt a -> Opt a
deleteVar Name
v = ((Set Name, Any) -> (Set Name, Any)) -> Opt a -> Opt a
forall w (m :: * -> *) a. MonadWriter w m => (w -> w) -> m a -> m a
censor (\(Set Name
vs,Any
unsafe) -> (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete Name
v Set Name
vs, Any
unsafe))

tellUnsafe :: Opt ()
tellUnsafe :: Opt ()
tellUnsafe = (Set Name, Any) -> Opt ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Set Name
forall a. Monoid a => a
mempty, Bool -> Any
Monoid.Any Bool
True)

simplifyM :: ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM :: ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM ASTF FeldDomain a
a = do
    Selection AssertionLabel
cs <- ReaderT
  (Selection AssertionLabel)
  (Writer (Set Name, Any))
  (Selection AssertionLabel)
forall r (m :: * -> *). MonadReader r m => m r
ask
    case ASTF FeldDomain a
a of
      a :: ASTF FeldDomain a
a@(VarP TypeRepFun (DenResult (Full a))
_ Name
v)    -> Name -> Opt ()
tellVar Name
v Opt () -> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a
      (LamP TypeRepFun (DenResult (a1 :-> Full a))
t Name
v AST FeldDomain (Full a1)
body) -> Name -> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall a. Name -> Opt a -> Opt a
deleteVar Name
v (Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a))
-> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall a b. (a -> b) -> a -> b
$ (AST FeldDomain (Full a1) -> ASTF FeldDomain a)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (AST FeldDomain (Full a1))
-> Opt (ASTF FeldDomain a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeRepFun (DenResult (a1 :-> Full a))
-> Name -> AST FeldDomain (Full a1) -> ASTF FeldDomain a
forall (sup :: * -> *) (info :: * -> *) sig a1 a2 b.
(BindingT :<: sup, (a1 :-> sig) ~ (b :-> Full (a2 -> b)),
 Typeable a2) =>
info (DenResult (a1 :-> sig))
-> Name -> AST (sup :&: info) (Full a1) -> AST (sup :&: info) sig
LamP TypeRepFun (DenResult (a1 :-> Full a))
t Name
v) (ReaderT
   (Selection AssertionLabel)
   (Writer (Set Name, Any))
   (AST FeldDomain (Full a1))
 -> Opt (ASTF FeldDomain a))
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (AST FeldDomain (Full a1))
-> Opt (ASTF FeldDomain a)
forall a b. (a -> b) -> a -> b
$ AST FeldDomain (Full a1)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (AST FeldDomain (Full a1))
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM AST FeldDomain (Full a1)
body
      res :: ASTF FeldDomain a
res@(SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
I2N :$ AddP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
res -> TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
AddP TypeRep a
TypeRep (DenResult (a :-> Full a))
t (ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (ASTF FeldDomain a -> ASTF FeldDomain a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a) ReaderT
  (Selection AssertionLabel)
  (Writer (Set Name, Any))
  (ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b)
      res :: ASTF FeldDomain a
res@(SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
I2N :$ SubP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
res -> TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
SubP TypeRep a
TypeRep (DenResult (a :-> Full a))
t (ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (ASTF FeldDomain a -> ASTF FeldDomain a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a) ReaderT
  (Selection AssertionLabel)
  (Writer (Set Name, Any))
  (ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b)
      res :: ASTF FeldDomain a
res@(SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
I2N :$ MulP TypeRep a
_ ASTF FeldDomain a
a ASTF FeldDomain a
b) | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
res -> TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a
-> ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a
MulP TypeRep a
TypeRep (DenResult (a :-> Full a))
t (ASTF FeldDomain a -> ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (ASTF FeldDomain a -> ASTF FeldDomain a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a) ReaderT
  (Selection AssertionLabel)
  (Writer (Set Name, Any))
  (ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
b)
      res :: ASTF FeldDomain a
res@(SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
I2N :$ NegP TypeRep a
_ ASTF FeldDomain a
a)   | ASTF FeldDomain a -> Bool
forall a. ASTF FeldDomain a -> Bool
isExact ASTF FeldDomain a
res -> TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
(Num a, PrimType' a) =>
TypeRep a -> ASTF FeldDomain a -> ASTF FeldDomain a
NegP TypeRep a
TypeRep (DenResult (a :-> Full a))
t (ASTF FeldDomain a -> ASTF FeldDomain a)
-> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM (TypeRep (DenResult (a :-> Full a))
-> Primitive (a :-> Full a) -> AST FeldDomain (a :-> Full a)
forall (sub :: * -> *) (sup :: * -> *) sig.
(sub :<: sup) =>
TypeRep (DenResult sig) -> sub sig -> AST (sup :&: TypeRepFun) sig
SymP TypeRep (DenResult (a :-> Full a))
t Primitive (a :-> Full a)
forall a b.
(Integral a, Num b, PrimType' a, PrimType' b) =>
Primitive (a :-> Full b)
I2N AST FeldDomain (a :-> Full a)
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF FeldDomain a
a)
        -- Pushing down `I2N` is not good for in-exact types, since that puts
        -- more of the expression under the in-exact type. This means that fewer
        -- simplifications may apply. Also, operations on in-exact types are
        -- typically more expensive.
        --
        -- Here it's important to guard on whether the *result* is an exact
        -- type. (For other numeric operations it doesn't matter which
        -- sub-expression we check because they all have the same type.)
      (SymP TypeRep (DenResult (a :-> (a :-> Full a)))
_ (GuardVal AssertionLabel
c String
_) :$ AST FeldDomain (Full a)
_ :$ AST FeldDomain (Full a)
a) | Bool -> Bool
not (Selection AssertionLabel
cs Selection AssertionLabel -> AssertionLabel -> Bool
forall a. Selection a -> a -> Bool
`includes` AssertionLabel
c) -> AST FeldDomain (Full a) -> Opt (AST FeldDomain (Full a))
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM AST FeldDomain (Full a)
a
      ASTF FeldDomain a
_ -> (forall sig.
 (a ~ DenResult sig) =>
 FeldDomain sig
 -> Args (AST FeldDomain) sig -> Opt (ASTF FeldDomain a))
-> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (sym :: * -> *) a b.
(forall sig.
 (a ~ DenResult sig) =>
 sym sig -> Args (AST sym) sig -> b)
-> ASTF sym a -> b
simpleMatch
        ( \s :: FeldDomain sig
s@(_ :&: t) Args (AST FeldDomain) sig
as -> do
            (ASTF FeldDomain a
a',(Set Name
vs, Monoid.Any Bool
unsafe)) <- Opt (ASTF FeldDomain a)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (ASTF FeldDomain a, (Set Name, Any))
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (ASTF FeldDomain a -> ASTF FeldDomain a
forall a. ASTF FeldDomain a -> ASTF FeldDomain a
simplifyUp (ASTF FeldDomain a -> ASTF FeldDomain a)
-> (Args (AST FeldDomain) sig -> ASTF FeldDomain a)
-> Args (AST FeldDomain) sig
-> ASTF FeldDomain a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST FeldDomain sig
-> Args (AST FeldDomain) sig -> ASTF FeldDomain (DenResult sig)
forall (sym :: * -> *) sig.
AST sym sig -> Args (AST sym) sig -> ASTF sym (DenResult sig)
appArgs (FeldDomain sig -> AST FeldDomain sig
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym FeldDomain sig
s) (Args (AST FeldDomain) sig -> ASTF FeldDomain a)
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (Args (AST FeldDomain) sig)
-> Opt (ASTF FeldDomain a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a))
-> Args (AST FeldDomain) sig
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (Args (AST FeldDomain) sig)
forall (m :: * -> *) (c1 :: * -> *) (c2 :: * -> *).
Monad m =>
(forall a. c1 (Full a) -> m (c2 (Full a)))
-> forall sig. Args c1 sig -> m (Args c2 sig)
mapArgsM forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM Args (AST FeldDomain) sig
as)
            case () of
                ()
_ | SymP TypeRep (DenResult (Full a))
_ (FreeVar String
_) <- ASTF FeldDomain a
a' -> Opt ()
tellUnsafe Opt () -> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a'
                ()
_ | SymP TypeRep (DenResult (a :-> Full a))
_ (ArrIx IArr Index a
_) :$ AST FeldDomain (Full a)
_ <- ASTF FeldDomain a
a' -> Opt ()
tellUnsafe Opt () -> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a'
                      -- Array indexing is actually not unsafe. It's more like
                      -- an expression with a free variable. But setting the
                      -- unsafe flag does the trick.

                ()
_ | SymP TypeRep (DenResult (Full a))
_ Primitive (Full a)
Pi <- ASTF FeldDomain a
a' -> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a'
                ()
_ | MulP TypeRep a
_ ASTF FeldDomain a
_ (SymP TypeRep (DenResult (Full a))
_ Primitive (Full a)
Pi) <- ASTF FeldDomain a
a' -> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a'
                      -- Don't fold expressions like `2*pi`

                ()
_ | Just (Unsafe sig
_ :: Unsafe sig) <- FeldDomain sig -> Maybe (Unsafe sig)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj FeldDomain sig
s -> Opt ()
tellUnsafe Opt () -> Opt (ASTF FeldDomain a) -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a'
                ()
_ | Set Name -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Name
vs Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
unsafe
                  , ValT t'@(Single _) <- TypeRepFun (DenResult sig)
t
                    -> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ASTF FeldDomain a -> Opt (ASTF FeldDomain a))
-> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall a b. (a -> b) -> a -> b
$ TypeRep a -> a -> ASTF FeldDomain a
forall a. (Eq a, Show a) => TypeRep a -> a -> ASTF FeldDomain a
LitP TypeRep a
t' (a -> ASTF FeldDomain a) -> a -> ASTF FeldDomain a
forall a b. (a -> b) -> a -> b
$ ASTF FeldDomain a -> a
forall (sym :: * -> *) a. EvalEnv sym RunEnv => ASTF sym a -> a
evalClosed ASTF FeldDomain a
a'
                      -- Constant fold if expression is closed and does not
                      -- contain unsafe operations.
                ()
_ -> ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
forall (m :: * -> *) a. Monad m => a -> m a
return ASTF FeldDomain a
a'
        )
        ASTF FeldDomain a
a

simplify :: OptEnv -> ASTF FeldDomain a -> ASTF FeldDomain a
simplify :: Selection AssertionLabel -> ASTF FeldDomain a -> ASTF FeldDomain a
simplify Selection AssertionLabel
env = (ASTF FeldDomain a, (Set Name, Any)) -> ASTF FeldDomain a
forall a b. (a, b) -> a
fst ((ASTF FeldDomain a, (Set Name, Any)) -> ASTF FeldDomain a)
-> (ASTF FeldDomain a -> (ASTF FeldDomain a, (Set Name, Any)))
-> ASTF FeldDomain a
-> ASTF FeldDomain a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Writer (Set Name, Any) (ASTF FeldDomain a)
-> (ASTF FeldDomain a, (Set Name, Any))
forall w a. Writer w a -> (a, w)
runWriter (Writer (Set Name, Any) (ASTF FeldDomain a)
 -> (ASTF FeldDomain a, (Set Name, Any)))
-> (ASTF FeldDomain a
    -> Writer (Set Name, Any) (ASTF FeldDomain a))
-> ASTF FeldDomain a
-> (ASTF FeldDomain a, (Set Name, Any))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT
   (Selection AssertionLabel)
   (Writer (Set Name, Any))
   (ASTF FeldDomain a)
 -> Selection AssertionLabel
 -> Writer (Set Name, Any) (ASTF FeldDomain a))
-> Selection AssertionLabel
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (ASTF FeldDomain a)
-> Writer (Set Name, Any) (ASTF FeldDomain a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Selection AssertionLabel)
  (Writer (Set Name, Any))
  (ASTF FeldDomain a)
-> Selection AssertionLabel
-> Writer (Set Name, Any) (ASTF FeldDomain a)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Selection AssertionLabel
env (ReaderT
   (Selection AssertionLabel)
   (Writer (Set Name, Any))
   (ASTF FeldDomain a)
 -> Writer (Set Name, Any) (ASTF FeldDomain a))
-> (ASTF FeldDomain a
    -> ReaderT
         (Selection AssertionLabel)
         (Writer (Set Name, Any))
         (ASTF FeldDomain a))
-> ASTF FeldDomain a
-> Writer (Set Name, Any) (ASTF FeldDomain a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTF FeldDomain a
-> ReaderT
     (Selection AssertionLabel)
     (Writer (Set Name, Any))
     (ASTF FeldDomain a)
forall a. ASTF FeldDomain a -> Opt (ASTF FeldDomain a)
simplifyM

-- | Interface for controlling code motion
cmInterface :: CodeMotionInterface FeldDomain
cmInterface :: CodeMotionInterface FeldDomain
cmInterface = (forall a b. TypeRepFun a -> TypeRepFun b -> Maybe (Dict (a ~ b)))
-> (forall a b.
    TypeRepFun a -> TypeRepFun b -> TypeRepFun (a -> b))
-> (forall a. TypeRepFun a -> Name -> BindingT (Full a))
-> (forall a b.
    TypeRepFun a
    -> TypeRepFun b -> Name -> BindingT (b :-> Full (a -> b)))
-> (forall a b. ASTF FeldDomain a -> ASTF FeldDomain b -> Bool)
-> (forall a. ASTF FeldDomain a -> Bool)
-> CodeMotionInterface FeldDomain
forall (binding :: * -> *) (sym :: * -> *) (symI :: * -> *)
       (info :: * -> *).
(binding :<: sym, Let :<: sym, symI ~ (sym :&: info)) =>
(forall a b. info a -> info b -> Maybe (Dict (a ~ b)))
-> (forall a b. info a -> info b -> info (a -> b))
-> (forall a. info a -> Name -> binding (Full a))
-> (forall a b.
    info a -> info b -> Name -> binding (b :-> Full (a -> b)))
-> (forall a b. ASTF symI a -> ASTF symI b -> Bool)
-> (forall a. ASTF symI a -> Bool)
-> CodeMotionInterface symI
defaultInterfaceDecor
    forall a b. TypeRepFun a -> TypeRepFun b -> Maybe (Dict (a ~ b))
typeEqFun
    (\(ValT t)   -> TypeRep a -> TypeRepFun b -> TypeRepFun (a -> b)
forall a b. TypeRep a -> TypeRepFun b -> TypeRepFun (a -> b)
FunT TypeRep a
t)
    (\(ValT t)   -> case TypeRep a -> Dict (Typeable a)
forall a. TypeRep a -> Dict (Typeable a)
witTypeable TypeRep a
t of Dict (Typeable a)
Dict -> Name -> BindingT (Full a)
forall a. Typeable a => Name -> BindingT (Full a)
VarT)
    (\(ValT t) TypeRepFun b
_ -> case TypeRep a -> Dict (Typeable a)
forall a. TypeRep a -> Dict (Typeable a)
witTypeable TypeRep a
t of Dict (Typeable a)
Dict -> Name -> BindingT (b :-> Full (a -> b))
forall a b. Typeable a => Name -> BindingT (b :-> Full (a -> b))
LamT)
    forall a b. ASTF FeldDomain a -> ASTF FeldDomain b -> Bool
sharable
    (Bool -> ASTF FeldDomain a -> Bool
forall a b. a -> b -> a
const Bool
True)
  where
    sharable :: ASTF FeldDomain a -> ASTF FeldDomain b -> Bool
    sharable :: ASTF FeldDomain a -> ASTF FeldDomain b -> Bool
sharable (Sym FeldDomain (Full a)
_) ASTF FeldDomain b
_      = Bool
False  -- Simple expressions not shared
    sharable (LamP TypeRepFun (DenResult (a1 :-> Full a))
_ Name
_ AST FeldDomain (Full a1)
_) ASTF FeldDomain b
_ = Bool
False
    sharable ASTF FeldDomain a
_ (LamP TypeRepFun (DenResult (a1 :-> Full b))
_ Name
_ AST FeldDomain (Full a1)
_) = Bool
False
      -- Don't place let bindings over lambdas. This ensures that function
      -- arguments of higher-order constructs such as `ForLoop` are always
      -- lambdas.
    sharable (SymP TypeRep (DenResult (a :-> Full a))
_ (Tuple (a :-> Full a)
_ :: Tuple (b :-> Full c)) :$ AST FeldDomain (Full a)
_) ASTF FeldDomain b
_ = Bool
False
      -- Any unary `Tuple` symbol must be a selector (because there are no
      -- 1-tuples).
    sharable (SymP TypeRep (DenResult (a :-> Full a))
_ Primitive (a :-> Full a)
I2N :$ AST FeldDomain (Full a)
_) ASTF FeldDomain b
_ = Bool
False
--     sharable (SymP _ (ArrIx _) :$ _) _ = False
    sharable ASTF FeldDomain a
_ ASTF FeldDomain b
_ = Bool
True

-- | Optimize a Feldspar expression
optimize :: OptEnv -> ASTF FeldDomain a -> ASTF FeldDomain a
optimize :: Selection AssertionLabel -> ASTF FeldDomain a -> ASTF FeldDomain a
optimize Selection AssertionLabel
env = CodeMotionInterface FeldDomain
-> ASTF FeldDomain a -> ASTF FeldDomain a
forall (sym :: * -> *) m a.
(Equality sym, BindingDomain sym) =>
CodeMotionInterface sym -> ASTF sym a -> ASTF sym a
codeMotion CodeMotionInterface FeldDomain
cmInterface (ASTF FeldDomain a -> ASTF FeldDomain a)
-> (ASTF FeldDomain a -> ASTF FeldDomain a)
-> ASTF FeldDomain a
-> ASTF FeldDomain a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Selection AssertionLabel -> ASTF FeldDomain a -> ASTF FeldDomain a
forall a.
Selection AssertionLabel -> ASTF FeldDomain a -> ASTF FeldDomain a
simplify Selection AssertionLabel
env