packages feed

Agda-2.3.2.2: src/prototyping/mixfix/old/MixFix.hs

module Main where

import Control.Monad
import Control.Monad.Error
import Data.Char
import Data.List
import qualified Data.Set as Set

import Utils.ReadP
import Utils.List

data Raw = Name String
	 | RawApp [Raw]
	 | Paren Raw
	 | Braces Raw
	 | RawLit Int
	 | AppR Raw (Arg Raw)
	 | OpR String [Raw]
    deriving (Show, Eq)

data Exp = Op String [Exp]  -- operator application
	 | App Exp (Arg Exp)
	 | Lit Int
	 | Id String

data Hiding = Hidden | NotHidden
    deriving (Eq)

data Arg e = Arg Hiding e
    deriving (Eq)

instance Show a => Show (Arg a) where
    showsPrec p (Arg Hidden e)	  = showString "{" . shows e . showString "}"
    showsPrec p (Arg NotHidden e) = showsPrec p e

instance Show Exp where
    showsPrec p e = case e of
	Id x	    -> showString x
	Lit n	    -> shows n
	App e1 e2   -> showParen (p > 1) $
	    showsPrec 1 e1 . showString " " . showsPrec 2 e2
	Op op es
	    | isPrefix op -> showParen (p > 0) $ merge ss' es'
	    | otherwise	  -> showParen (p > 0) $ merge es' ss'
	    where
		ss' = map showString $ wordsBy ('_'==) op
		es' = map (showsPrec 1) es

		isPrefix ('_':s) = False
		isPrefix _	 = True

		merge xs ys = foldr (.) id $ intersperse (showString " ") $ merge' xs ys

		merge' (x:xs) (y:ys) = x : y : merge' xs ys
		merge' []      ys    = ys
		merge' xs      []    = xs

type P = ReadP Raw
type Parser = P Raw

-- Parsing raw terms (for testing)
parseRaw :: String -> Raw
parseRaw s = case parse p0 s of
    [e]	-> e
    []	-> error "parseRaw: no parse"
    es	-> error $ "parseRaw: ambiguous parse: " ++ show es
    where
	p0 = RawApp <$> sepBy1 p1 (many1 $ satisfy isSpace)
	p1 = choice [ do char '('; x <- p0; char ')'; return $ Paren x
		    , do char '{'; x <- p0; char '}'; return $ Braces x
		    , RawLit . read <$> many1 (satisfy isDigit)
		    , Name <$> ((:) <$> satisfy idStart <*> many (satisfy idChar))
		    ]
	idChar  c = not $ isSpace c || elem c "(){}"
	idStart c = idChar c && not (isDigit c)

infixl 8 <$>, <*>
f <$> m = liftM f m
f <*> m = ap f m

-- General combinators
recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok a
recursive f = p0
    where
	fs = f p0
	p0 = foldr ( $ ) p0 fs
	choice' = foldr1 (++++)
	f ++++ g = \p -> f p +++ g p

-- Specific combinators
name :: String -> P String
name s = unName <$> char (Name s)
    where
	unName (Name s) = s

binop :: Parser -> P (Raw -> Raw -> Raw)
binop opP = do
    OpR op es <- opP
    return $ \x y -> OpR ("_" ++ op ++ "_") ([x] ++ es ++ [y])

preop :: Parser -> P (Raw -> Raw)
preop opP = do
    OpR op es <- opP
    return $ \x -> OpR (op ++ "_") (es ++ [x])

postop :: Parser -> P (Raw -> Raw)
postop opP = do
    OpR op es <- opP
    return $ \x -> OpR ("_" ++ op) ([x] ++ es)

opP :: Parser -> [String] -> Parser
opP p [] = fail "empty mixfix operator"
opP p ss = OpR s <$> mix ss
    where
	s = concat $ intersperse "_" ss
	mix [s]	   = do name s; return []
	mix (s:ss) = do
	    name s
	    e <- p
	    es <- mix ss
	    return $ e : es

prefixP :: Parser -> Parser -> Parser
prefixP op p = do
    fs <- many (preop op)
    e  <- p
    return $ foldr ( $ ) e fs

postfixP :: Parser -> Parser -> Parser
postfixP op p = do
    e <- p
    fs <- many (postop op)
    return $ foldl (flip ( $ )) e fs

infixlP op p = chainl1 p (binop op)
infixrP op p = chainr1 p (binop op)
infixP  op p = do
    e <- p
    f <- restP
    return $ f e
    where
	restP = return id +++ do
	    f <- binop op
	    e <- p
	    return $ flip f e

nonfixP op p = op +++ p

