module Factor.Term
where
import qualified Data.Char as Char
import qualified Data.List as List
import System.Random (RandomGen)
import Text.Parsec ((<|>),Parsec,ParseError)
import qualified Text.Parsec as Parsec
import Text.PrettyPrint ((<+>),Doc)
import qualified Text.PrettyPrint as PP
import Factor.Prime (Gfp,Prime,PrimePower)
import qualified Factor.Prime as Prime
import Factor.Util
type Index = Int
type Var = String
data Term =
IntegerTerm Integer
| PrimeIndexTerm Index
| NumberWidthTerm Width
| PrimeWidthTerm Width
| CompositeWidthTerm Width
| NegateTerm Term
| AddTerm Term Term
| SubtractTerm Term Term
| MultiplyTerm Term Term
| ExpTerm Term Term
| VarTerm Var
| ModTerm Term Term
| LetTerm Var Term Term
deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq,Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord,Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show)
modulo :: Term -> Integer -> Term
modulo :: Term -> Integer -> Term
modulo Term
t Integer
p = Term -> Term -> Term
ModTerm Term
t (Integer -> Term
IntegerTerm Integer
p)
fromGfp :: Prime -> Gfp -> Term
fromGfp :: Integer -> Integer -> Term
fromGfp Integer
p Integer
x = Term -> Integer -> Term
modulo (Integer -> Term
IntegerTerm (Integer -> Integer -> Integer
Prime.toSmallestInteger Integer
p Integer
x)) Integer
p
fromPrimePower :: PrimePower -> Term
fromPrimePower :: PrimePower -> Term
fromPrimePower (Integer
p,Integer
1) = Integer -> Term
IntegerTerm Integer
p
fromPrimePower (Integer
p,Integer
k) = Term -> Term -> Term
ExpTerm (Integer -> Term
IntegerTerm Integer
p) (Integer -> Term
IntegerTerm Integer
k)
fromPrimePowers :: [PrimePower] -> Term
fromPrimePowers :: [PrimePower] -> Term
fromPrimePowers = [Term] -> Term
mkProduct ([Term] -> Term)
-> ([PrimePower] -> [Term]) -> [PrimePower] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimePower -> Term) -> [PrimePower] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map PrimePower -> Term
fromPrimePower
mkSum :: [Term] -> Term
mkSum :: [Term] -> Term
mkSum [] = Integer -> Term
IntegerTerm Integer
0
mkSum (Term
t1 : [Term]
ts) = (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\Term
t Term
u -> Term -> Term -> Term
AddTerm Term
t Term
u) Term
t1 [Term]
ts
mkProduct :: [Term] -> Term
mkProduct :: [Term] -> Term
mkProduct [] = Integer -> Term
IntegerTerm Integer
1
mkProduct (Term
t1 : [Term]
ts) = (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\Term
t Term
u -> Term -> Term -> Term
MultiplyTerm Term
t Term
u) Term
t1 [Term]
ts
subterms :: Term -> [Term]
subterms :: Term -> [Term]
subterms (NegateTerm Term
t) = [Term
t]
subterms (AddTerm Term
t Term
u) = [Term
t,Term
u]
subterms (SubtractTerm Term
t Term
u) = [Term
t,Term
u]
subterms (MultiplyTerm Term
t Term
u) = [Term
t,Term
u]
subterms (ExpTerm Term
t Term
u) = [Term
t,Term
u]
subterms (ModTerm Term
t Term
u) = [Term
t,Term
u]
subterms (LetTerm String
_ Term
e Term
t) = [Term
e,Term
t]
subterms Term
_ = []
data Result =
RewriteResult Term
| UnchangedResult
| ErrorResult
deriving (Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c== :: Result -> Result -> Bool
Eq,Eq Result
Eq Result
-> (Result -> Result -> Ordering)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Result)
-> (Result -> Result -> Result)
-> Ord Result
Result -> Result -> Bool
Result -> Result -> Ordering
Result -> Result -> Result
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Result -> Result -> Result
$cmin :: Result -> Result -> Result
max :: Result -> Result -> Result
$cmax :: Result -> Result -> Result
>= :: Result -> Result -> Bool
$c>= :: Result -> Result -> Bool
> :: Result -> Result -> Bool
$c> :: Result -> Result -> Bool
<= :: Result -> Result -> Bool
$c<= :: Result -> Result -> Bool
< :: Result -> Result -> Bool
$c< :: Result -> Result -> Bool
compare :: Result -> Result -> Ordering
$ccompare :: Result -> Result -> Ordering
$cp1Ord :: Eq Result
Ord,Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> Result -> ShowS
Show)
newtype Rewrite = Rewrite { Rewrite -> Term -> Result
unRewrite :: Term -> Result }
applyRewrite :: Rewrite -> Term -> Maybe Term
applyRewrite :: Rewrite -> Term -> Maybe Term
applyRewrite Rewrite
rw Term
tm =
case Rewrite -> Term -> Result
unRewrite Rewrite
rw Term
tm of
RewriteResult Term
tm' -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
tm'
Result
UnchangedResult -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
tm
Result
ErrorResult -> Maybe Term
forall a. Maybe a
Nothing
applyRewriteUnsafe :: Rewrite -> Term -> Term
applyRewriteUnsafe :: Rewrite -> Term -> Term
applyRewriteUnsafe Rewrite
rw Term
tm =
case Rewrite -> Term -> Maybe Term
applyRewrite Rewrite
rw Term
tm of
Just Term
tm' -> Term
tm'
Maybe Term
Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ String
"couldn't rewrite " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm
idRewrite :: Rewrite
idRewrite :: Rewrite
idRewrite = (Term -> Result) -> Rewrite
Rewrite (Result -> Term -> Result
forall a b. a -> b -> a
const Result
UnchangedResult)
errorRewrite :: Rewrite
errorRewrite :: Rewrite
errorRewrite = (Term -> Result) -> Rewrite
Rewrite (Result -> Term -> Result
forall a b. a -> b -> a
const Result
ErrorResult)
tryRewrite :: Rewrite -> Rewrite
tryRewrite :: Rewrite -> Rewrite
tryRewrite (Rewrite Term -> Result
rw) = (Term -> Result) -> Rewrite
Rewrite ((Term -> Result) -> Rewrite) -> (Term -> Result) -> Rewrite
forall a b. (a -> b) -> a -> b
$ \Term
tm ->
case Term -> Result
rw Term
tm of
Result
ErrorResult -> Result
UnchangedResult
Result
res -> Result
res
thenRewrite :: Rewrite -> Rewrite -> Rewrite
thenRewrite :: Rewrite -> Rewrite -> Rewrite
thenRewrite (Rewrite Term -> Result
rw1) (Rewrite Term -> Result
rw2) = (Term -> Result) -> Rewrite
Rewrite ((Term -> Result) -> Rewrite) -> (Term -> Result) -> Rewrite
forall a b. (a -> b) -> a -> b
$ \Term
tm ->
case Term -> Result
rw1 Term
tm of
res1 :: Result
res1 @ (RewriteResult Term
tm') ->
case Term -> Result
rw2 Term
tm' of
Result
UnchangedResult -> Result
res1
Result
res2 -> Result
res2
Result
UnchangedResult -> Term -> Result
rw2 Term
tm
Result
ErrorResult -> Result
ErrorResult
orelseRewrite :: Rewrite -> Rewrite -> Rewrite
orelseRewrite :: Rewrite -> Rewrite -> Rewrite
orelseRewrite (Rewrite Term -> Result
rw1) (Rewrite Term -> Result
rw2) = (Term -> Result) -> Rewrite
Rewrite ((Term -> Result) -> Rewrite) -> (Term -> Result) -> Rewrite
forall a b. (a -> b) -> a -> b
$ \Term
tm ->
case Term -> Result
rw1 Term
tm of
Result
ErrorResult -> Term -> Result
rw2 Term
tm
Result
res1 -> Result
res1
firstRewrite :: [Rewrite] -> Rewrite
firstRewrite :: [Rewrite] -> Rewrite
firstRewrite = (Rewrite -> Rewrite -> Rewrite) -> Rewrite -> [Rewrite] -> Rewrite
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Rewrite -> Rewrite -> Rewrite
orelseRewrite Rewrite
errorRewrite
subtermRewrite :: Rewrite -> Rewrite
subtermRewrite :: Rewrite -> Rewrite
subtermRewrite (Rewrite Term -> Result
rw) = (Term -> Result) -> Rewrite
Rewrite Term -> Result
sub
where
sub :: Term -> Result
sub (NegateTerm Term
t) = (Term -> Term) -> Term -> Result
sub1 Term -> Term
NegateTerm Term
t
sub (AddTerm Term
t Term
u) = (Term -> Term -> Term) -> Term -> Term -> Result
sub2 Term -> Term -> Term
AddTerm Term
t Term
u
sub (SubtractTerm Term
t Term
u) = (Term -> Term -> Term) -> Term -> Term -> Result
sub2 Term -> Term -> Term
SubtractTerm Term
t Term
u
sub (MultiplyTerm Term
t Term
u) = (Term -> Term -> Term) -> Term -> Term -> Result
sub2 Term -> Term -> Term
MultiplyTerm Term
t Term
u
sub (ExpTerm Term
t Term
u) = (Term -> Term -> Term) -> Term -> Term -> Result
sub2 Term -> Term -> Term
ExpTerm Term
t Term
u
sub (ModTerm Term
t Term
u) = (Term -> Term -> Term) -> Term -> Term -> Result
sub2 Term -> Term -> Term
ModTerm Term
t Term
u
sub (LetTerm String
v Term
e Term
t) = (Term -> Term -> Term) -> Term -> Term -> Result
sub2 (String -> Term -> Term -> Term
LetTerm String
v) Term
e Term
t
sub Term
_ = Result
UnchangedResult
sub1 :: (Term -> Term) -> Term -> Result
sub1 Term -> Term
c Term
t =
case Term -> Result
rw Term
t of
RewriteResult Term
t' -> Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term
c Term
t'
Result
UnchangedResult -> Result
UnchangedResult
Result
ErrorResult -> Result
ErrorResult
sub2 :: (Term -> Term -> Term) -> Term -> Term -> Result
sub2 Term -> Term -> Term
c Term
t Term
u =
case (Term -> Result
rw Term
t, Term -> Result
rw Term
u) of
(RewriteResult Term
t', RewriteResult Term
u') -> Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
c Term
t' Term
u'
(RewriteResult Term
t', Result
UnchangedResult) -> Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
c Term
t' Term
u
(Result
UnchangedResult, RewriteResult Term
u') -> Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
c Term
t Term
u'
(Result
UnchangedResult, Result
UnchangedResult) -> Result
UnchangedResult
(Result, Result)
_ -> Result
ErrorResult
bottomUpRewrite :: Rewrite -> Rewrite
bottomUpRewrite :: Rewrite -> Rewrite
bottomUpRewrite Rewrite
rw = Rewrite
go
where go :: Rewrite
go = Rewrite -> Rewrite -> Rewrite
thenRewrite (Rewrite -> Rewrite
subtermRewrite Rewrite
go) (Rewrite -> Rewrite
tryRewrite Rewrite
rw)
instVarRewrite :: Var -> Term -> Rewrite
instVarRewrite :: String -> Term -> Rewrite
instVarRewrite String
v Term
t = (Term -> Result) -> Rewrite
Rewrite Term -> Result
inst
where
inst :: Term -> Result
inst (VarTerm String
w) | String
w String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v = Result
res
inst Term
_ = Result
ErrorResult
res :: Result
res = if Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Term
VarTerm String
v then Result
UnchangedResult else Term -> Result
RewriteResult Term
t
expandLetRewrite :: Rewrite -> (Rewrite -> Rewrite) -> Rewrite
expandLetRewrite :: Rewrite -> (Rewrite -> Rewrite) -> Rewrite
expandLetRewrite (Rewrite Term -> Result
rw1) Rewrite -> Rewrite
rw2 = (Term -> Result) -> Rewrite
Rewrite Term -> Result
bind
where
bind :: Term -> Result
bind (LetTerm String
v Term
e Term
t) =
case Term -> Result
rw1 Term
e of
RewriteResult Term
e' -> Rewrite -> Term -> Result
body (Rewrite -> Rewrite
rw2 (Rewrite -> Rewrite) -> Rewrite -> Rewrite
forall a b. (a -> b) -> a -> b
$ String -> Term -> Rewrite
instVarRewrite String
v Term
e') Term
t
Result
UnchangedResult -> Rewrite -> Term -> Result
body (Rewrite -> Rewrite
rw2 (Rewrite -> Rewrite) -> Rewrite -> Rewrite
forall a b. (a -> b) -> a -> b
$ String -> Term -> Rewrite
instVarRewrite String
v Term
e) Term
t
Result
ErrorResult -> Result
ErrorResult
bind Term
_ = Result
ErrorResult
body :: Rewrite -> Term -> Result
body (Rewrite Term -> Result
rw) Term
t =
case Term -> Result
rw Term
t of
Result
UnchangedResult -> Term -> Result
RewriteResult Term
t
Result
res -> Result
res
expandLetsRewrite :: Rewrite -> Rewrite
expandLetsRewrite :: Rewrite -> Rewrite
expandLetsRewrite = Rewrite -> Rewrite
go
where
go :: Rewrite -> Rewrite
go Rewrite
rw = Rewrite -> Rewrite -> Rewrite
orelseRewrite
(Rewrite -> (Rewrite -> Rewrite) -> Rewrite
expandLetRewrite (Rewrite -> Rewrite
go Rewrite
rw) (Rewrite -> Rewrite
go (Rewrite -> Rewrite) -> (Rewrite -> Rewrite) -> Rewrite -> Rewrite
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rewrite -> Rewrite -> Rewrite) -> Rewrite -> Rewrite -> Rewrite
forall a b c. (a -> b -> c) -> b -> a -> c
flip Rewrite -> Rewrite -> Rewrite
orelseRewrite Rewrite
rw))
(Rewrite -> Rewrite -> Rewrite
thenRewrite (Rewrite -> Rewrite
subtermRewrite (Rewrite -> Rewrite
go Rewrite
rw)) (Rewrite -> Rewrite
tryRewrite Rewrite
rw))
uniform :: RandomGen r => Term -> r -> (Term,r)
uniform :: Term -> r -> (Term, r)
uniform (PrimeIndexTerm Int
i) r
r = (Integer -> Term
IntegerTerm Integer
p, r
r)
where p :: Integer
p = [Integer]
Prime.primes [Integer] -> Int -> Integer
forall a. [a] -> Int -> a
!! Int
i
uniform (NumberWidthTerm Int
w) r
r = (Integer -> Term
IntegerTerm Integer
n, r
r')
where (Integer
n,r
r') = Int -> r -> (Integer, r)
forall r. RandomGen r => Int -> r -> (Integer, r)
uniformInteger Int
w r
r
uniform (PrimeWidthTerm Int
w) r
r = (Integer -> Term
IntegerTerm Integer
p, r
r')
where (Integer
p,r
r') = Int -> r -> (Integer, r)
forall r. RandomGen r => Int -> r -> (Integer, r)
Prime.uniformPrime Int
w r
r
uniform (CompositeWidthTerm Int
w) r
r = (Integer -> Term
IntegerTerm Integer
c, r
r')
where (Integer
c,r
r') = Int -> r -> (Integer, r)
forall r. RandomGen r => Int -> r -> (Integer, r)
Prime.uniformComposite Int
w r
r
uniform (NegateTerm Term
t) r
r = (Term -> Term
NegateTerm Term
t', r
r')
where (Term
t',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r
uniform (AddTerm Term
t Term
u) r
r = (Term -> Term -> Term
AddTerm Term
t' Term
u', r
r'')
where
(Term
t',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r
(Term
u',r
r'') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
u r
r'
uniform (SubtractTerm Term
t Term
u) r
r = (Term -> Term -> Term
SubtractTerm Term
t' Term
u', r
r'')
where
(Term
t',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r
(Term
u',r
r'') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
u r
r'
uniform (MultiplyTerm Term
t Term
u) r
r = (Term -> Term -> Term
MultiplyTerm Term
t' Term
u', r
r'')
where
(Term
t',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r
(Term
u',r
r'') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
u r
r'
uniform (ExpTerm Term
t Term
u) r
r = (Term -> Term -> Term
ExpTerm Term
t' Term
u', r
r'')
where
(Term
t',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r
(Term
u',r
r'') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
u r
r'
uniform (ModTerm Term
t Term
u) r
r = (Term -> Term -> Term
ModTerm Term
t' Term
u', r
r'')
where
(Term
t',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r
(Term
u',r
r'') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
u r
r'
uniform (LetTerm String
v Term
e Term
t) r
r = (String -> Term -> Term -> Term
LetTerm String
v Term
e' Term
t', r
r'')
where
(Term
e',r
r') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
e r
r
(Term
t',r
r'') = Term -> r -> (Term, r)
forall r. RandomGen r => Term -> r -> (Term, r)
uniform Term
t r
r'
uniform Term
tm r
r = (Term
tm,r
r)
negativeIntegerRewrite :: Rewrite
negativeIntegerRewrite :: Rewrite
negativeIntegerRewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (IntegerTerm Integer
i) | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term
NegateTerm (Integer -> Term
IntegerTerm (-Integer
i))
rw Term
_ = Result
ErrorResult
negateNegateRewrite :: Rewrite
negateNegateRewrite :: Rewrite
negateNegateRewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (NegateTerm (NegateTerm Term
t)) = Term -> Result
RewriteResult Term
t
rw Term
_ = Result
ErrorResult
addNegate2Rewrite :: Rewrite
addNegate2Rewrite :: Rewrite
addNegate2Rewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (AddTerm Term
t (NegateTerm Term
u)) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
SubtractTerm Term
t Term
u
rw Term
_ = Result
ErrorResult
subtractNegate2Rewrite :: Rewrite
subtractNegate2Rewrite :: Rewrite
subtractNegate2Rewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (SubtractTerm Term
t (NegateTerm Term
u)) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
AddTerm Term
t Term
u
rw Term
_ = Result
ErrorResult
multiplyNegateRewrite :: Rewrite
multiplyNegateRewrite :: Rewrite
multiplyNegateRewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (MultiplyTerm (NegateTerm Term
t) (NegateTerm Term
u)) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
MultiplyTerm Term
t Term
u
rw (MultiplyTerm Term
t (NegateTerm Term
u)) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term
NegateTerm (Term -> Term -> Term
MultiplyTerm Term
t Term
u)
rw (MultiplyTerm (NegateTerm Term
t) Term
u) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Term
NegateTerm (Term -> Term -> Term
MultiplyTerm Term
t Term
u)
rw Term
_ = Result
ErrorResult
nnfInteger :: Term -> Term
nnfInteger :: Term -> Term
nnfInteger = Rewrite -> Term -> Term
applyRewriteUnsafe (Rewrite -> Rewrite
bottomUpRewrite Rewrite
negativeIntegerRewrite)
nnf :: Term -> Term
nnf :: Term -> Term
nnf = Rewrite -> Term -> Term
applyRewriteUnsafe (Rewrite -> Term -> Term) -> Rewrite -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Rewrite -> Rewrite
bottomUpRewrite (Rewrite -> Rewrite) -> Rewrite -> Rewrite
forall a b. (a -> b) -> a -> b
$ [Rewrite] -> Rewrite
firstRewrite
[Rewrite
negativeIntegerRewrite,
Rewrite
negateNegateRewrite,
Rewrite
addNegate2Rewrite,
Rewrite
subtractNegate2Rewrite,
Rewrite
multiplyNegateRewrite]
multiplyOneRewrite :: Rewrite
multiplyOneRewrite :: Rewrite
multiplyOneRewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (MultiplyTerm (IntegerTerm Integer
1) Term
u) = Term -> Result
RewriteResult Term
u
rw (MultiplyTerm Term
t (IntegerTerm Integer
1)) = Term -> Result
RewriteResult Term
t
rw Term
_ = Result
ErrorResult
expOneRewrite :: Rewrite
expOneRewrite :: Rewrite
expOneRewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (ExpTerm (IntegerTerm Integer
1) Term
_) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Integer -> Term
IntegerTerm Integer
1
rw (ExpTerm Term
t (IntegerTerm Integer
1)) = Term -> Result
RewriteResult Term
t
rw Term
_ = Result
ErrorResult
expZeroRewrite :: Rewrite
expZeroRewrite :: Rewrite
expZeroRewrite = (Term -> Result) -> Rewrite
Rewrite Term -> Result
rw
where
rw :: Term -> Result
rw (ExpTerm Term
_ (IntegerTerm Integer
0)) = Term -> Result
RewriteResult (Term -> Result) -> Term -> Result
forall a b. (a -> b) -> a -> b
$ Integer -> Term
IntegerTerm Integer
1
rw Term
_ = Result
ErrorResult
simplify :: Term -> Term
simplify :: Term -> Term
simplify = Rewrite -> Term -> Term
applyRewriteUnsafe (Rewrite -> Term -> Term) -> Rewrite -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Rewrite -> Rewrite
bottomUpRewrite (Rewrite -> Rewrite) -> Rewrite -> Rewrite
forall a b. (a -> b) -> a -> b
$ [Rewrite] -> Rewrite
firstRewrite
[Rewrite
multiplyOneRewrite,
Rewrite
expOneRewrite,
Rewrite
expZeroRewrite]
isReservedWord :: String -> Bool
isReservedWord :: String -> Bool
isReservedWord String
"in" = Bool
True
isReservedWord String
"let" = Bool
True
isReservedWord String
"mod" = Bool
True
isReservedWord String
_ = Bool
False
spaceParser :: Parsec String st ()
spaceParser :: Parsec String st ()
spaceParser = String -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
Parsec.oneOf String
" \t\n" ParsecT String st Identity Char
-> Parsec String st () -> Parsec String st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parsec String st ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
spacesParser :: Parsec String st ()
spacesParser :: Parsec String st ()
spacesParser = Parsec String st () -> Parsec String st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany Parsec String st ()
forall st. Parsec String st ()
spaceParser
spaces1Parser :: Parsec String st ()
spaces1Parser :: Parsec String st ()
spaces1Parser = Parsec String st () -> Parsec String st ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany1 Parsec String st ()
forall st. Parsec String st ()
spaceParser
integerParser :: Parsec String st Integer
integerParser :: Parsec String st Integer
integerParser = Parsec String st Integer
forall u. ParsecT String u Identity Integer
zero Parsec String st Integer
-> Parsec String st Integer -> Parsec String st Integer
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parsec String st Integer
forall u. ParsecT String u Identity Integer
positive
where
zero :: ParsecT String u Identity Integer
zero = do
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'0'
Integer -> ParsecT String u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
positive :: ParsecT String u Identity Integer
positive = do
Integer
h <- ParsecT String u Identity Integer
forall u. ParsecT String u Identity Integer
positiveDigit
[Integer]
t <- ParsecT String u Identity Integer
-> ParsecT String u Identity [Integer]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT String u Identity Integer
forall u. ParsecT String u Identity Integer
digit
Integer -> ParsecT String u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\Integer
n Integer
d -> Integer
10Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) Integer
h [Integer]
t)
digit :: ParsecT String u Identity Integer
digit = ParsecT String u Identity Integer
forall u. ParsecT String u Identity Integer
zero ParsecT String u Identity Integer
-> ParsecT String u Identity Integer
-> ParsecT String u Identity Integer
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity Integer
forall u. ParsecT String u Identity Integer
positiveDigit
positiveDigit :: ParsecT String u Identity Integer
positiveDigit = do
Char
d <- String -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
Parsec.oneOf String
"123456789"
Integer -> ParsecT String u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Char -> Int
Char.digitToInt Char
d)
indexParser :: Parsec String st Index
indexParser :: Parsec String st Int
indexParser = do
Char
_ <- Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'_'
Integer
i <- Parsec String st Integer
forall u. ParsecT String u Identity Integer
integerParser
Int -> Parsec String st Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Parsec String st Int) -> Int -> Parsec String st Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
widthParser :: Parsec String st Width
widthParser :: Parsec String st Int
widthParser = do
Char
_ <- Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'['
Parsec String st ()
forall st. Parsec String st ()
spacesParser
Integer
i <- Parsec String st Integer
forall u. ParsecT String u Identity Integer
integerParser
Parsec String st ()
forall st. Parsec String st ()
spacesParser
Char
_ <- Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
']'
Int -> Parsec String st Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Parsec String st Int) -> Int -> Parsec String st Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
classIndexParser :: Char -> Parsec String st Index
classIndexParser :: Char -> Parsec String st Int
classIndexParser Char
c = Parsec String st Int -> Parsec String st Int
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
Parsec.try (Parsec String st Int -> Parsec String st Int)
-> Parsec String st Int -> Parsec String st Int
forall a b. (a -> b) -> a -> b
$ do
Char
_ <- Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
c
Parsec String st Int
forall st. Parsec String st Int
indexParser
primeIndexParser :: Parsec String st Index
primeIndexParser :: Parsec String st Int
primeIndexParser = Char -> Parsec String st Int
forall st. Char -> Parsec String st Int
classIndexParser Char
'P'
classWidthParser :: Char -> Parsec String st Width
classWidthParser :: Char -> Parsec String st Int
classWidthParser Char
c = Parsec String st Int -> Parsec String st Int
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
Parsec.try (Parsec String st Int -> Parsec String st Int)
-> Parsec String st Int -> Parsec String st Int
forall a b. (a -> b) -> a -> b
$ do
Char
_ <- Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
c
Parsec String st ()
forall st. Parsec String st ()
spacesParser
Parsec String st Int
forall st. Parsec String st Int
widthParser
numberWidthParser :: Parsec String st Width
numberWidthParser :: Parsec String st Int
numberWidthParser = Char -> Parsec String st Int
forall st. Char -> Parsec String st Int
classWidthParser Char
'N'
primeWidthParser :: Parsec String st Width
primeWidthParser :: Parsec String st Int
primeWidthParser = Char -> Parsec String st Int
forall st. Char -> Parsec String st Int
classWidthParser Char
'P'
compositeWidthParser :: Parsec String st Width
compositeWidthParser :: Parsec String st Int
compositeWidthParser = Char -> Parsec String st Int
forall st. Char -> Parsec String st Int
classWidthParser Char
'C'
varParser :: Parsec String st Var
varParser :: Parsec String st String
varParser = Parsec String st String -> Parsec String st String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
Parsec.try (Parsec String st String -> Parsec String st String)
-> Parsec String st String -> Parsec String st String
forall a b. (a -> b) -> a -> b
$ do
Char
c <- ParsecT String st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
Parsec.lower
String
cs <- ParsecT String st Identity Char -> Parsec String st String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT String st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
Parsec.alphaNum
let v :: String
v = Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
cs
if String -> Bool
isReservedWord String
v then String -> Parsec String st String
forall s u (m :: * -> *) a. String -> ParsecT s u m a
Parsec.parserFail String
"reserved word" else String -> Parsec String st String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v
termParser :: Parsec String st Term
termParser :: Parsec String st Term
termParser = do { Parsec String st ()
forall st. Parsec String st ()
spacesParser ; Term
t <- Parsec String st Term
forall u. ParsecT String u Identity Term
topTm ; Parsec String st ()
forall st. Parsec String st ()
spacesParser ; Term -> Parsec String st Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t }
where
parensTm :: ParsecT String u Identity Term
parensTm = ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
Parsec.try (ParsecT String u Identity Term -> ParsecT String u Identity Term)
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ do
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'('
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Term
t <- ParsecT String u Identity Term
topTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
')'
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
topTm :: ParsecT String u Identity Term
topTm = ParsecT String u Identity Term
letTm ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity Term
modTm
letTm :: ParsecT String u Identity Term
letTm = do
String
_ <- String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
Parsec.string String
"let"
Parsec String u ()
forall st. Parsec String st ()
spaces1Parser
String
v <- ParsecT String u Identity String
forall st. Parsec String st String
varParser
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'='
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Term
e <- ParsecT String u Identity Term
sumTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
String
_ <- String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
Parsec.string String
"in"
Parsec String u ()
forall st. Parsec String st ()
spaces1Parser
Term
t <- ParsecT String u Identity Term
modTm
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ParsecT String u Identity Term)
-> Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term -> Term
LetTerm String
v Term
e Term
t
modTm :: ParsecT String u Identity Term
modTm = do
Term
t <- ParsecT String u Identity Term
sumTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Maybe Term
m <- ParsecT String u Identity Term
-> ParsecT String u Identity (Maybe Term)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
Parsec.optionMaybe ParsecT String u Identity Term
modOpTm
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ParsecT String u Identity Term)
-> Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ case Maybe Term
m of { Maybe Term
Nothing -> Term
t ; Just Term
p -> Term -> Term -> Term
ModTerm Term
t Term
p }
modOpTm :: ParsecT String u Identity Term
modOpTm = ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
Parsec.try (ParsecT String u Identity Term -> ParsecT String u Identity Term)
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ do
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'('
Parsec String u ()
forall st. Parsec String st ()
spacesParser
String
_ <- String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
Parsec.string String
"mod"
Parsec String u ()
forall st. Parsec String st ()
spaces1Parser
Term
t <- ParsecT String u Identity Term
expTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
')'
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
sumTm :: ParsecT String u Identity Term
sumTm = do
Term
t1 <- ParsecT String u Identity Term
negTm ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity Term
prodTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
[(Term -> Term -> Term, Term)]
ts <- ParsecT String u Identity (Term -> Term -> Term, Term)
-> ParsecT String u Identity [(Term -> Term -> Term, Term)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT String u Identity (Term -> Term -> Term, Term)
addTm
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ParsecT String u Identity Term)
-> Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ (Term -> (Term -> Term -> Term, Term) -> Term)
-> Term -> [(Term -> Term -> Term, Term)] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\Term
t (Term -> Term -> Term
c,Term
u) -> Term -> Term -> Term
c Term
t Term
u) Term
t1 [(Term -> Term -> Term, Term)]
ts
addTm :: ParsecT String u Identity (Term -> Term -> Term, Term)
addTm = do
Term -> Term -> Term
o <- ParsecT String u Identity (Term -> Term -> Term)
forall u. ParsecT String u Identity (Term -> Term -> Term)
addOp
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Term
t <- ParsecT String u Identity Term
prodTm
(Term -> Term -> Term, Term)
-> ParsecT String u Identity (Term -> Term -> Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
o,Term
t)
addOp :: ParsecT String u Identity (Term -> Term -> Term)
addOp =
(Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'+' ParsecT String u Identity Char
-> ParsecT String u Identity (Term -> Term -> Term)
-> ParsecT String u Identity (Term -> Term -> Term)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term -> Term)
-> ParsecT String u Identity (Term -> Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Term -> Term -> Term
AddTerm) ParsecT String u Identity (Term -> Term -> Term)
-> ParsecT String u Identity (Term -> Term -> Term)
-> ParsecT String u Identity (Term -> Term -> Term)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'-' ParsecT String u Identity Char
-> ParsecT String u Identity (Term -> Term -> Term)
-> ParsecT String u Identity (Term -> Term -> Term)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term -> Term)
-> ParsecT String u Identity (Term -> Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Term -> Term -> Term
SubtractTerm)
negTm :: ParsecT String u Identity Term
negTm = do
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'-'
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Term
t <- ParsecT String u Identity Term
prodTm
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ParsecT String u Identity Term)
-> Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
NegateTerm Term
t
prodTm :: ParsecT String u Identity Term
prodTm = do
Term
t1 <- ParsecT String u Identity Term
expTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
[Term]
ts <- ParsecT String u Identity Term -> ParsecT String u Identity [Term]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT String u Identity Term
multTm
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ParsecT String u Identity Term)
-> Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
mkProduct (Term
t1 Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ts)
multTm :: ParsecT String u Identity Term
multTm = do
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'*'
Parsec String u ()
forall st. Parsec String st ()
spacesParser
ParsecT String u Identity Term
expTm
expTm :: ParsecT String u Identity Term
expTm = do
Term
t <- ParsecT String u Identity Term
atomicTm
Parsec String u ()
forall st. Parsec String st ()
spacesParser
Maybe Term
m <- ParsecT String u Identity Term
-> ParsecT String u Identity (Maybe Term)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
Parsec.optionMaybe ParsecT String u Identity Term
expOpTm
Term -> ParsecT String u Identity Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ParsecT String u Identity Term)
-> Term -> ParsecT String u Identity Term
forall a b. (a -> b) -> a -> b
$ case Maybe Term
m of { Maybe Term
Nothing -> Term
t ; Just Term
e -> Term -> Term -> Term
ExpTerm Term
t Term
e }
expOpTm :: ParsecT String u Identity Term
expOpTm = do
Char
_ <- Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'^'
Parsec String u ()
forall st. Parsec String st ()
spacesParser
ParsecT String u Identity Term
expTm
atomicTm :: ParsecT String u Identity Term
atomicTm =
(Integer -> Term
IntegerTerm (Integer -> Term)
-> ParsecT String u Identity Integer
-> ParsecT String u Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String u Identity Integer
forall u. ParsecT String u Identity Integer
integerParser) ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(Int -> Term
PrimeIndexTerm (Int -> Term)
-> ParsecT String u Identity Int -> ParsecT String u Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String u Identity Int
forall st. Parsec String st Int
primeIndexParser) ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(Int -> Term
NumberWidthTerm (Int -> Term)
-> ParsecT String u Identity Int -> ParsecT String u Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String u Identity Int
forall st. Parsec String st Int
numberWidthParser) ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(Int -> Term
PrimeWidthTerm (Int -> Term)
-> ParsecT String u Identity Int -> ParsecT String u Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String u Identity Int
forall st. Parsec String st Int
primeWidthParser) ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(Int -> Term
CompositeWidthTerm (Int -> Term)
-> ParsecT String u Identity Int -> ParsecT String u Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String u Identity Int
forall st. Parsec String st Int
compositeWidthParser) ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(String -> Term
VarTerm (String -> Term)
-> ParsecT String u Identity String
-> ParsecT String u Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String u Identity String
forall st. Parsec String st String
varParser) ParsecT String u Identity Term
-> ParsecT String u Identity Term -> ParsecT String u Identity Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
ParsecT String u Identity Term
parensTm
parse :: String -> Either ParseError Term
parse :: String -> Either ParseError Term
parse = Parsec String () Term -> String -> String -> Either ParseError Term
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
Parsec.parse (Parsec String () Term
forall u. ParsecT String u Identity Term
termParser Parsec String () Term
-> ParsecT String () Identity () -> Parsec String () Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
Parsec.eof) String
""
fromString :: String -> Maybe Term
fromString :: String -> Maybe Term
fromString String
s = case String -> Either ParseError Term
parse String
s of { Left ParseError
_ -> Maybe Term
forall a. Maybe a
Nothing ; Right Term
t -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
t }
indexToDoc :: Index -> Doc
indexToDoc :: Int -> Doc
indexToDoc Int
i = Char -> Doc
PP.char Char
'_' Doc -> Doc -> Doc
PP.<> Int -> Doc
PP.int Int
i
widthToDoc :: Width -> Doc
widthToDoc :: Int -> Doc
widthToDoc = Doc -> Doc
PP.brackets (Doc -> Doc) -> (Int -> Doc) -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc
PP.int
atomicToDoc :: Term -> Doc
atomicToDoc :: Term -> Doc
atomicToDoc (IntegerTerm Integer
n) = Integer -> Doc
PP.integer Integer
n
atomicToDoc (PrimeIndexTerm Int
w) = Char -> Doc
PP.char Char
'P' Doc -> Doc -> Doc
PP.<> Int -> Doc
indexToDoc Int
w
atomicToDoc (NumberWidthTerm Int
w) = Char -> Doc
PP.char Char
'N' Doc -> Doc -> Doc
PP.<> Int -> Doc
widthToDoc Int
w
atomicToDoc (PrimeWidthTerm Int
w) = Char -> Doc
PP.char Char
'P' Doc -> Doc -> Doc
PP.<> Int -> Doc
widthToDoc Int
w
atomicToDoc (CompositeWidthTerm Int
w) = Char -> Doc
PP.char Char
'C' Doc -> Doc -> Doc
PP.<> Int -> Doc
widthToDoc Int
w
atomicToDoc (VarTerm String
v) = String -> Doc
PP.text String
v
atomicToDoc Term
tm = Doc -> Doc
PP.parens (Term -> Doc
toDoc Term
tm)
expToDoc :: Term -> Doc
expToDoc :: Term -> Doc
expToDoc = [Doc] -> Doc
PP.fcat ([Doc] -> Doc) -> (Term -> [Doc]) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Doc]
strip
where
strip :: Term -> [Doc]
strip (ExpTerm Term
t Term
u) = (Term -> Doc
atomicToDoc Term
t Doc -> Doc -> Doc
PP.<> Char -> Doc
PP.char Char
'^') Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Term -> [Doc]
strip Term
u
strip Term
t = [Term -> Doc
atomicToDoc Term
t]
prodToDoc :: Term -> Doc
prodToDoc :: Term -> Doc
prodToDoc = [Doc] -> Term -> Doc
strip []
where
strip :: [Doc] -> Term -> Doc
strip [Doc]
l (MultiplyTerm Term
t Term
u) = [Doc] -> Term -> Doc
strip ((Char -> Doc
PP.char Char
'*' Doc -> Doc -> Doc
<+> Term -> Doc
expToDoc Term
u) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
l) Term
t
strip [Doc]
l Term
t = [Doc] -> Doc
PP.fsep (Term -> Doc
expToDoc Term
t Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
l)
negateToDoc :: Term -> Doc
negateToDoc :: Term -> Doc
negateToDoc (NegateTerm Term
t) = Char -> Doc
PP.char Char
'-' Doc -> Doc -> Doc
PP.<> Term -> Doc
prodToDoc Term
t
negateToDoc Term
tm = Term -> Doc
prodToDoc Term
tm
sumToDoc :: Term -> Doc
sumToDoc :: Term -> Doc
sumToDoc = [Doc] -> Term -> Doc
strip []
where
strip :: [Doc] -> Term -> Doc
strip [Doc]
l (AddTerm Term
t Term
u) = [Doc] -> Term -> Doc
strip ((Char -> Doc
PP.char Char
'+' Doc -> Doc -> Doc
<+> Term -> Doc
prodToDoc Term
u) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
l) Term
t
strip [Doc]
l (SubtractTerm Term
t Term
u) = [Doc] -> Term -> Doc
strip ((Char -> Doc
PP.char Char
'-' Doc -> Doc -> Doc
<+> Term -> Doc
prodToDoc Term
u) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
l) Term
t
strip [Doc]
l Term
t = [Doc] -> Doc
PP.fsep (Term -> Doc
negateToDoc Term
t Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
l)
modToDoc :: Term -> Doc
modToDoc :: Term -> Doc
modToDoc (ModTerm Term
t Term
m) =
Term -> Doc
sumToDoc Term
t Doc -> Doc -> Doc
<+> Doc -> Doc
PP.parens (String -> Doc
PP.text String
"mod" Doc -> Doc -> Doc
<+> Term -> Doc
expToDoc Term
m)
modToDoc Term
tm = Term -> Doc
sumToDoc Term
tm
toDoc :: Term -> Doc
toDoc :: Term -> Doc
toDoc (LetTerm String
v Term
e Term
t) =
String -> Doc
PP.text String
"let" Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
v Doc -> Doc -> Doc
<+> Char -> Doc
PP.char Char
'=' Doc -> Doc -> Doc
<+>
Term -> Doc
sumToDoc Term
e Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"in" Doc -> Doc -> Doc
<+> Term -> Doc
modToDoc Term
t
toDoc Term
tm = Term -> Doc
modToDoc Term
tm
toString :: Term -> String
toString :: Term -> String
toString = Style -> Doc -> String
PP.renderStyle Style
style (Doc -> String) -> (Term -> Doc) -> Term -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
toDoc
where style :: Style
style = Style
PP.style {lineLength :: Int
PP.lineLength = Int
80, ribbonsPerLine :: Float
PP.ribbonsPerLine = Float
1.0}