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

op :: GenParser Char st Op
op :: forall st. GenParser Char st Op
op = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Op
Op forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack) (forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> 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
_ <- 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
_ <- forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')'
  forall (m :: * -> *) a. Monad m => a -> m a
return b
r

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

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

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

    infixOp :: ParsecT String u Identity String
infixOp =
          forall tok st a. GenParser tok st a -> GenParser tok st a
try (forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"+")
      forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> forall tok st a. GenParser tok st a -> GenParser tok st a
try (forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"<")
      forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (forall tok st a. GenParser tok st a -> GenParser tok st a
try (forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"\\/") forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return String
"∪")
      forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> 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 <- forall u. Parsec String u RuntimeTerm
nonInfixTerm
      ()
_  <- forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      String
top <- forall {u}. ParsecT String u Identity String
infixOp
      ()
_  <- forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      RuntimeTerm
t2 <- forall u. Parsec String u RuntimeTerm
nonInfixTerm
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall st. GenParser Char st Op
op
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> [RuntimeTerm] -> RuntimeTerm
App Op
o []

    appTerm :: ParsecT String st Identity RuntimeTerm
appTerm = do
      Op
o    <- forall st. GenParser Char st Op
op
      [RuntimeTerm]
trms <- forall s (m :: * -> *) u b.
Stream s m Char =>
ParsecT s u m b -> ParsecT s u m b
parens forall a b. (a -> b) -> a -> b
$ 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 forall u. Parsec String u RuntimeTerm
term (forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
',' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces)
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse forall u. Parsec String u RuntimeTerm
term String
"" String
str of
    Left ParseError
err -> forall a. HasCallStack => String -> a
error (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