appP :: Parser -> Parser
appP p = do
    h  <- p
    es <- many (nothidden +++ hidden)
    return $ foldl AppR h es
    where
	isHidden (Braces _) = True
	isHidden _	    = False

	nothidden = Arg NotHidden <$> do
	    e <- p
	    case e of
		Braces _ -> pfail
		_	 -> return e

	hidden = do
	    Braces e <- satisfy isHidden
	    return $ Arg Hidden e

atomP :: [String] -> Parser
atomP xs = do
    t <- get
    case t of
	Name x | not $ Set.member x xs'
	    -> pfail
	_   -> return t
    where
	xs' = Set.fromList xs

-- Running a parser
parseExp :: Parser -> Raw -> Either String Exp
parseExp p r = case r of
    Name s	-> return $ Id s
    RawApp es	-> parseExp p =<< parseApp p es
    Paren e	-> parseExp p e
    Braces e	-> fail $ "bad hidden app"
    RawLit n	-> return $ Lit n
    AppR e1 (Arg h e2) -> do
	e1' <- parseExp p e1
	e2' <- parseExp p e2
	return $ App e1' (Arg h e2')
    OpR x es -> Op x <$> mapM (parseExp p) es

parseApp :: Parser -> [Raw] -> Either String Raw
parseApp p es = case parse p es of
    [e]	-> return e
    []	-> fail "no parse"
    es	-> fail $ "ambiguous parse: " ++ show es

-- Building the parser
data Operator = Prefix  { opPrecedence :: Int, opName :: [String] }
	      | Postfix { opPrecedence :: Int, opName :: [String] }
	      | InfixL  { opPrecedence :: Int, opName :: [String] }
	      | InfixR  { opPrecedence :: Int, opName :: [String] }
	      | Infix   { opPrecedence :: Int, opName :: [String] }
	      | Nonfix  { opName :: [String] }
    deriving Show

buildParser :: [String] -> [Operator] -> Parser
buildParser local ops =
    recursive $ \p ->
	let op = opP p in
	map (mkP op) (order fixops)
	++ [ appP ]
	++ map (nonfixP . op . opName) nonops
	++ [ const $ atomP local ]
    where

	(nonops, fixops) = partition nonfix ops

	isprefix (Prefix _ _)	= True
	isprefix _		= False

	ispostfix (Postfix _ _) = True
	ispostfix _		= False

	isinfixl (InfixL _ _)	= True
	isinfixl _		= False

	isinfixr (InfixR _ _)	= True
	isinfixr _		= False

	isinfix (Infix _ _)	= True
	isinfix _		= False

	nonfix (Nonfix _)	= True
	nonfix _		= False

	on f g x y = f (g x) (g y)

	order = groupBy ((==) `on` opPrecedence) . sortBy (compare `on` opPrecedence)

	mkP op ops = case concat [infx, inlfx, inrfx, prefx, postfx] of
		[]	-> id
		[(_,f)] -> f
		xs	-> error $ "cannot mix " ++ show (map fst xs)
	    where
		choice' = foldr1 (++++)
		f ++++ g = \p -> f p +++ g p
		inlfx	= fixP infixlP  isinfixl
		inrfx	= fixP infixrP  isinfixr
		infx	= fixP infixP   isinfix
		prefx	= fixP prefixP  isprefix
		postfx	= fixP postfixP ispostfix

		fixP f g = case filter g ops of
			    []	-> []
			    os	-> [ (os, f $ choice $ map (op . opName) os) ]

-- Tests
arithP :: Parser
arithP = buildParser xs ops
    where
	xs = map (:[]) ['a'..'z']
	ops =
	    [ InfixL  20 ["+"]
	    , InfixL  30 ["*"]
	    , InfixR  40 ["^"]
	    , Postfix 35 ["!"]
	    , InfixR  15 [":"]
	    , InfixR  18 ["/\\"]
	    , InfixR  16 ["\\/"]
	    ]

testP :: Parser
testP = buildParser xs ops
    where
	xs = map (:[]) ['a'..'z']
	ops = [ InfixL n ["+" ++ show n] | n <- [0..20] ]

arithP' :: Parser
arithP' = recursive $ \p ->
    let op = opP p in
    [ id ++++ infixrP (op [":"])
    , id ++++ infixrP (op ["\\/"])
    , id ++++ infixrP (op ["/\\"])
    , id ++++ infixlP (op ["+"])
    , id ++++ infixlP (op ["*"])
    , id ++++ postfixP (op ["!"])
    , id ++++ infixrP (op ["^"])
    , appP
    , const $ atomP $ map (:[]) ['a'..'z']
    ]
    where
	f ++++ g = \p -> f p +++ g p

main = print $ parseExp testP $ parseRaw "1 +0 2 +0 3"