{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnicodeSyntax #-}
module CAS.Dumb.Symbols where
import CAS.Dumb.Tree
import Data.Monoid
import qualified Language.Haskell.TH.Syntax as Hs
import Control.Arrow
import Data.String (IsString)
import GHC.Exts (Constraint)
import GHC.Stack (HasCallStack)
import Data.Ratio (denominator, numerator)
import Numeric.Literals.Decimal
data SymbolD σ c = NatSymbol !Integer
| PrimitiveSymbol Char
| StringSymbol c
data Infix s = Infix {
forall s. Infix s -> Fixity
symbolFixity :: !Hs.Fixity
, forall s. Infix s -> s
infixSymbox :: !s
}
instance Eq s => Eq (Infix s) where
Infix Fixity
_ s
o == :: Infix s -> Infix s -> Bool
== Infix Fixity
_ s
p = s
oforall a. Eq a => a -> a -> Bool
==s
p
type family SpecialEncapsulation s
data Encapsulation s = Encapsulation {
forall s. Encapsulation s -> Bool
needInnerParens, forall s. Encapsulation s -> Bool
haveOuterparens :: !Bool
, forall s. Encapsulation s -> s
leftEncaps, forall s. Encapsulation s -> s
rightEncaps :: !s
}
| SpecialEncapsulation (SpecialEncapsulation s)
instance Eq (Encapsulation String) where
Encapsulation Bool
_ Bool
_ String
l String
r == :: Encapsulation String -> Encapsulation String -> Bool
== Encapsulation Bool
_ Bool
_ String
l' String
r'
= String -> String -> (String, String)
dropParens (forall a. [a] -> [a]
reverse String
l) String
r forall a. Eq a => a -> a -> Bool
== String -> String -> (String, String)
dropParens (forall a. [a] -> [a]
reverse String
l') String
r'
where dropParens :: String -> String -> (String, String)
dropParens (Char
'(':String
lr) (Char
')':String
rr) = String -> String -> (String, String)
dropParens String
lr String
rr
dropParens (Char
' ':String
lr) String
rr = String -> String -> (String, String)
dropParens String
lr String
rr
dropParens String
lr (Char
' ':String
rr) = String -> String -> (String, String)
dropParens String
lr String
rr
dropParens String
lr String
rr = (String
lr,String
rr)
SpecialEncapsulation SpecialEncapsulation String
e == SpecialEncapsulation SpecialEncapsulation String
e' = SpecialEncapsulation String
eforall a. Eq a => a -> a -> Bool
==SpecialEncapsulation String
e'
Encapsulation String
_ == Encapsulation String
_ = Bool
False
type AlgebraExpr σ l = CAS (Infix l) (Encapsulation l) (SymbolD σ l)
type AlgebraExpr' γ σ l = CAS' γ (Infix l) (Encapsulation l) (SymbolD σ l)
type AlgebraPattern σ l = AlgebraExpr' GapId σ l
don'tParenthesise :: Monoid s¹
=> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
don'tParenthesise :: forall s¹ γ s² s⁰.
Monoid s¹ =>
CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
don'tParenthesise (Symbol s⁰
s) = forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol s⁰
s
don'tParenthesise (Gap γ
γ) = forall γ s² s¹ s⁰. γ -> CAS' γ s² s¹ s⁰
Gap γ
γ
don'tParenthesise (Function (Encapsulation Bool
nin Bool
_ s¹
l s¹
r) CAS' γ (Infix s²) (Encapsulation s¹) s⁰
x)
= forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function (forall s. Bool -> Bool -> s -> s -> Encapsulation s
Encapsulation Bool
nin Bool
True s¹
l s¹
r) CAS' γ (Infix s²) (Encapsulation s¹) s⁰
x
don'tParenthesise CAS' γ (Infix s²) (Encapsulation s¹) s⁰
x = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function (forall s. Bool -> Bool -> s -> s -> Encapsulation s
Encapsulation Bool
False Bool
True forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty) CAS' γ (Infix s²) (Encapsulation s¹) s⁰
x
symbolInfix :: s²
-> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
symbolInfix :: forall s² γ s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
symbolInfix = forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator
symbolFunction :: Monoid s¹ => s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction :: forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction s¹
f CAS' γ (Infix s²) (Encapsulation s¹) s⁰
a = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function (forall s. Bool -> Bool -> s -> s -> Encapsulation s
Encapsulation Bool
True Bool
False s¹
f forall a. Monoid a => a
mempty) CAS' γ (Infix s²) (Encapsulation s¹) s⁰
a
data AlgebraicInvEncapsulation
= Negation | Reciprocal
deriving (AlgebraicInvEncapsulation -> AlgebraicInvEncapsulation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AlgebraicInvEncapsulation -> AlgebraicInvEncapsulation -> Bool
$c/= :: AlgebraicInvEncapsulation -> AlgebraicInvEncapsulation -> Bool
== :: AlgebraicInvEncapsulation -> AlgebraicInvEncapsulation -> Bool
$c== :: AlgebraicInvEncapsulation -> AlgebraicInvEncapsulation -> Bool
Eq, Int -> AlgebraicInvEncapsulation -> ShowS
[AlgebraicInvEncapsulation] -> ShowS
AlgebraicInvEncapsulation -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AlgebraicInvEncapsulation] -> ShowS
$cshowList :: [AlgebraicInvEncapsulation] -> ShowS
show :: AlgebraicInvEncapsulation -> String
$cshow :: AlgebraicInvEncapsulation -> String
showsPrec :: Int -> AlgebraicInvEncapsulation -> ShowS
$cshowsPrec :: Int -> AlgebraicInvEncapsulation -> ShowS
Show)
type instance SpecialEncapsulation String = AlgebraicInvEncapsulation
instance ∀ σ γ . (SymbolClass σ, SCConstraint σ String)
=> Num (AlgebraExpr' γ σ String) where
fromInteger :: Integer -> AlgebraExpr' γ σ String
fromInteger Integer
n
| Integer
nforall a. Ord a => a -> a -> Bool
<Integer
0 = forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ -Integer
n
| Bool
otherwise = forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall a b. (a -> b) -> a -> b
$ forall σ c. Integer -> SymbolD σ c
NatSymbol Integer
n
+ :: AlgebraExpr' γ σ String
-> AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
(+) = forall s² γ s¹ s⁰.
(s² -> Bool)
-> s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
chainableInfixL (forall a. Eq a => a -> a -> Bool
==Infix String
plusOp) Infix String
plusOp
where fcs :: Char -> String
fcs = forall σ (p :: * -> *) c.
(SymbolClass σ, Functor p, SCConstraint σ c) =>
p σ -> Char -> c
fromCharSymbol ([]::[σ])
plusOp :: Infix String
plusOp = forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
6 FixityDirection
Hs.InfixL) forall a b. (a -> b) -> a -> b
$ Char -> String
fcs Char
'+'
* :: AlgebraExpr' γ σ String
-> AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
(*) = forall s² γ s¹ s⁰.
(s² -> Bool)
-> s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
chainableInfixL (forall a. Eq a => a -> a -> Bool
==Infix String
mulOp) Infix String
mulOp
where fcs :: Char -> String
fcs = forall σ (p :: * -> *) c.
(SymbolClass σ, Functor p, SCConstraint σ c) =>
p σ -> Char -> c
fromCharSymbol ([]::[σ])
mulOp :: Infix String
mulOp = forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
7 FixityDirection
Hs.InfixL) forall a b. (a -> b) -> a -> b
$ Char -> String
fcs Char
'*'
abs :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
abs = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction String
"abs "
signum :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
signum = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction String
"signum "
negate :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
negate = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function forall a b. (a -> b) -> a -> b
$ forall s. SpecialEncapsulation s -> Encapsulation s
SpecialEncapsulation AlgebraicInvEncapsulation
Negation
instance ∀ σ γ . (SymbolClass σ, SCConstraint σ String)
=> Fractional (AlgebraExpr' γ σ String) where
fromRational :: Rational -> AlgebraExpr' γ σ String
fromRational Rational
n = case forall a. Fractional a => Rational -> a
fromRational Rational
n of
Integer
n:%Integer
d -> forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d
FractionalLit
nSci -> forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol (forall σ c. c -> SymbolD σ c
StringSymbol forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FractionalLit
nSci)
recip :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
recip = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function forall a b. (a -> b) -> a -> b
$ forall s. SpecialEncapsulation s -> Encapsulation s
SpecialEncapsulation AlgebraicInvEncapsulation
Reciprocal
instance ∀ σ γ . (SymbolClass σ, SCConstraint σ String)
=> Floating (AlgebraExpr' γ σ String) where
pi :: AlgebraExpr' γ σ String
pi = forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall a b. (a -> b) -> a -> b
$ forall σ c. c -> SymbolD σ c
StringSymbol String
"pi"
** :: AlgebraExpr' γ σ String
-> AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
(**) = forall s² γ s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
symbolInfix (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
8 FixityDirection
Hs.InfixL) String
"**")
logBase :: AlgebraExpr' γ σ String
-> AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
logBase = forall s² γ s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
symbolInfix (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
10 FixityDirection
Hs.InfixL) String
"`logBase`")
sqrt :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
sqrt = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"sqrt "
exp :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
exp = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"exp "
log :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
log = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"log "
sin :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
sin = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"sin "
cos :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
cos = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"cos "
tan :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
tan = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"tan "
asin :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
asin = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"asin "
acos :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
acos = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"acos "
atan :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
atan = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"atan "
sinh :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
sinh = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"sinh "
cosh :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
cosh = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"cosh "
tanh :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
tanh = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"tanh "
asinh :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
asinh = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"asinh "
acosh :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
acosh = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"acosh "
atanh :: AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
atanh = forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction forall a b. (a -> b) -> a -> b
$ String
"atanh "
class ASCIISymbols c where
fromASCIISymbol :: Char -> c
toASCIISymbols :: c -> String
instance ASCIISymbols String where
fromASCIISymbol :: Char -> String
fromASCIISymbol = forall (f :: * -> *) a. Applicative f => a -> f a
pure
toASCIISymbols :: ShowS
toASCIISymbols = forall a. a -> a
id
class Eq (SpecialEncapsulation c) => RenderableEncapsulations c where
fixateAlgebraEncaps :: (SymbolClass σ, SCConstraint σ c)
=> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
instance RenderableEncapsulations String where
fixateAlgebraEncaps :: forall σ γ.
(SymbolClass σ, SCConstraint σ String) =>
AlgebraExpr' γ σ String -> AlgebraExpr' γ σ String
fixateAlgebraEncaps (OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x
((Infix String
o,Function (SpecialEncapsulation SpecialEncapsulation String
ι) CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z):[(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
ys))
| (Infix (Hs.Fixity Int
6 FixityDirection
Hs.InfixL) String
"+", AlgebraicInvEncapsulation
Negation) <- (Infix String
o,SpecialEncapsulation String
ι)
= case forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps forall a b. (a -> b) -> a -> b
$ forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x [(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
ys of
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x' -> forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
6 FixityDirection
Hs.InfixL) String
"-") CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x' CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z'
| (Infix (Hs.Fixity Int
7 FixityDirection
Hs.InfixL) String
"*", AlgebraicInvEncapsulation
Reciprocal) <- (Infix String
o,SpecialEncapsulation String
ι)
= case forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps forall a b. (a -> b) -> a -> b
$ forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x [(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
ys of
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x' -> forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
7 FixityDirection
Hs.InfixL) String
"/") CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x' CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z'
where z' :: CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z' = forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z
fixateAlgebraEncaps (OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x []) = forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x
fixateAlgebraEncaps (OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x ((o :: Infix String
o@(Infix (Hs.Fixity Int
_ FixityDirection
Hs.InfixL) String
_), CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z):[(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
ys))
= forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator Infix String
o (forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps forall a b. (a -> b) -> a -> b
$ forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x [(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
ys) (forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
z)
fixateAlgebraEncaps (Operator Infix String
o CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x (Function (SpecialEncapsulation SpecialEncapsulation String
ι) CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y))
| (Infix (Hs.Fixity Int
6 FixityDirection
Hs.InfixL) String
"+", AlgebraicInvEncapsulation
Negation) <- (Infix String
o,SpecialEncapsulation String
ι)
= forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
6 FixityDirection
Hs.InfixL) String
"-") CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x' CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y'
| (Infix (Hs.Fixity Int
7 FixityDirection
Hs.InfixL) String
"*", AlgebraicInvEncapsulation
Reciprocal) <- (Infix String
o,SpecialEncapsulation String
ι)
= forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
7 FixityDirection
Hs.InfixL) String
"/") CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x' CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y'
where [CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x',CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y'] = forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncapsforall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x,CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y]
fixateAlgebraEncaps (Function (SpecialEncapsulation AlgebraicInvEncapsulation
SpecialEncapsulation String
Negation) CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e)
= forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
6 FixityDirection
Hs.InfixL) String
"-")
(forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall a b. (a -> b) -> a -> b
$ forall σ c. c -> SymbolD σ c
StringSymbol String
" ") forall a b. (a -> b) -> a -> b
$ forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e
fixateAlgebraEncaps (Function (SpecialEncapsulation AlgebraicInvEncapsulation
SpecialEncapsulation String
Reciprocal) CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e)
= forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator (forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
7 FixityDirection
Hs.InfixL) String
"/")
(forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall a b. (a -> b) -> a -> b
$ forall σ c. Integer -> SymbolD σ c
NatSymbol Integer
1) forall a b. (a -> b) -> a -> b
$ forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e
fixateAlgebraEncaps (Function Encapsulation String
f CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e) = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function Encapsulation String
f forall a b. (a -> b) -> a -> b
$ forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e
fixateAlgebraEncaps (Operator Infix String
o CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y)
= forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator Infix String
o (forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x) (forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
y)
fixateAlgebraEncaps (OperatorChain CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x₀ [(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
oys)
= forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain (forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
x₀) (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall c σ γ.
(RenderableEncapsulations c, SymbolClass σ, SCConstraint σ c) =>
CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
-> CAS' γ (Infix c) (Encapsulation c) (SymbolD σ c)
fixateAlgebraEncaps forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Infix String,
CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String))]
oys)
fixateAlgebraEncaps CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e = CAS' γ (Infix String) (Encapsulation String) (SymbolD σ String)
e
type RenderingCombinator σ c r
= Bool
-> Maybe r
-> SymbolD σ c
-> Maybe r
-> r
data ContextFixity = AtLHS Hs.Fixity
| AtRHS Hs.Fixity
| AtFunctionArgument
deriving (ContextFixity -> ContextFixity -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ContextFixity -> ContextFixity -> Bool
$c/= :: ContextFixity -> ContextFixity -> Bool
== :: ContextFixity -> ContextFixity -> Bool
$c== :: ContextFixity -> ContextFixity -> Bool
Eq)
expressionFixity :: AlgebraExpr σ c -> Maybe Hs.Fixity
expressionFixity :: forall σ c. AlgebraExpr σ c -> Maybe Fixity
expressionFixity (Symbol SymbolD σ c
_) = forall a. Maybe a
Nothing
expressionFixity (Function Encapsulation c
_ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
_) = forall a. Maybe a
Nothing
expressionFixity (Operator (Infix Fixity
fxty c
_) CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
_ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
_) = forall a. a -> Maybe a
Just Fixity
fxty
expressionFixity (OperatorChain CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
_ ((Infix Fixity
fxty c
_,CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
_):[(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
_)) = forall a. a -> Maybe a
Just Fixity
fxty
expressionFixity (OperatorChain CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x₀ []) = forall σ c. AlgebraExpr σ c -> Maybe Fixity
expressionFixity CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x₀
expressionFixity (Gap Void
_) = forall a. Maybe a
Nothing
renderSymbolExpression :: ∀ σ c r . (SymbolClass σ, SCConstraint σ c, HasCallStack)
=> ContextFixity -> RenderingCombinator σ c r
-> AlgebraExpr σ c -> r
renderSymbolExpression :: forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression ContextFixity
_ RenderingCombinator σ c r
ρ (Symbol SymbolD σ c
s) = RenderingCombinator σ c r
ρ Bool
False forall a. Maybe a
Nothing SymbolD σ c
s forall a. Maybe a
Nothing
renderSymbolExpression ContextFixity
ctxt RenderingCombinator σ c r
ρ (Function (Encapsulation Bool
needInnerP Bool
atomical c
l c
r) CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x)
= RenderingCombinator σ c r
ρ (Bool -> Bool
not Bool
atomical Bool -> Bool -> Bool
&& ContextFixity
ctxtforall a. Eq a => a -> a -> Bool
==ContextFixity
AtFunctionArgument) forall a. Maybe a
Nothing (forall σ c. c -> SymbolD σ c
StringSymbol c
l) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
forall a b. (a -> b) -> a -> b
$ RenderingCombinator σ c r
ρ Bool
False (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression
(if Bool
needInnerP then ContextFixity
AtFunctionArgument
else Fixity -> ContextFixity
AtLHS (Int -> FixityDirection -> Fixity
Hs.Fixity (-Int
1) FixityDirection
Hs.InfixN))
RenderingCombinator σ c r
ρ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x)
(forall σ c. c -> SymbolD σ c
StringSymbol c
r) forall a. Maybe a
Nothing
renderSymbolExpression ContextFixity
ctxt RenderingCombinator σ c r
ρ (Operator Infix c
o CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
y)
= forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression ContextFixity
ctxt RenderingCombinator σ c r
ρ forall a b. (a -> b) -> a -> b
$ forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x [(Infix c
o,CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
y)]
renderSymbolExpression ContextFixity
ctxt RenderingCombinator σ c r
ρ (OperatorChain CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x []) = forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression ContextFixity
ctxt RenderingCombinator σ c r
ρ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x
renderSymbolExpression ContextFixity
ctxt RenderingCombinator σ c r
ρ (OperatorChain CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x ys :: [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
ys@((Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))
_:[(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
_)) = Bool
-> CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
-> [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
-> r
go Bool
parens CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
ys
where fxty :: Fixity
fxty = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ( \Fixity
f Fixity
f' -> if Fixity
fforall a. Eq a => a -> a -> Bool
==Fixity
f'
then Fixity
f
else forall a. HasCallStack => String -> a
error String
"All infixes in an OperatorChain must have the same fixity"
) forall a b. (a -> b) -> a -> b
$ forall s. Infix s -> Fixity
symbolFixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
ys
go :: Bool
-> CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
-> [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
-> r
go Bool
parens CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x [(Infix Fixity
_ c
o,CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
y)]
= RenderingCombinator σ c r
ρ Bool
parens (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression (Fixity -> ContextFixity
AtLHS Fixity
fxty) RenderingCombinator σ c r
ρ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x)
(forall σ c. c -> SymbolD σ c
StringSymbol c
o)
(forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression (Fixity -> ContextFixity
AtRHS Fixity
fxty) RenderingCombinator σ c r
ρ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
y)
go Bool
parens CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x ((Infix Fixity
_ c
o,CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
y):[(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
zs)
= RenderingCombinator σ c r
ρ Bool
parens (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Bool
-> CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
-> [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
-> r
go Bool
False CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
x [(Infix c, CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c))]
zs)
(forall σ c. c -> SymbolD σ c
StringSymbol c
o)
(forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression (Fixity -> ContextFixity
AtRHS Fixity
fxty) RenderingCombinator σ c r
ρ CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
y)
parens :: Bool
parens = case ContextFixity
ctxt of
ContextFixity
AtFunctionArgument -> Bool
True
AtLHS (Hs.Fixity Int
pfxty FixityDirection
_) | Hs.Fixity Int
lfxty FixityDirection
_ <- Fixity
fxty
, Int
lfxty forall a. Ord a => a -> a -> Bool
< Int
pfxty -> Bool
True
AtLHS (Hs.Fixity Int
pfxty FixityDirection
Hs.InfixL) | Hs.Fixity Int
lfxty FixityDirection
Hs.InfixL <- Fixity
fxty
, Int
lfxtyforall a. Eq a => a -> a -> Bool
==Int
pfxty -> Bool
False
AtLHS (Hs.Fixity Int
pfxty FixityDirection
_) | Hs.Fixity Int
lfxty FixityDirection
_ <- Fixity
fxty
, Int
lfxtyforall a. Eq a => a -> a -> Bool
==Int
pfxty -> Bool
True
AtLHS Fixity
_ -> Bool
False
AtRHS (Hs.Fixity Int
pfxty FixityDirection
_) | Hs.Fixity Int
lfxty FixityDirection
_ <- Fixity
fxty
, Int
lfxty forall a. Ord a => a -> a -> Bool
< Int
pfxty -> Bool
True
AtRHS (Hs.Fixity Int
pfxty FixityDirection
Hs.InfixR) | Hs.Fixity Int
lfxty FixityDirection
Hs.InfixR <- Fixity
fxty
, Int
lfxtyforall a. Eq a => a -> a -> Bool
==Int
pfxty -> Bool
False
AtRHS (Hs.Fixity Int
pfxty FixityDirection
_) | Hs.Fixity Int
lfxty FixityDirection
_ <- Fixity
fxty
, Int
lfxtyforall a. Eq a => a -> a -> Bool
==Int
pfxty -> Bool
True
AtRHS Fixity
_ -> Bool
False
renderSymbolExpression ContextFixity
_ RenderingCombinator σ c r
_ (Function (SpecialEncapsulation SpecialEncapsulation c
_) CAS' Void (Infix c) (Encapsulation c) (SymbolD σ c)
_) = forall a. HasCallStack => String -> a
error
String
"`renderSymbolExpression` cannot handle `SpecialEncapsulation`; please pre-process accordingly."
showsPrecASCIISymbol :: (ASCIISymbols c, SymbolClass σ, SCConstraint σ c)
=> Int -> AlgebraExpr σ c -> ShowS
showsPrecASCIISymbol :: forall c σ.
(ASCIISymbols c, SymbolClass σ, SCConstraint σ c) =>
Int -> AlgebraExpr σ c -> ShowS
showsPrecASCIISymbol Int
ctxt
= forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression (Fixity -> ContextFixity
AtLHS (Int -> FixityDirection -> Fixity
Hs.Fixity Int
ctxt FixityDirection
Hs.InfixN)) forall {c} {σ}.
ASCIISymbols c =>
Bool -> Maybe ShowS -> SymbolD σ c -> Maybe ShowS -> ShowS
ρ
where ρ :: Bool -> Maybe ShowS -> SymbolD σ c -> Maybe ShowS -> ShowS
ρ Bool
dop Maybe ShowS
lctxt (StringSymbol c
sym) Maybe ShowS
rctxt
= Bool -> ShowS -> ShowS
showParen Bool
dop forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
lctxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall c. ASCIISymbols c => c -> String
toASCIISymbols c
symforall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
rctxt
ρ Bool
dop Maybe ShowS
lctxt (NatSymbol Integer
n) Maybe ShowS
rctxt
= Bool -> ShowS -> ShowS
showParen Bool
dop forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
lctxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
rctxt
ρ Bool
dop Maybe ShowS
lctxt (PrimitiveSymbol Char
c) Maybe ShowS
rctxt
= Bool -> ShowS -> ShowS
showParen Bool
dop forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
lctxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
cforall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
rctxt
class UnicodeSymbols c where
fromUnicodeSymbol :: Char -> c
toUnicodeSymbols :: c -> String
instance UnicodeSymbols String where
fromUnicodeSymbol :: Char -> String
fromUnicodeSymbol = forall (f :: * -> *) a. Applicative f => a -> f a
pure
toUnicodeSymbols :: ShowS
toUnicodeSymbols = forall a. a -> a
id
showsPrecUnicodeSymbol :: (UnicodeSymbols c, SymbolClass σ, SCConstraint σ c)
=> Int -> AlgebraExpr σ c -> ShowS
showsPrecUnicodeSymbol :: forall c σ.
(UnicodeSymbols c, SymbolClass σ, SCConstraint σ c) =>
Int -> AlgebraExpr σ c -> ShowS
showsPrecUnicodeSymbol Int
ctxt
= forall σ c r.
(SymbolClass σ, SCConstraint σ c, HasCallStack) =>
ContextFixity -> RenderingCombinator σ c r -> AlgebraExpr σ c -> r
renderSymbolExpression (Fixity -> ContextFixity
AtLHS (Int -> FixityDirection -> Fixity
Hs.Fixity Int
ctxt FixityDirection
Hs.InfixN)) forall {c} {σ}.
UnicodeSymbols c =>
Bool -> Maybe ShowS -> SymbolD σ c -> Maybe ShowS -> ShowS
ρ
where ρ :: Bool -> Maybe ShowS -> SymbolD σ c -> Maybe ShowS -> ShowS
ρ Bool
dop Maybe ShowS
lctxt (StringSymbol c
sym) Maybe ShowS
rctxt
= Bool -> ShowS -> ShowS
showParen Bool
dop forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
lctxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall c. UnicodeSymbols c => c -> String
toUnicodeSymbols c
symforall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
rctxt
ρ Bool
dop Maybe ShowS
lctxt (NatSymbol Integer
n) Maybe ShowS
rctxt
= Bool -> ShowS -> ShowS
showParen Bool
dop forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
lctxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
rctxt
ρ Bool
dop Maybe ShowS
lctxt (PrimitiveSymbol Char
c) Maybe ShowS
rctxt
= Bool -> ShowS -> ShowS
showParen Bool
dop forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
lctxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
cforall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a. a -> a
id Maybe ShowS
rctxt
class SymbolClass σ where
type SCConstraint σ :: * -> Constraint
fromCharSymbol :: (Functor p, SCConstraint σ c) => p σ -> Char -> c
normaliseSymbols :: ∀ σ c γ s² s¹ . (SymbolClass σ, SCConstraint σ c)
=> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c)
normaliseSymbols :: forall σ c γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c)
normaliseSymbols = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SymbolD σ c -> SymbolD σ c
nmlzSym
where nmlzSym :: SymbolD σ c -> SymbolD σ c
nmlzSym (PrimitiveSymbol Char
c) = case forall σ (p :: * -> *) c.
(SymbolClass σ, Functor p, SCConstraint σ c) =>
p σ -> Char -> c
fromCharSymbol ([]::[σ]) of
Char -> c
fcs -> forall σ c. c -> SymbolD σ c
StringSymbol forall a b. (a -> b) -> a -> b
$ Char -> c
fcs Char
c
nmlzSym SymbolD σ c
s = SymbolD σ c
s
instance ∀ σ c . (SymbolClass σ, SCConstraint σ c, Eq c) => Eq (SymbolD σ c) where
NatSymbol Integer
i == :: SymbolD σ c -> SymbolD σ c -> Bool
== NatSymbol Integer
j = Integer
iforall a. Eq a => a -> a -> Bool
==Integer
j
StringSymbol c
x == StringSymbol c
y = c
xforall a. Eq a => a -> a -> Bool
==c
y
PrimitiveSymbol Char
x == PrimitiveSymbol Char
y = Char
xforall a. Eq a => a -> a -> Bool
==Char
y
x :: SymbolD σ c
x@(PrimitiveSymbol Char
c) == SymbolD σ c
y = case forall σ (p :: * -> *) c.
(SymbolClass σ, Functor p, SCConstraint σ c) =>
p σ -> Char -> c
fromCharSymbol ([]::[σ]) of
Char -> c
fcs -> forall σ c. c -> SymbolD σ c
StringSymbol (Char -> c
fcs Char
c)forall a. Eq a => a -> a -> Bool
==SymbolD σ c
y
SymbolD σ c
x == y :: SymbolD σ c
y@(PrimitiveSymbol Char
c) = case forall σ (p :: * -> *) c.
(SymbolClass σ, Functor p, SCConstraint σ c) =>
p σ -> Char -> c
fromCharSymbol ([]::[σ]) of
Char -> c
fcs -> SymbolD σ c
xforall a. Eq a => a -> a -> Bool
==forall σ c. c -> SymbolD σ c
StringSymbol (Char -> c
fcs Char
c)
SymbolD σ c
_ == SymbolD σ c
_ = Bool
False
infixl 4 %$>
(%$>) :: ∀ σ c c' γ s² s¹ . (SymbolClass σ, SCConstraint σ c)
=> (c -> c') -> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
c -> c'
f %$> :: forall σ c c' γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
(c -> c')
-> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
%$> Symbol (PrimitiveSymbol Char
c) = case forall σ (p :: * -> *) c.
(SymbolClass σ, Functor p, SCConstraint σ c) =>
p σ -> Char -> c
fromCharSymbol ([]::[σ]) of
Char -> c
fcs -> forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall σ c. c -> SymbolD σ c
StringSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> c'
f forall a b. (a -> b) -> a -> b
$ Char -> c
fcs Char
c
c -> c'
f %$> Symbol (StringSymbol c
s) = forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall σ c. c -> SymbolD σ c
StringSymbol forall a b. (a -> b) -> a -> b
$ c -> c'
f c
s
c -> c'
_ %$> Symbol (NatSymbol Integer
_) = forall a. HasCallStack => String -> a
error String
"`%$>` cannot be used with number literals."
c -> c'
f %$> Function s¹
g CAS' γ s² s¹ (SymbolD σ c)
q = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function s¹
g forall a b. (a -> b) -> a -> b
$ c -> c'
f forall σ c c' γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
(c -> c')
-> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
%$> CAS' γ s² s¹ (SymbolD σ c)
q
c -> c'
f %$> Operator s²
o CAS' γ s² s¹ (SymbolD σ c)
p CAS' γ s² s¹ (SymbolD σ c)
q = forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator s²
o (c -> c'
fforall σ c c' γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
(c -> c')
-> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
%$>CAS' γ s² s¹ (SymbolD σ c)
p) (c -> c'
fforall σ c c' γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
(c -> c')
-> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
%$>CAS' γ s² s¹ (SymbolD σ c)
q)
c -> c'
f %$> OperatorChain CAS' γ s² s¹ (SymbolD σ c)
p [(s², CAS' γ s² s¹ (SymbolD σ c))]
qs = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain (c -> c'
fforall σ c c' γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
(c -> c')
-> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
%$>CAS' γ s² s¹ (SymbolD σ c)
p) (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (c -> c'
fforall σ c c' γ s² s¹.
(SymbolClass σ, SCConstraint σ c) =>
(c -> c')
-> CAS' γ s² s¹ (SymbolD σ c) -> CAS' γ s² s¹ (SymbolD σ c')
%$>)forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(s², CAS' γ s² s¹ (SymbolD σ c))]
qs)
c -> c'
f %$> Gap γ
γ = forall γ s² s¹ s⁰. γ -> CAS' γ s² s¹ s⁰
Gap γ
γ
continueExpr :: (Eq l, Monoid l)
=> ( AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l )
-> ( AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l )
-> ( AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l )
continueExpr :: forall l γ σ.
(Eq l, Monoid l) =>
(AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l)
-> (AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l)
-> AlgebraExpr' γ σ l
-> AlgebraExpr' γ σ l
continueExpr AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
op AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
f = AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
go
where go :: AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
go (OperatorChain AlgebraExpr' γ σ l
e₀ ((eo :: Infix l
eo@(Infix (Hs.Fixity Int
fte FixityDirection
_) l
_), AlgebraExpr' γ σ l
eΩ):[(Infix l, AlgebraExpr' γ σ l)]
es))
| Int
fte forall a. Ord a => a -> a -> Bool
<= Int
chainingFxty
= forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator Infix l
eo (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain AlgebraExpr' γ σ l
e₀ [(Infix l, AlgebraExpr' γ σ l)]
es) (AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
go AlgebraExpr' γ σ l
eΩ)
go AlgebraExpr' γ σ l
e
| Just (l
co, FixityDirection
fxtyDir) <- Maybe (l, FixityDirection)
chainingOp
= forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain AlgebraExpr' γ σ l
e [(forall s. Fixity -> s -> Infix s
Infix (Int -> FixityDirection -> Fixity
Hs.Fixity Int
chainingFxty FixityDirection
fxtyDir) l
co, AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
f AlgebraExpr' γ σ l
e)]
| Bool
otherwise
= AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
op AlgebraExpr' γ σ l
e forall a b. (a -> b) -> a -> b
$ AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
f AlgebraExpr' γ σ l
e
(Int
chainingFxty, Maybe (l, FixityDirection)
chainingOp)
= case AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l
op (forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall a b. (a -> b) -> a -> b
$ forall σ c. c -> SymbolD σ c
StringSymbol forall a. Monoid a => a
mempty)
(forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol forall a b. (a -> b) -> a -> b
$ forall σ c. c -> SymbolD σ c
StringSymbol forall a. Monoid a => a
mempty) of
OperatorChain AlgebraExpr' γ σ l
_ ((Infix (Hs.Fixity Int
fxty FixityDirection
fxtyDir) l
op, AlgebraExpr' γ σ l
_):[(Infix l, AlgebraExpr' γ σ l)]
_)
-> (Int
fxty, forall a. a -> Maybe a
Just (l
op, FixityDirection
fxtyDir))
AlgebraExpr' γ σ l
_ -> (-Int
1, forall a. Maybe a
Nothing)
infixl 1 &~~!, &~~:
(&~~!) :: ( Eq l, Eq (Encapsulation l), SymbolClass σ, SCConstraint σ l
, Show (AlgebraExpr σ l), Show (AlgebraPattern σ l) )
=> AlgebraExpr σ l -> [AlgebraPattern σ l] -> AlgebraExpr σ l
AlgebraExpr σ l
e &~~! :: forall l σ.
(Eq l, Eq (Encapsulation l), SymbolClass σ, SCConstraint σ l,
Show (AlgebraExpr σ l), Show (AlgebraPattern σ l)) =>
AlgebraExpr σ l -> [AlgebraPattern σ l] -> AlgebraExpr σ l
&~~! [] = AlgebraExpr σ l
e
OperatorChain AlgebraExpr σ l
e₀ ((eo :: Infix l
eo@(Infix (Hs.Fixity Int
fte FixityDirection
_) l
_), AlgebraExpr σ l
eΩ):[(Infix l, AlgebraExpr σ l)]
es)
&~~! tfms :: [AlgebraPattern σ l]
tfms@(OperatorChain AlgebraPattern σ l
p₀ [(to :: Infix l
to@(Infix (Hs.Fixity Int
ftp FixityDirection
_) l
_),AlgebraPattern σ l
p₁)] : [AlgebraPattern σ l]
_)
| Int
fteforall a. Ord a => a -> a -> Bool
<=Int
ftp = forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator Infix l
eo (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain AlgebraExpr σ l
e₀ [(Infix l, AlgebraExpr σ l)]
es) (AlgebraExpr σ l
eΩforall l σ.
(Eq l, Eq (Encapsulation l), SymbolClass σ, SCConstraint σ l,
Show (AlgebraExpr σ l), Show (AlgebraPattern σ l)) =>
AlgebraExpr σ l -> [AlgebraPattern σ l] -> AlgebraExpr σ l
&~~![AlgebraPattern σ l]
tfms)
AlgebraExpr σ l
e &~~! tfms :: [AlgebraPattern σ l]
tfms@(OperatorChain AlgebraPattern σ l
_ [(Infix l
tfmOp, AlgebraPattern σ l
_)] : [AlgebraPattern σ l]
_)
= forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain AlgebraExpr σ l
e [(Infix l
tfmOp, forall {s⁰} {s¹} {s²}.
(Eq s⁰, Eq s¹, Eq s², Show (CAS s² s¹ s⁰),
Show (CAS' Int s² s¹ s⁰)) =>
CAS s² s¹ s⁰ -> [CAS' Int s² s¹ s⁰] -> CAS s² s¹ s⁰
go AlgebraExpr σ l
e [AlgebraPattern σ l]
tfms)]
where go :: CAS s² s¹ s⁰ -> [CAS' Int s² s¹ s⁰] -> CAS s² s¹ s⁰
go CAS s² s¹ s⁰
e' (OperatorChain CAS' Int s² s¹ s⁰
p₀ [(s²
tfmOp', CAS' Int s² s¹ s⁰
p₁)] : [CAS' Int s² s¹ s⁰]
tfms') = CAS s² s¹ s⁰ -> [CAS' Int s² s¹ s⁰] -> CAS s² s¹ s⁰
go (CAS s² s¹ s⁰
e' forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s², Show (CAS s² s¹ s⁰),
Show (CAS' Int s² s¹ s⁰)) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~! (CAS' Int s² s¹ s⁰
p₀forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
p₁)) [CAS' Int s² s¹ s⁰]
tfms'
go CAS s² s¹ s⁰
e' [] = CAS s² s¹ s⁰
e'
(&~~:) :: ( Eq l, Eq (Encapsulation l), SymbolClass σ, SCConstraint σ l
, Show (AlgebraExpr σ l), Show (AlgebraPattern σ l) )
=> AlgebraExpr σ l -> [AlgebraPattern σ l] -> AlgebraExpr σ l
AlgebraExpr σ l
e &~~: :: forall l σ.
(Eq l, Eq (Encapsulation l), SymbolClass σ, SCConstraint σ l,
Show (AlgebraExpr σ l), Show (AlgebraPattern σ l)) =>
AlgebraExpr σ l -> [AlgebraPattern σ l] -> AlgebraExpr σ l
&~~: [] = AlgebraExpr σ l
e
OperatorChain AlgebraExpr σ l
e₀ ((eo :: Infix l
eo@(Infix (Hs.Fixity Int
fte FixityDirection
_) l
_), AlgebraExpr σ l
eΩ):[(Infix l, AlgebraExpr σ l)]
es)
&~~: tfms :: [AlgebraPattern σ l]
tfms@(OperatorChain AlgebraPattern σ l
p₀ [(to :: Infix l
to@(Infix (Hs.Fixity Int
ftp FixityDirection
_) l
_),AlgebraPattern σ l
p₁)] : [AlgebraPattern σ l]
_)
| Int
fteforall a. Ord a => a -> a -> Bool
<=Int
ftp = forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator Infix l
eo (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain AlgebraExpr σ l
e₀ [(Infix l, AlgebraExpr σ l)]
es) (AlgebraExpr σ l
eΩforall l σ.
(Eq l, Eq (Encapsulation l), SymbolClass σ, SCConstraint σ l,
Show (AlgebraExpr σ l), Show (AlgebraPattern σ l)) =>
AlgebraExpr σ l -> [AlgebraPattern σ l] -> AlgebraExpr σ l
&~~:[AlgebraPattern σ l]
tfms)
AlgebraExpr σ l
e &~~: tfms :: [AlgebraPattern σ l]
tfms@(OperatorChain AlgebraPattern σ l
_ [(Infix l
tfmOp, AlgebraPattern σ l
_)] : [AlgebraPattern σ l]
_)
= forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain AlgebraExpr σ l
e [(Infix l
tfmOp, forall {s⁰} {s¹} {s²}.
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> [CAS' Int s² s¹ s⁰] -> CAS s² s¹ s⁰
go AlgebraExpr σ l
e [AlgebraPattern σ l]
tfms)]
where go :: CAS s² s¹ s⁰ -> [CAS' Int s² s¹ s⁰] -> CAS s² s¹ s⁰
go CAS s² s¹ s⁰
e' (OperatorChain CAS' Int s² s¹ s⁰
p₀ [(s²
tfmOp', CAS' Int s² s¹ s⁰
p₁)] : [CAS' Int s² s¹ s⁰]
tfms')
= case CAS s² s¹ s⁰
e' forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~: (CAS' Int s² s¹ s⁰
p₀forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
p₁) of
CAS s² s¹ s⁰
alt -> CAS s² s¹ s⁰ -> [CAS' Int s² s¹ s⁰] -> CAS s² s¹ s⁰
go CAS s² s¹ s⁰
alt [CAS' Int s² s¹ s⁰]
tfms'
go CAS s² s¹ s⁰
e' [] = CAS s² s¹ s⁰
e'