Commit 3a816652 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel
Browse files

polynomial functor: Allow to omit `inj` and parens when possible

Allows to write a morphism for the functor `{a}` as `x: a` instead of
`x: inj 0 (a)`
parent 39d563b8
......@@ -12,10 +12,11 @@ module MA.Functors.Polynomial
, FactorValue(..)
) where
import Data.Bifunctor
import Control.Monad
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe (catMaybes)
import Data.Maybe (catMaybes, maybeToList)
import Data.Text (Text)
import Data.Vector (Vector)
......@@ -103,48 +104,76 @@ type instance Weight Polynomial = SumValue Bool -- H2
type instance H3 Polynomial = SumValue Three
instance ParseMorphism Polynomial where
parseMorphismPoint (Polynomial expr) = parseSum expr
where
-- Coproducts
parseSum ::
MonadParser m => Sum (m a) -> m (SumValue (), [(a, Label Polynomial)])
parseSum (Sum summands) = do
void $ L.symbol "inj"
i <- L.decimal
when (i < 0 || i >= length summands) $
fail ("polynomial: injection " ++ show i ++ " is out of bounds")
(h1, successors) <- parseProduct (summands NonEmpty.!! i)
return (SumValue i h1, successors)
-- Products
parseProduct ::
MonadParser m => Product (m a) -> m (ProductValue (), [(a, Int)])
parseProduct (Product (f :| fs)) = L.parens $ do
factors <- (:)
<$> parseFactor f
<*> traverse (\x -> L.comma *> parseFactor x) fs
let (h1, successors) = unzip factors
labeledSuccessors = zipWith (\a i -> fmap (,i) a) successors [0..]
return ( ProductValue (V.fromList h1) , catMaybes labeledSuccessors)
-- Factors
parseFactor :: MonadParser m => Factor (m a) -> m (FactorValue (), Maybe a)
parseFactor (Const names) = do
h1 <- ConstValue <$> someName names
return (h1, Nothing) -- const has no successors
parseFactor (Identity inner) = do
successor <- inner
return (IdValue (), Just successor)
someName :: MonadParser m => Vector Text -> m Int
someName v =
(V.ifoldr (\i new old -> (L.symbol new *> pure i) <|> old) empty v)
<?> ("one of " ++ show v)
parseMorphismPoint (Polynomial expr) = parseSum1 expr
----------- Coproducts parser
-- | Parse either a single product or an injection into the coproduct, depending
-- on the number of co-factors.
parseSum1 ::
MonadParser m => Sum (m a) -> m (SumValue (), [(a, Label Polynomial)])
parseSum1 sum@(Sum (product :| [])) = do
-- only a single summand => parse product directly
-- We first try to parse 'inj i' and delegate to the product parser only if
-- that fails.
-- This avoids strange situations where a constant calle 'inj' exists and the
-- input starts with inj.
(try parseSumPrefix >>= parseSum sum) <|>
(first (SumValue 0) <$> parseProduct1 product)
parseSum1 other = parseSumPrefix >>= parseSum other -- otherwise, require 'inj'
-- | parses @inj i@ where @i@ is a decimal integer
parseSumPrefix :: MonadParser m => m Int
parseSumPrefix = L.symbol "inj" *> L.decimal
-- | Parse an injection into the coproduct with the syntax 'inj i _'
parseSum ::
MonadParser m => Sum (m a) -> Int -> m (SumValue (), [(a, Label Polynomial)])
parseSum (Sum summands) i = do
when (i < 0 || i >= length summands) $
fail ("polynomial: injection " ++ show i ++ " is out of bounds")
(h1, successors) <- parseProduct1 (summands NonEmpty.!! i)
return (SumValue i h1, successors)
----------- Products parser
-- | Parse either a single factor without parens or a tuple.
parseProduct1 ::
MonadParser m => Product (m a) -> m (ProductValue (), [(a, Int)])
parseProduct1 product@(Product (factor :| [])) =
let mkProduct = bimap (ProductValue . V.singleton) (maybeToList . fmap (,0))
in (mkProduct <$> parseFactor factor) <|> parseProduct product
parseProduct1 other = parseProduct other
parseProduct ::
MonadParser m => Product (m a) -> m (ProductValue (), [(a, Int)])
parseProduct (Product (f :| fs)) = L.parens $ do
factors <- (:)
<$> parseFactor f
<*> traverse (\x -> L.comma *> parseFactor x) fs
let (h1, successors) = unzip factors
labeledSuccessors = zipWith (\a i -> fmap (,i) a) successors [0..]
return ( ProductValue (V.fromList h1) , catMaybes labeledSuccessors)
----------- Factor parser
parseFactor :: MonadParser m => Factor (m a) -> m (FactorValue (), Maybe a)
parseFactor (Const names) = do
h1 <- ConstValue <$> someName names
return (h1, Nothing) -- const has no successors
parseFactor (Identity inner) = do
successor <- inner
return (IdValue (), Just successor)
someName :: MonadParser m => Vector Text -> m Int
someName v =
(V.ifoldr (\i new old -> (L.symbol new *> pure i) <|> old) empty v)
<?> ("one of " ++ show v)
instance RefinementInterface Polynomial where
......
......@@ -147,15 +147,15 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
it "parses a product of a constant and an X" $
morphp (mkPoly [[Const (v ["a"]), Identity Variable]]) "x: inj 0 (a, x)" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0, IdValue ()])] [(0, (1, 1), 0)]
encoding [(1, mkVal 0 [ConstValue 0, IdValue ()])] [(0, (1, 1), 0)]
it "parses a product of two elements" $
morphp (mkPoly [[Identity Variable, Identity Variable]]) "x: inj 0 (x, x)" `shouldParse`
encoding [(1, mkVal 0 [IdValue (), IdValue ()])] [(0, (1, 0), 0), (0, (1, 1), 0)]
encoding [(1, mkVal 0 [IdValue (), IdValue ()])] [(0, (1, 0), 0), (0, (1, 1), 0)]
it "parses a sum of two constants" $
morphp (mkPoly [[Const (v ["a"])], [Const (v ["b"])]]) "x: inj 0 (a)\ny: inj 1 (b)" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0]), (1, mkVal 1 [ConstValue 0])] []
encoding [(1, mkVal 0 [ConstValue 0]), (1, mkVal 1 [ConstValue 0])] []
it "parses X+(AxX)" $
morphp
......@@ -165,6 +165,27 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
[(1, mkVal 0 [IdValue ()]), (1, mkVal 1 [ConstValue 0, IdValue ()])]
[(0, (1, 0), 1), (1, (1, 1), 0)]
it "allows to omit 'inj' for co-products with only one factor" $ do
morphp (mkPoly [[Const (v ["a"])]]) "x: (a)" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
morphp (mkPoly [[Identity Variable, Identity Variable]]) "x: (x, x)" `shouldParse`
encoding [(1, mkVal 0 [IdValue (), IdValue ()])] [(0, (1, 0), 0), (0, (1, 1), 0)]
it "doesn't confuse a constant called inj and an injection" $ do
morphp (mkPoly [[Const (v ["injection"])]]) "x: injection" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
morphp (mkPoly [[Const (v ["inj"])]]) "x: inj" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
morphp (mkPoly [[Const (v ["inj"])]]) "x: inj 0 inj" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
it "allows to omit parens for products with only one factor" $ do
morphp (mkPoly [[Const (v ["a"])], [Const (v ["b"])]]) "x: inj 0 a" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
it "allows to omit both 'inj' and parens" $ do
morphp (mkPoly [[Const (v ["a"])]]) "x: a" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
refineSpec :: Spec
refineSpec = describe "refining" $ do
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment