-- | Parsing strings into properties.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, GADTs, TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
module QuickSpec.Internal.Parse where

import Control.Monad
import Data.Char
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Term hiding (char)
import QuickSpec.Internal.Type
import qualified Data.Label as Label
import Text.ParserCombinators.ReadP

class Parse fun a where
  parse :: ReadP fun -> ReadP a

instance Parse fun Var where
  parse :: ReadP fun -> ReadP Var
parse ReadP fun
_ = do
    Char
x <- (Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isUpper
    [Char]
xs <- (Char -> Bool) -> ReadP [Char]
munch Char -> Bool
isAlphaNum
    let name :: [Char]
name = Char
xforall a. a -> [a] -> [a]
:[Char]
xs
    -- Use Data.Label as an easy way to generate a variable number
    forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Int -> Var
V Type
typeVar (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Label a -> Int32
Label.labelNum (forall a. (Typeable a, Ord a) => a -> Label a
Label.label [Char]
name))))

instance (fun1 ~ fun, Apply (Term fun)) => Parse fun1 (Term fun) where
  parse :: ReadP fun1 -> ReadP (Term fun)
parse ReadP fun1
pfun =
    ReadP (Term fun1)
parseApp forall a. ReadP a -> ReadP a -> ReadP a
<++ ReadP (Term fun)
parseVar
    where
      parseVar :: ReadP (Term fun)
parseVar = forall f. Var -> Term f
Var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun1
pfun
      parseApp :: ReadP (Term fun1)
parseApp = do
        fun1
f <- ReadP fun1
pfun
        [Term fun1]
args <- ReadP [Term fun1]
parseArgs forall a. ReadP a -> ReadP a -> ReadP a
<++ forall (m :: * -> *) a. Monad m => a -> m a
return []
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Poly a -> a
unPoly (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Apply a => a -> a -> a
apply (forall a. Typed a => a -> Poly a
poly (forall f. f -> Term f
Fun fun1
f)) (forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> Poly a
poly [Term fun1]
args)))
      parseArgs :: ReadP [Term fun1]
parseArgs = forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
between (Char -> ReadP Char
char Char
'(') (Char -> ReadP Char
char Char
')') (forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy (forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun1
pfun) (Char -> ReadP Char
char Char
','))

instance (Parse fun a, Typed a) => Parse fun (Equation a) where
  parse :: ReadP fun -> ReadP (Equation a)
parse ReadP fun
pfun = do
    a
t <- forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun
pfun
    [Char] -> ReadP [Char]
string [Char]
"="
    a
u <- forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun
pfun
    -- Compute type unifier of t and u
    -- "maybe mzero return" injects Maybe into MonadPlus
    Poly Type
pt <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (m :: * -> *) a. MonadPlus m => m a
mzero forall (m :: * -> *) a. Monad m => a -> m a
return (Poly Type -> Poly Type -> Maybe (Poly Type)
polyMgu (forall a. Typed a => a -> Poly a
poly (forall a. Typed a => a -> Type
typ a
t)) (forall a. Typed a => a -> Poly a
poly (forall a. Typed a => a -> Type
typ a
u)))
    a
t <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (m :: * -> *) a. MonadPlus m => m a
mzero forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => Type -> a -> Maybe a
cast (forall a. Poly a -> a
unPoly Poly Type
pt) a
t)
    a
u <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (m :: * -> *) a. MonadPlus m => m a
mzero forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => Type -> a -> Maybe a
cast (forall a. Poly a -> a
unPoly Poly Type
pt) a
u)
    forall (m :: * -> *) a. Monad m => a -> m a
return (a
t forall a. a -> a -> Equation a
:=: a
u)

instance (Parse fun a, Typed a) => Parse fun (Prop a) where
  parse :: ReadP fun -> ReadP (Prop a)
parse ReadP fun
pfun = do
    [Equation a]
lhs <- forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy (forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun
pfun) ([Char] -> ReadP [Char]
string [Char]
"&")
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Equation a]
lhs) (forall (f :: * -> *) a. Functor f => f a -> f ()
void ([Char] -> ReadP [Char]
string [Char]
"=>"))
    Equation a
rhs <- forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun
pfun
    forall (m :: * -> *) a. Monad m => a -> m a
return ([Equation a]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: Equation a
rhs)

parseProp :: (Parse fun a, Pretty a) => ReadP fun -> String -> a
parseProp :: forall fun a. (Parse fun a, Pretty a) => ReadP fun -> [Char] -> a
parseProp ReadP fun
pfun [Char]
xs =
  case forall a. ReadP a -> ReadS a
readP_to_S (forall fun a. Parse fun a => ReadP fun -> ReadP a
parse ReadP fun
pfun forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
eof) (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace) [Char]
xs) of
    [(a
x, [])] -> a
x
    [(a, [Char])]
ps -> forall a. HasCallStack => [Char] -> a
error ([Char]
"parse': got result " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [(a, [Char])]
ps forall a. [a] -> [a] -> [a]
++ [Char]
" while parsing " forall a. [a] -> [a] -> [a]
++ [Char]
xs)