{-# LANGUAGE CPP #-}
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' :: (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
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
#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
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
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
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)
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
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 (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
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 :: 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
()
_ | 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
()
_ | 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
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)
(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'
()
_ | 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'
()
_ | 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'
()
_ -> 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
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
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
sharable (SymP TypeRep (DenResult (a :-> Full a))
_ (Tuple (a :-> Full a)
_ :: Tuple (b :-> Full c)) :$ AST FeldDomain (Full a)
_) ASTF FeldDomain b
_ = Bool
False
sharable (SymP TypeRep (DenResult (a :-> Full a))
_ Primitive (a :-> Full a)
I2N :$ AST FeldDomain (Full a)
_) ASTF FeldDomain b
_ = Bool
False
sharable ASTF FeldDomain a
_ ASTF FeldDomain b
_ = Bool
True
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