{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Nat (termToInt, intToTerm, parseTerm, pp, s, z) where


import Data.Text
import Text.Parsec (Parsec, ParsecT, Stream)
import Text.ParserCombinators.Parsec.Char
import Text.ParserCombinators.Parsec
import Data.String

import qualified Language.REST.MetaTerm as MT
import           Language.REST.Op
import           Language.REST.Types
import           Language.REST.RuntimeTerm as RT

z, s :: Op
s :: Op
s      = Text -> Op
Op Text
"s"
z :: Op
z      = Text -> Op
Op Text
"z"

intToTerm :: Int -> RuntimeTerm
intToTerm :: Int -> RuntimeTerm
intToTerm Int
0 = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
z []
intToTerm Int
n = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
s [Int -> RuntimeTerm
intToTerm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]

termToInt :: (MT.ToMetaTerm a) => a -> Maybe Int
termToInt :: forall a. ToMetaTerm a => a -> Maybe Int
termToInt a
t = MetaTerm -> Maybe Int
forall {a}. Num a => MetaTerm -> Maybe a
go (a -> MetaTerm
forall a. ToMetaTerm a => a -> MetaTerm
MT.toMetaTerm a
t) where
  go :: MetaTerm -> Maybe a
go (MT.RWApp Op
mop [])   | Op
mop Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
z = a -> Maybe a
forall a. a -> Maybe a
Just a
0
  go (MT.RWApp Op
mop [MetaTerm
t1]) | Op
mop Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
s = (a
1 a -> a -> a
forall a. Num a => a -> a -> a
+) (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaTerm -> Maybe a
go MetaTerm
t1
  go MetaTerm
_                  = Maybe a
forall a. Maybe a
Nothing

instance ToRuntimeTerm Int where
  toRuntimeTerm :: Int -> RuntimeTerm
toRuntimeTerm = Int -> RuntimeTerm
intToTerm

pp :: MT.ToMetaTerm a => a -> String
pp :: forall a. ToMetaTerm a => a -> String
pp = PPArgs -> a -> String
forall a. ToMetaTerm a => PPArgs -> a -> String
prettyPrint ([(Text, Text)]
-> [(Text, Text)] -> (MetaTerm -> Maybe Text) -> PPArgs
PPArgs []
                  [ (Text
"<", Text
"<")
                  , (Text
"+", Text
"+")
                  , (Text
"*", Text
"*")
                  , (Text
"∪", Text
"∪")
                  , (Text
"union", Text
"∪")
                  , (Text
"intersect", Text
"∩")
                  ] MetaTerm -> Maybe Text
showInt)
  where
    showInt :: MT.MetaTerm -> Maybe Text
    showInt :: MetaTerm -> Maybe Text
showInt MetaTerm
t = String -> Text
pack (String -> Text) -> (Int -> String) -> Int -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> Text) -> Maybe Int -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaTerm -> Maybe Int
forall a. ToMetaTerm a => a -> Maybe Int
termToInt MetaTerm
t

op :: GenParser Char st Op
op :: forall st. GenParser Char st Op
op = (String -> Op)
-> ParsecT String st Identity String
-> ParsecT String st Identity Op
forall a b.
(a -> b)
-> ParsecT String st Identity a -> ParsecT String st Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Op
Op (Text -> Op) -> (String -> Text) -> String -> Op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack) (ParsecT String st Identity Char
-> ParsecT String st Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT String st Identity Char
-> ParsecT String st Identity Char
-> ParsecT String st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'\''))

parens :: Stream s m Char => ParsecT s u m b -> ParsecT s u m b
parens :: forall s (m :: * -> *) u b.
Stream s m Char =>
ParsecT s u m b -> ParsecT s u m b
parens ParsecT s u m b
p = do
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'('
  b
r <- ParsecT s u m b
p
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')'
  b -> ParsecT s u m b
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return b
r

term :: Parsec String u RuntimeTerm
term :: forall u. Parsec String u RuntimeTerm
term = GenParser Char u RuntimeTerm -> GenParser Char u RuntimeTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char u RuntimeTerm
forall u. Parsec String u RuntimeTerm
infixTerm GenParser Char u RuntimeTerm
-> GenParser Char u RuntimeTerm -> GenParser Char u RuntimeTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char u RuntimeTerm
forall u. Parsec String u RuntimeTerm
nonInfixTerm
  where

    nonInfixTerm :: ParsecT String u Identity RuntimeTerm
nonInfixTerm = ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall s (m :: * -> *) u b.
Stream s m Char =>
ParsecT s u m b -> ParsecT s u m b
parens ParsecT String u Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
term) ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try ParsecT String u Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
appTerm ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try ParsecT String u Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
numberTerm ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
-> ParsecT String u Identity RuntimeTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
nullTerm

    numberTerm :: ParsecT String u Identity RuntimeTerm
numberTerm = do
      Char
d1 <- ParsecT String u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
      String
