{-# 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