-- |
-- Module      : CAS.Dumb.Symbols
-- Copyright   : (c) Justus Sagemüller 2017
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 

{-# 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 
                  => CAS' γ (Infix ) (Encapsulation ) s⁰
                  -> CAS' γ (Infix ) (Encapsulation ) 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
_ l 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 l 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 ::  -- ^ The operator we want to describe
  -> CAS' γ   s⁰ -> CAS' γ   s⁰ -> CAS' γ   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  => 
  -> CAS' γ (Infix ) (Encapsulation ) s⁰
  -> CAS' γ (Infix ) (Encapsulation ) s⁰
symbolFunction :: forall s¹ γ s² s⁰.
Monoid s¹ =>
s¹
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
-> CAS' γ (Infix s²) (Encapsulation s¹) s⁰
symbolFunction 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 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        -- ^ Should the result be parenthesised?
       -> Maybe r     -- ^ Left context
       -> SymbolD σ c -- ^ Central expression/function/infix to render
       -> Maybe r     -- ^ Right context
       -> r           -- ^ Rendering result

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 γ   . (SymbolClass σ, SCConstraint σ c)
                      => CAS' γ   (SymbolD σ c) -> CAS' γ   (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 %$>
-- | Transform the symbols of an expression, in their underlying representation.
--
-- @
-- (map succ%$> 𝑎+𝑝) * 𝑥  ≡  (𝑏+𝑞) * 𝑥
-- @
-- 
--   Note that this can /not/ be used with number literals.
(%$>) ::  σ c c' γ   . (SymbolClass σ, SCConstraint σ c)
         => (c -> c') -> CAS' γ   (SymbolD σ c) -> CAS' γ   (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 g CAS' γ s² s¹ (SymbolD σ c)
q = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function 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 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 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 )
       -- ^ Combinator to use for chaining the new expression to the old ones
     -> ( AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l )
       -- ^ Transformation to apply to the rightmost expression in the previous chain
     -> ( AlgebraExpr' γ σ l -> AlgebraExpr' γ σ l )
       -- ^ Transformation which appends the result.
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
):[(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
)
       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 &~~!, &~~:

-- | Apply a sequence of pattern-transformations and yield the result
--   concatenated to the original via the corresponding chain-operator.
--   Because only the rightmost expression in a chain is processed,
--   this can be iterated, giving a chain of intermediate results.
--
--   If one of the patterns does not match, this manipulator will raise
--   an error.
(&~~!) :: ( 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
):[(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
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₀ [(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'


-- | Apply a sequence of pattern-transformations, each in every spot possible,
--   and yield the result
--   concatenated to the original via the corresponding chain-operator.
--   Because only the rightmost expression in a chain is processed,
--   this can be iterated, giving a chain of intermediate results.
(&~~:) :: ( 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
):[(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
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₀ [(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'