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

{-# LANGUAGE DeriveFunctor, DeriveGeneric       #-}
{-# LANGUAGE TupleSections                      #-}
{-# LANGUAGE PatternSynonyms                    #-}
{-# LANGUAGE FlexibleInstances                  #-}
{-# LANGUAGE FlexibleContexts                   #-}
{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax #-}

module CAS.Dumb.Tree where

import CAS.Dumb.Util.These

import qualified Data.Hashable as SH
import qualified Data.HashMap.Lazy as HMap
import qualified Data.Map as Map
import Data.Map (Map)

import Data.Void
import Control.Monad
import Control.Arrow

import GHC.Generics


data CAS' γ s² s¹ s⁰ = Symbol !s⁰
                     | Function !s¹ (CAS' γ s² s¹ s⁰)
                     | Operator !s² (CAS' γ s² s¹ s⁰) (CAS' γ s² s¹ s⁰)
                     | OperatorChain
                          (CAS' γ s² s¹ s⁰)       -- Initial operand
                          [(s², CAS' γ s² s¹ s⁰)] -- Chain of operator-application, in
                                                  -- reverse order (i.e. the head of this
                                                  -- list contains the rightmost operand)
                     | Gap !γ
  deriving (forall a b. a -> CAS' γ s² s¹ b -> CAS' γ s² s¹ a
forall a b. (a -> b) -> CAS' γ s² s¹ a -> CAS' γ s² s¹ b
forall γ s² s¹ a b. a -> CAS' γ s² s¹ b -> CAS' γ s² s¹ a
forall γ s² s¹ a b. (a -> b) -> CAS' γ s² s¹ a -> CAS' γ s² s¹ b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> CAS' γ s² s¹ b -> CAS' γ s² s¹ a
$c<$ :: forall γ s² s¹ a b. a -> CAS' γ s² s¹ b -> CAS' γ s² s¹ a
fmap :: forall a b. (a -> b) -> CAS' γ s² s¹ a -> CAS' γ s² s¹ b
$cfmap :: forall γ s² s¹ a b. (a -> b) -> CAS' γ s² s¹ a -> CAS' γ s² s¹ b
Functor, CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall γ s² s¹ s⁰.
(Eq s⁰, Eq s¹, Eq s², Eq γ) =>
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Bool
/= :: CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Bool
$c/= :: forall γ s² s¹ s⁰.
(Eq s⁰, Eq s¹, Eq s², Eq γ) =>
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Bool
== :: CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Bool
$c== :: forall γ s² s¹ s⁰.
(Eq s⁰, Eq s¹, Eq s², Eq γ) =>
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall γ s² s¹ s⁰ x. Rep (CAS' γ s² s¹ s⁰) x -> CAS' γ s² s¹ s⁰
forall γ s² s¹ s⁰ x. CAS' γ s² s¹ s⁰ -> Rep (CAS' γ s² s¹ s⁰) x
$cto :: forall γ s² s¹ s⁰ x. Rep (CAS' γ s² s¹ s⁰) x -> CAS' γ s² s¹ s⁰
$cfrom :: forall γ s² s¹ s⁰ x. CAS' γ s² s¹ s⁰ -> Rep (CAS' γ s² s¹ s⁰) x
Generic)



chainableInfixL, chainableInfixR, chainableInfix
               :: (s² -> Bool)  -- ^ Condition that all operators in the chain
                                --   must fulfill to be joined by this one
               -> s²            -- ^ The operator we want to add
               -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
               -> CAS' γ s² s¹ s⁰
chainableInfixL :: forall s² γ s¹ s⁰.
(s² -> Bool)
-> s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
chainableInfixL s² -> Bool
ppred s²
infx (OperatorChain CAS' γ s² s¹ s⁰
x [(s², CAS' γ s² s¹ s⁰)]
ys) CAS' γ s² s¹ s⁰
z
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (s² -> Bool
ppred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(s², CAS' γ s² s¹ s⁰)]
ys  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ (s²
infx,CAS' γ s² s¹ s⁰
z)forall a. a -> [a] -> [a]
:[(s², CAS' γ s² s¹ s⁰)]
ys
chainableInfixL s² -> Bool
_ s²
infx CAS' γ s² s¹ s⁰
a CAS' γ s² s¹ s⁰
b = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
a [(s²
infx,CAS' γ s² s¹ s⁰
b)]

chainableInfixR :: forall s² γ s¹ s⁰.
(s² -> Bool)
-> s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
chainableInfixR s² -> Bool
ppred s²
infx (OperatorChain CAS' γ s² s¹ s⁰
x [(s², CAS' γ s² s¹ s⁰)]
ys) CAS' γ s² s¹ s⁰
z
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (s² -> Bool
ppred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(s², CAS' γ s² s¹ s⁰)]
ys  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ (s²
infx,CAS' γ s² s¹ s⁰
z)forall a. a -> [a] -> [a]
:[(s², CAS' γ s² s¹ s⁰)]
ys
chainableInfixR s² -> Bool
ppred s²
infx CAS' γ s² s¹ s⁰
x (OperatorChain CAS' γ s² s¹ s⁰
y [(s², CAS' γ s² s¹ s⁰)]
zs)
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (s² -> Bool
ppred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(s², CAS' γ s² s¹ s⁰)]
zs  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
zsforall a. [a] -> [a] -> [a]
++[(s²
infx,CAS' γ s² s¹ s⁰
y)]
chainableInfixR s² -> Bool
_ s²
infx CAS' γ s² s¹ s⁰
a CAS' γ s² s¹ s⁰
b = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
a [(s²
infx,CAS' γ s² s¹ s⁰
b)]

chainableInfix :: forall s² γ s¹ s⁰.
(s² -> Bool)
-> s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
chainableInfix s² -> Bool
ppred s²
infx (OperatorChain CAS' γ s² s¹ s⁰
x [(s², CAS' γ s² s¹ s⁰)]
ys) CAS' γ s² s¹ s⁰
z
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (s² -> Bool
ppred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(s², CAS' γ s² s¹ s⁰)]
ys  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ (s²
infx,CAS' γ s² s¹ s⁰
z)forall a. a -> [a] -> [a]
:[(s², CAS' γ s² s¹ s⁰)]
ys
chainableInfix s² -> Bool
ppred s²
infx CAS' γ s² s¹ s⁰
x (OperatorChain CAS' γ s² s¹ s⁰
y [(s², CAS' γ s² s¹ s⁰)]
zs)
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (s² -> Bool
ppred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(s², CAS' γ s² s¹ s⁰)]
zs  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
zsforall a. [a] -> [a] -> [a]
++[(s²
infx,CAS' γ s² s¹ s⁰
y)]
chainableInfix s² -> Bool
_ s²
infx CAS' γ s² s¹ s⁰
a CAS' γ s² s¹ s⁰
b = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
a [(s²
infx,CAS' γ s² s¹ s⁰
b)]

associativeOperator :: Eq s² => s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
                                  -> CAS' γ s² s¹ s⁰
associativeOperator :: forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator s²
o (OperatorChain CAS' γ s² s¹ s⁰
x [(s², CAS' γ s² s¹ s⁰)]
ys) (OperatorChain CAS' γ s² s¹ s⁰
ξ [(s², CAS' γ s² s¹ s⁰)]
υs)
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
==s²
o) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
ys forall a. [a] -> [a] -> [a]
++ [(s², CAS' γ s² s¹ s⁰)]
υs  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
υs forall a. [a] -> [a] -> [a]
++ (s²
o,CAS' γ s² s¹ s⁰
ξ)forall a. a -> [a] -> [a]
:[(s², CAS' γ s² s¹ s⁰)]
ys
associativeOperator s²
o (OperatorChain CAS' γ s² s¹ s⁰
x [(s², CAS' γ s² s¹ s⁰)]
ys) CAS' γ s² s¹ s⁰
z
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
==s²
o) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
ys  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ (s²
o,CAS' γ s² s¹ s⁰
z)forall a. a -> [a] -> [a]
:[(s², CAS' γ s² s¹ s⁰)]
ys
associativeOperator s²
o CAS' γ s² s¹ s⁰
x (OperatorChain CAS' γ s² s¹ s⁰
y [(s², CAS' γ s² s¹ s⁰)]
zs)
 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
==s²
o) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
zs  = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x forall a b. (a -> b) -> a -> b
$ [(s², CAS' γ s² s¹ s⁰)]
zs forall a. [a] -> [a] -> [a]
++ [(s²
o,CAS' γ s² s¹ s⁰
y)]
associativeOperator s²
o CAS' γ s² s¹ s⁰
x CAS' γ s² s¹ s⁰
y = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' γ s² s¹ s⁰
x [(s²
o,CAS' γ s² s¹ s⁰
y)]



type CAS = CAS' Void

instance (SH.Hashable γ, SH.Hashable s⁰, SH.Hashable s¹, SH.Hashable s²)
              => SH.Hashable (CAS' γ s² s¹ s⁰)


infixr 4 :=, :=:
data Equality' γ s² s¹ s⁰
  = (:=) { forall γ s² s¹ s⁰. Equality' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
originalExpression :: !(CAS' γ s² s¹ s⁰)
         , forall γ s² s¹ s⁰. Equality' γ s² s¹ s⁰ -> [Equality' γ s² s¹ s⁰]
transformationOptions :: [Equality' γ s² s¹ s⁰] }
  | (:=:) { originalExpression :: !(CAS' γ s² s¹ s⁰)
          , forall γ s² s¹ s⁰. Equality' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
transformedExpression :: !(CAS' γ s² s¹ s⁰) }
type Equality = Equality' Void

type GapId = Int
type Expattern s² s¹ s⁰ = CAS' GapId s² s¹ s⁰
type Eqspattern s² s¹ s⁰ = Equality' GapId s² s¹ s⁰

matchPattern :: ∀ s⁰ s¹ s² . (Eq s⁰, Eq s¹, Eq s²)
         => Expattern s² s¹ s⁰ -> CAS s² s¹ s⁰ -> Maybe (Map GapId (CAS s² s¹ s⁰))
matchPattern :: forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern (Gap Int
i) CAS s² s¹ s⁰
e = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton Int
i CAS s² s¹ s⁰
e
matchPattern (Symbol s⁰
s) (Symbol s⁰
s')
 | s⁰
sforall a. Eq a => a -> a -> Bool
==s⁰
s'  = forall a. a -> Maybe a
Just forall k a. Map k a
Map.empty
matchPattern (Function s¹
f CAS' Int s² s¹ s⁰
x) (Function s¹
f' CAS s² s¹ s⁰
ξ)
 | s¹
fforall a. Eq a => a -> a -> Bool
==s¹
f'  = forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern CAS' Int s² s¹ s⁰
x CAS s² s¹ s⁰
ξ
matchPattern (Operator s²
o CAS' Int s² s¹ s⁰
x CAS' Int s² s¹ s⁰
y) (Operator s²
o' CAS s² s¹ s⁰
ξ CAS s² s¹ s⁰
υ)
    = forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS' Int s² s¹ s⁰
x [(s²
o,CAS' Int s² s¹ s⁰
y)]) (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS s² s¹ s⁰
ξ [(s²
o',CAS s² s¹ s⁰
υ)])
matchPattern (OperatorChain CAS' Int s² s¹ s⁰
x [(s², CAS' Int s² s¹ s⁰)]
zs) (OperatorChain CAS s² s¹ s⁰
ξ [(s², CAS s² s¹ s⁰)]
ζs)
 | (forall a b. (a, b) -> a
fstforall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(s², CAS' Int s² s¹ s⁰)]
zs) forall a. Eq a => a -> a -> Bool
== (forall a b. (a, b) -> a
fstforall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(s², CAS s² s¹ s⁰)]
ζs)  = do
     Map Int (CAS s² s¹ s⁰)
xmatches <- forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern CAS' Int s² s¹ s⁰
x CAS s² s¹ s⁰
ξ
     [Map Int (CAS s² s¹ s⁰)]
zsmatches <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern (forall a b. (a, b) -> b
sndforall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(s², CAS' Int s² s¹ s⁰)]
zs) (forall a b. (a, b) -> b
sndforall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(s², CAS s² s¹ s⁰)]
ζs)
     Map Int (CAS s² s¹ s⁰)
-> [Map Int (CAS s² s¹ s⁰)] -> Maybe (Map Int (CAS s² s¹ s⁰))
merge Map Int (CAS s² s¹ s⁰)
xmatches [Map Int (CAS s² s¹ s⁰)]
zsmatches
 where merge :: Map GapId (CAS s² s¹ s⁰) -> [Map GapId (CAS s² s¹ s⁰)]
                   -> Maybe (Map GapId (CAS s² s¹ s⁰))
       merge :: Map Int (CAS s² s¹ s⁰)
-> [Map Int (CAS s² s¹ s⁰)] -> Maybe (Map Int (CAS s² s¹ s⁰))
merge Map Int (CAS s² s¹ s⁰)
acc [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Int (CAS s² s¹ s⁰)
acc
       merge Map Int (CAS s² s¹ s⁰)
acc (Map Int (CAS s² s¹ s⁰)
xm:[Map Int (CAS s² s¹ s⁰)]
ms)
          = forall (t :: * -> *) k a.
(Applicative t, Ord k) =>
(a -> a -> t a) -> Map k a -> Map k a -> t (Map k a)
traverseUnionConflicts (\CAS s² s¹ s⁰
v CAS s² s¹ s⁰
w -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (CAS s² s¹ s⁰
vforall a. Eq a => a -> a -> Bool
==CAS s² s¹ s⁰
w) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. a -> Maybe a
Just CAS s² s¹ s⁰
v) Map Int (CAS s² s¹ s⁰)
xm Map Int (CAS s² s¹ s⁰)
acc
             forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Map Int (CAS s² s¹ s⁰)
-> [Map Int (CAS s² s¹ s⁰)] -> Maybe (Map Int (CAS s² s¹ s⁰))
`merge` [Map Int (CAS s² s¹ s⁰)]
ms)
matchPattern CAS' Int s² s¹ s⁰
_ CAS s² s¹ s⁰
_ = forall a. Maybe a
Nothing

infixl 1 &~:, &~?, &~!

-- | @expr '&~:' pat ':=:' rep@ replaces every occurence of @pat@ within @expr@ with @rep@.
--
-- For example, <http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119886- 𝑎>·<http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119887- 𝑏> − <http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119888- 𝑐>·<http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119889- 𝑑> '&~:' <http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-12549- ㄅ>·<http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-12568- ㄘ> ':=:' ㄘ·ㄅ yields 𝑏·𝑎 − 𝑑·𝑐.
(&~:) :: (Eq s⁰, Eq s¹, Eq s²) => CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
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⁰
orig := (CAS' Int s² s¹ s⁰
alt:=[Equality' Int s² s¹ s⁰]
_):[Equality' Int s² s¹ s⁰]
_ = 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⁰
origforall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
alt
OperatorChain CAS s² s¹ s⁰
x [(s², CAS s² s¹ s⁰)]
ys &~: pat :: CAS' Int s² s¹ s⁰
pat@(OperatorChain CAS' Int s² s¹ s⁰
ξ [(s², CAS' Int s² s¹ s⁰)]
υs):=:CAS' Int s² s¹ s⁰
alt
  | Int
exprLength forall a. Ord a => a -> a -> Bool
> Int
patLength
  , ([(s², CAS s² s¹ s⁰)]
remainSect, [(s², CAS s² s¹ s⁰)]
patLSect) <- forall a. Int -> [a] -> ([a], [a])
splitAt (Int
exprLengthforall a. Num a => a -> a -> a
-Int
patLength) [(s², CAS s² s¹ s⁰)]
ys
    = let (s²
or₀, CAS s² s¹ s⁰
yr₀) = forall a. [a] -> a
last [(s², CAS s² s¹ s⁰)]
remainSect
      in case forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern CAS' Int s² s¹ s⁰
pat (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS s² s¹ s⁰
x [(s², CAS s² s¹ s⁰)]
patLSect) of
       Just Map Int (CAS s² s¹ s⁰)
varMatchesL -> case forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
varMatchesL CAS' Int s² s¹ s⁰
alt of
          Just CAS s² s¹ s⁰
patReplaced -> forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator s²
or₀ CAS s² s¹ s⁰
patReplaced
                               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 s² s¹ s⁰
yr₀ (forall a. [a] -> [a]
init [(s², CAS s² s¹ s⁰)]
remainSect) 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⁰
patforall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
alt
       Maybe (Map Int (CAS s² s¹ s⁰))
Nothing -> let (s²
o₀,CAS s² s¹ s⁰
y₀) = forall a. [a] -> a
last [(s², CAS s² s¹ s⁰)]
ys
                  in forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator s²
o₀ (CAS s² s¹ s⁰
xforall 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⁰
patforall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
alt))
                       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 s² s¹ s⁰
y₀ (forall a. [a] -> [a]
init [(s², CAS s² s¹ s⁰)]
ys) 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⁰
patforall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
alt
 where patLength :: Int
patLength = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(s², CAS' Int s² s¹ s⁰)]
υs
       exprLength :: Int
exprLength = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(s², CAS s² s¹ s⁰)]
ys
CAS s² s¹ s⁰
e &~: CAS' Int s² s¹ s⁰
orig:=:CAS' Int s² s¹ s⁰
alt
  | Just Map Int (CAS s² s¹ s⁰)
varMatches <- forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern CAS' Int s² s¹ s⁰
orig CAS s² s¹ s⁰
e
      = case forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
varMatches CAS' Int s² s¹ s⁰
alt of
          Just CAS s² s¹ s⁰
refilled -> CAS s² s¹ s⁰
refilled
Function s¹
f CAS s² s¹ s⁰
x &~: Equality' Int s² s¹ s⁰
p = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function s¹
f forall a b. (a -> b) -> a -> b
$ CAS s² s¹ s⁰
xforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~:Equality' Int s² s¹ s⁰
p
Operator s²
o CAS s² s¹ s⁰
x CAS s² s¹ s⁰
y &~: Equality' Int s² s¹ s⁰
p = forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator s²
o (CAS s² s¹ s⁰
xforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~:Equality' Int s² s¹ s⁰
p) (CAS s² s¹ s⁰
yforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~:Equality' Int s² s¹ s⁰
p)
OperatorChain CAS s² s¹ s⁰
x [] &~: Equality' Int s² s¹ s⁰
p = CAS s² s¹ s⁰
xforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~:Equality' Int s² s¹ s⁰
p
OperatorChain CAS s² s¹ s⁰
x ((s²
oo,CAS s² s¹ s⁰
z):[(s², CAS s² s¹ s⁰)]
ys) &~: Equality' Int s² s¹ s⁰
p
    = forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator s²
oo (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS s² s¹ s⁰
x [(s², CAS s² s¹ s⁰)]
ysforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~:Equality' Int s² s¹ s⁰
p) (CAS s² s¹ s⁰
zforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
&~:Equality' Int s² s¹ s⁰
p)
CAS s² s¹ s⁰
e &~: Equality' Int s² s¹ s⁰
_ = CAS s² s¹ s⁰
e

-- | @expr '&~?' pat ':=:' rep@ gives every possible way @pat@ can be replaced exactly
-- once within @expr@.
--
-- For example, <http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119886- 𝑎>·<http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119887- 𝑏> − <http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119888- 𝑐>·<http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-119889- 𝑑> '&~?' <http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-12549- ㄅ>·<http://hackage.haskell.org/package/dumb-cas/docs/CAS-Dumb-Symbols-Unicode-MathLatin_RomanGreek__BopomofoGaps.html#v:-12568- ㄘ> ':=:' ㄘ·ㄅ yields [𝑏·𝑎 − 𝑐·𝑑, 𝑎·𝑏 − 𝑑·𝑐].
(&~?) :: (Eq s⁰, Eq s¹, Eq s²) => CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
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⁰
orig := (CAS' Int s² s¹ s⁰
alt:=[Equality' Int s² s¹ s⁰]
_):[Equality' Int s² s¹ s⁰]
_ = 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⁰
origforall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
alt
CAS s² s¹ s⁰
e &~? CAS' Int s² s¹ s⁰
orig:=:CAS' Int s² s¹ s⁰
alt
  | Just Map Int (CAS s² s¹ s⁰)
varMatches <- forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern CAS' Int s² s¹ s⁰
orig CAS s² s¹ s⁰
e
      = case forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
varMatches CAS' Int s² s¹ s⁰
alt of
          Just CAS s² s¹ s⁰
refilled -> [CAS s² s¹ s⁰
refilled]
Function s¹
f CAS s² s¹ s⁰
x &~? Equality' Int s² s¹ s⁰
p = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function s¹
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CAS s² s¹ s⁰
xforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~?Equality' Int s² s¹ s⁰
p)
Operator s²
o CAS s² s¹ s⁰
x CAS s² s¹ s⁰
y &~? Equality' Int s² s¹ s⁰
p = (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator s²
o) CAS s² s¹ s⁰
y forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CAS s² s¹ s⁰
xforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~?Equality' Int s² s¹ s⁰
p))
                    forall a. [a] -> [a] -> [a]
++ (      forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator s²
o  CAS s² s¹ s⁰
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CAS s² s¹ s⁰
yforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~?Equality' Int s² s¹ s⁰
p))
OperatorChain CAS s² s¹ s⁰
x [] &~? Equality' Int s² s¹ s⁰
p = CAS s² s¹ s⁰
xforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~?Equality' Int s² s¹ s⁰
p
OperatorChain CAS s² s¹ s⁰
x ((s²
o,CAS s² s¹ s⁰
y):[(s², CAS s² s¹ s⁰)]
zs) &~? p :: Equality' Int s² s¹ s⁰
p@(CAS' Int s² s¹ s⁰
orig:=:CAS' Int s² s¹ s⁰
alt)
       = [ forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator s²
o CAS s² s¹ s⁰
ξs' CAS s² s¹ s⁰
y
         | CAS s² s¹ s⁰
ξs' <- forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS s² s¹ s⁰
x [(s², CAS s² s¹ s⁰)]
zs forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~? Equality' Int s² s¹ s⁰
p ]
      forall a. [a] -> [a] -> [a]
++ [CAS s² s¹ s⁰]
rSectMatched
      forall a. [a] -> [a] -> [a]
++ (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS s² s¹ s⁰
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[(s², CAS s² s¹ s⁰)]
zs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s²
o,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CAS s² s¹ s⁰
yforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~?Equality' Int s² s¹ s⁰
p))
 where rSectMatched :: [CAS s² s¹ s⁰]
rSectMatched
        | OperatorChain CAS' Int s² s¹ s⁰
ξ [(s², CAS' Int s² s¹ s⁰)]
υs <- CAS' Int s² s¹ s⁰
orig
        , Int
patLength <- forall (t :: * -> *) a. Foldable t => t a -> Int
length [(s², CAS' Int s² s¹ s⁰)]
υs
        , Int
exprLength forall a. Ord a => a -> a -> Bool
> Int
patLength
        , ([(s², CAS s² s¹ s⁰)]
patRSect, (s²
o₁,CAS s² s¹ s⁰
z₁):[(s², CAS s² s¹ s⁰)]
remainSect) <- forall a. Int -> [a] -> ([a], [a])
splitAt (Int
patLengthforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ [(s², CAS s² s¹ s⁰)]
zs
        , Just Map Int (CAS s² s¹ s⁰)
varMatches <- forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
Expattern s² s¹ s⁰
-> CAS s² s¹ s⁰ -> Maybe (Map Int (CAS s² s¹ s⁰))
matchPattern CAS' Int s² s¹ s⁰
orig 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 s² s¹ s⁰
z₁ ((s²
o,CAS s² s¹ s⁰
y)forall a. a -> [a] -> [a]
:[(s², CAS s² s¹ s⁰)]
patRSect)
           = case forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
varMatches CAS' Int s² s¹ s⁰
alt of
               Just CAS s² s¹ s⁰
refilled -> [forall s² γ s¹ s⁰.
Eq s² =>
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
associativeOperator s²
o₁
                                  (forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain CAS s² s¹ s⁰
x [(s², CAS s² s¹ s⁰)]
remainSect) CAS s² s¹ s⁰
refilled]
        | Bool
otherwise  = []
       exprLength :: Int
exprLength = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(s², CAS s² s¹ s⁰)]
zs forall a. Num a => a -> a -> a
+ Int
1
CAS s² s¹ s⁰
e &~? Equality' Int s² s¹ s⁰
_ = []


-- | @expr '&~!' pat ':=:' rep@ replaces @pat@ exactly once in @expr@. If this
--   is not possible, an error is raised. If multiple occurences match, the leftmost
--   is preferred.
(&~!) :: ( Eq s⁰, Eq s¹, Eq s²
         , Show (CAS s² s¹ s⁰), Show (CAS' GapId s² s¹ s⁰) )
         => CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> CAS s² s¹ s⁰
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⁰
orig := (CAS' Int s² s¹ s⁰
alt:=[Equality' Int s² s¹ s⁰]
_):[Equality' Int s² s¹ s⁰]
_ = 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⁰
origforall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> Equality' γ s² s¹ s⁰
:=:CAS' Int s² s¹ s⁰
alt
CAS s² s¹ s⁰
e&~!pat :: Equality' Int s² s¹ s⁰
pat@(CAS' Int s² s¹ s⁰
orig:=:CAS' Int s² s¹ s⁰
_) = case CAS s² s¹ s⁰
eforall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
CAS s² s¹ s⁰ -> Eqspattern s² s¹ s⁰ -> [CAS s² s¹ s⁰]
&~?Equality' Int s² s¹ s⁰
pat of
     (CAS s² s¹ s⁰
e':[CAS s² s¹ s⁰]
_) -> CAS s² s¹ s⁰
e'
     []     -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Unable to match pattern "forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show CAS' Int s² s¹ s⁰
orig
                          forall a. [a] -> [a] -> [a]
++[Char]
"\nin expression "forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show CAS s² s¹ s⁰
e


fillGaps :: Map GapId (CAS s² s¹ s⁰) -> (Expattern s² s¹ s⁰) -> Maybe (CAS s² s¹ s⁰)
fillGaps :: forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
matches (Gap Int
i)
  | rematch :: Maybe (CAS s² s¹ s⁰)
rematch@(Just CAS s² s¹ s⁰
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int (CAS s² s¹ s⁰)
matches  = Maybe (CAS s² s¹ s⁰)
rematch
fillGaps Map Int (CAS s² s¹ s⁰)
matches (Symbol s⁰
s) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall γ s² s¹ s⁰. s⁰ -> CAS' γ s² s¹ s⁰
Symbol s⁰
s
fillGaps Map Int (CAS s² s¹ s⁰)
matches (Function s¹
f CAS' Int s² s¹ s⁰
x) = forall γ s² s¹ s⁰. s¹ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Function s¹
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
matches CAS' Int s² s¹ s⁰
x
fillGaps Map Int (CAS s² s¹ s⁰)
matches (Operator s²
o CAS' Int s² s¹ s⁰
x CAS' Int s² s¹ s⁰
y)
    = forall γ s² s¹ s⁰.
s² -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰ -> CAS' γ s² s¹ s⁰
Operator s²
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
matches CAS' Int s² s¹ s⁰
x
                 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
matches CAS' Int s² s¹ s⁰
y
fillGaps Map Int (CAS s² s¹ s⁰)
matches (OperatorChain CAS' Int s² s¹ s⁰
x [(s², CAS' Int s² s¹ s⁰)]
ys)
    = forall γ s² s¹ s⁰.
CAS' γ s² s¹ s⁰ -> [(s², CAS' γ s² s¹ s⁰)] -> CAS' γ s² s¹ s⁰
OperatorChain forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
matches CAS' Int s² s¹ s⁰
x
                    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (s²
o,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s² s¹ s⁰.
Map Int (CAS s² s¹ s⁰)
-> Expattern s² s¹ s⁰ -> Maybe (CAS s² s¹ s⁰)
fillGaps Map Int (CAS s² s¹ s⁰)
matches CAS' Int s² s¹ s⁰
y | (s²
o,CAS' Int s² s¹ s⁰
y) <- [(s², CAS' Int s² s¹ s⁰)]
ys ]
fillGaps Map Int (CAS s² s¹ s⁰)
_ CAS' Int s² s¹ s⁰
_ = forall a. Maybe a
Nothing

exploreEquality :: (Eq s⁰, Eq s¹, Eq s²)
           => [Expattern s² s¹ s⁰] -> CAS s² s¹ s⁰ -> Equality s² s¹ s⁰
exploreEquality :: forall s⁰ s¹ s².
(Eq s⁰, Eq s¹, Eq s²) =>
[Expattern s² s¹ s⁰] -> CAS s² s¹ s⁰ -> Equality s² s¹ s⁰
exploreEquality [Expattern s² s¹ s⁰]
tfms = forall a. HasCallStack => a
undefined





showStructure :: CAS' γ s² s¹ s⁰ -> String
showStructure :: forall γ s² s¹ s⁰. CAS' γ s² s¹ s⁰ -> [Char]
showStructure CAS' γ s² s¹ s⁰
e = forall {γ} {a} {s¹} {s⁰}. CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go CAS' γ s² s¹ s⁰
e [Char]
""
 where go :: CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go (Symbol s⁰
_) = (Char
'σ'forall a. a -> [a] -> [a]
:)
       go (Gap γ
_) = (Char
'γ'forall a. a -> [a] -> [a]
:)
       go (Function s¹
_ CAS' γ a s¹ s⁰
x) = ([Char]
"φ ("forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go CAS' γ a s¹ s⁰
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
')'forall a. a -> [a] -> [a]
:)
       go (Operator a
_ CAS' γ a s¹ s⁰
x CAS' γ a s¹ s⁰
y) = (Char
'('forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go CAS' γ a s¹ s⁰
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
")`υ`("forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go CAS' γ a s¹ s⁰
y forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
")"forall a. [a] -> [a] -> [a]
++)
       go (OperatorChain CAS' γ a s¹ s⁰
x [(a, CAS' γ a s¹ s⁰)]
ys) = ([Char]
"χ ["forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go CAS' γ a s¹ s⁰
x
                              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
$ (([Char]
", "forall a. [a] -> [a] -> [a]
++)forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CAS' γ a s¹ s⁰ -> [Char] -> [Char]
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall a. [a] -> [a]
reverse [(a, CAS' γ a s¹ s⁰)]
ys) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
']'forall a. a -> [a] -> [a]
:)



type Unwieldiness = Double

class Unwieldy e where
  unwieldiness :: e -> Unwieldiness

instance (Unwieldy s², Unwieldy s¹, Unwieldy s⁰) => Unwieldy (CAS s² s¹ s⁰) where
  unwieldiness :: CAS s² s¹ s⁰ -> Unwieldiness
unwieldiness (Symbol s⁰
s) = forall e. Unwieldy e => e -> Unwieldiness
unwieldiness s⁰
s
  unwieldiness (Function s¹
f CAS s² s¹ s⁰
x) = forall e. Unwieldy e => e -> Unwieldiness
unwieldiness s¹
f forall a. Num a => a -> a -> a
+ forall e. Unwieldy e => e -> Unwieldiness
unwieldiness CAS s² s¹ s⁰
x
  unwieldiness (Operator s²
o CAS s² s¹ s⁰
x CAS s² s¹ s⁰
y)
      = forall e. Unwieldy e => e -> Unwieldiness
unwieldiness s²
o forall a. Num a => a -> a -> a
+ forall e. Unwieldy e => e -> Unwieldiness
unwieldiness CAS s² s¹ s⁰
x forall a. Num a => a -> a -> a
+ Unwieldiness
bigFirstPreferenceforall a. Num a => a -> a -> a
*forall e. Unwieldy e => e -> Unwieldiness
unwieldiness CAS s² s¹ s⁰
y
  unwieldiness (OperatorChain CAS s² s¹ s⁰
x [(s², CAS s² s¹ s⁰)]
ys)
      = forall e. Unwieldy e => e -> Unwieldiness
unwieldiness CAS s² s¹ s⁰
x forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ Unwieldiness
q forall a. Num a => a -> a -> a
* (forall e. Unwieldy e => e -> Unwieldiness
unwieldiness s²
o forall a. Num a => a -> a -> a
+ forall e. Unwieldy e => e -> Unwieldiness
unwieldiness CAS s² s¹ s⁰
y)
                             | (Unwieldiness
q,(s²
o,CAS s² s¹ s⁰
y)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Unwieldiness
1, Unwieldiness
bigFirstPreference ..] forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [(s², CAS s² s¹ s⁰)]
ys ]

-- | How much it is preferred to start an operator-chain with the most complex
--   subexpression (e.g. with the highest-order monomial).
bigFirstPreference :: Unwieldiness
bigFirstPreference :: Unwieldiness
bigFirstPreference = Unwieldiness
1 forall a. Num a => a -> a -> a
+ Unwieldiness
1e-6