{- |
module: Factor.Term
description: Expression terms
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}
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

-------------------------------------------------------------------------------
-- Terms
-------------------------------------------------------------------------------

type Index = Int  -- Non-negative

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)

-------------------------------------------------------------------------------
-- Constructors and destructors
-------------------------------------------------------------------------------

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 (used for shrinking QuickCheck counterexamples)
-------------------------------------------------------------------------------

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
_ = []

-------------------------------------------------------------------------------
-- Rewriting terms
-------------------------------------------------------------------------------

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

-- Never returns an error result
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)

-------------------------------------------------------------------------------
-- Expanding let terms
-------------------------------------------------------------------------------

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

-- Never returns an error result
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))

-------------------------------------------------------------------------------
-- Picking/computing concrete values
-------------------------------------------------------------------------------

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)

-------------------------------------------------------------------------------
-- Lifting negations
-------------------------------------------------------------------------------

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]

-------------------------------------------------------------------------------
-- Simplifying terms
-------------------------------------------------------------------------------

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]

-------------------------------------------------------------------------------
-- Parsing terms
-------------------------------------------------------------------------------

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 }

-------------------------------------------------------------------------------
-- Pretty-printing terms
-------------------------------------------------------------------------------

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}