n <- ParsecT String u Identity Char -> ParsecT String u Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
      RuntimeTerm -> ParsecT String u Identity RuntimeTerm
forall a. a -> ParsecT String u Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RuntimeTerm -> ParsecT String u Identity RuntimeTerm)
-> RuntimeTerm -> ParsecT String u Identity RuntimeTerm
forall a b. (a -> b) -> a -> b
$ Int -> RuntimeTerm
intToTerm (String -> Int
forall a. Read a => String -> a
read (Char
d1 Char -> String -> String
forall a. a -> [a] -> [a]
: String
n))

    infixOp :: ParsecT String u Identity String
infixOp =
          ParsecT String u Identity String
-> ParsecT String u Identity String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"+")
      ParsecT String u Identity String
-> ParsecT String u Identity String
-> ParsecT String u Identity String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String u Identity String
-> ParsecT String u Identity String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"<")
      ParsecT String u Identity String
-> ParsecT String u Identity String
-> ParsecT String u Identity String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT String u Identity String
-> ParsecT String u Identity String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"\\/") ParsecT String u Identity String
-> ParsecT String u Identity String
-> ParsecT String u Identity String
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> ParsecT String u Identity String
forall a. a -> ParsecT String u Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"∪")
      ParsecT String u Identity String
-> ParsecT String u Identity String
-> ParsecT String u Identity String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"*"

    infixTerm :: ParsecT String u Identity RuntimeTerm
infixTerm = do
      RuntimeTerm
t1 <- ParsecT String u Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
nonInfixTerm
      ()
_  <- ParsecT String u Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      String
top <- ParsecT String u Identity String
forall {u}. ParsecT String u Identity String
infixOp
      ()
_  <- ParsecT String u Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      RuntimeTerm
t2 <- ParsecT String u Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
nonInfixTerm
      RuntimeTerm -> ParsecT String u Identity RuntimeTerm
forall a. a -> ParsecT String u Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RuntimeTerm -> ParsecT String u Identity RuntimeTerm)
-> RuntimeTerm -> ParsecT String u Identity RuntimeTerm
forall a b. (a -> b) -> a -> b
$ Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op (String -> Text
pack String
top)) [RuntimeTerm
t1, RuntimeTerm
t2]

    nullTerm :: ParsecT String st Identity RuntimeTerm
nullTerm = do
      Op
o <- GenParser Char st Op
forall st. GenParser Char st Op
op
      RuntimeTerm -> ParsecT String st Identity RuntimeTerm
forall a. a -> ParsecT String st Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RuntimeTerm -> ParsecT String st Identity RuntimeTerm)
-> RuntimeTerm -> ParsecT String st Identity RuntimeTerm
forall a b. (a -> b) -> a -> b
$ Op -> [RuntimeTerm] -> RuntimeTerm
App Op
o []

    appTerm :: ParsecT String st Identity RuntimeTerm
appTerm = do
      Op
o    <- GenParser Char st Op
forall st. GenParser Char st Op
op
      [RuntimeTerm]
trms <- ParsecT String st Identity [RuntimeTerm]
-> ParsecT String st Identity [RuntimeTerm]
forall s (m :: * -> *) u b.
Stream s m Char =>
ParsecT s u m b -> ParsecT s u m b
parens (ParsecT String st Identity [RuntimeTerm]
 -> ParsecT String st Identity [RuntimeTerm])
-> ParsecT String st Identity [RuntimeTerm]
-> ParsecT String st Identity [RuntimeTerm]
forall a b. (a -> b) -> a -> b
$ ParsecT String st Identity RuntimeTerm
-> ParsecT String st Identity ()
-> ParsecT String st Identity [RuntimeTerm]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT String st Identity RuntimeTerm
forall u. Parsec String u RuntimeTerm
term (Char -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
',' ParsecT String st Identity Char
-> ParsecT String st Identity () -> ParsecT String st Identity ()
forall a b.
ParsecT String st Identity a
-> ParsecT String st Identity b -> ParsecT String st Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces)
      RuntimeTerm -> ParsecT String st Identity RuntimeTerm
forall a. a -> ParsecT String st Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RuntimeTerm -> ParsecT String st Identity RuntimeTerm)
-> RuntimeTerm -> ParsecT String st Identity RuntimeTerm
forall a b. (a -> b) -> a -> b
$ Op -> [RuntimeTerm] -> RuntimeTerm
App Op
o [RuntimeTerm]
trms


parseTerm :: String -> RuntimeTerm
parseTerm :: String -> RuntimeTerm
parseTerm String
str =
  case Parsec String () RuntimeTerm
-> String -> String -> Either ParseError RuntimeTerm
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () RuntimeTerm
forall u. Parsec String u RuntimeTerm
term String
"" String
str of
    Left ParseError
err -> String -> RuntimeTerm
forall a. HasCallStack => String -> a
error (ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
    Right RuntimeTerm
t  -> RuntimeTerm
t

instance IsString RuntimeTerm where
  fromString :: String -> RuntimeTerm
fromString = String -> RuntimeTerm
parseTerm