Commit 26dd5fe4 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel
Browse files

Allow to use finite integer sets as exponent

Parses functor expressions of the form `X^2` with corresponding
morphisms `{0: x, 1: y}`.

The latter should in theory also be writable as a product `(x,y)`, but
that would lead to ambiguity with the product parser, so currently
you'd have to use the functor `XxX` instead of `X^2` to get that
morphism syntax.
parent 4c477911
......@@ -13,6 +13,7 @@ module MA.Functors.Polynomial
, Product(..)
, Factor(..)
, ConstSet(..)
, Exponent(..)
, SumValue(..)
, ProductValue(..)
, FactorValue(..)
......@@ -59,10 +60,15 @@ data ConstSet
| ExplicitSet (Vector Text)
deriving (Show, Eq)
data Exponent
= FiniteNatExp Int
| ExplicitExp (Vector Text)
deriving (Show, Eq)
data Factor a
= Const ConstSet
| Identity a
| Exponential a (Vector Text)
| Exponential a Exponent
deriving (Functor, Foldable, Traversable)
$(deriveEq1 ''Factor)
......@@ -107,11 +113,12 @@ parseConstExpr =
parseIdOrExp :: MonadParser m => m a -> m (Factor a)
parseIdOrExp inner = do
x <- inner
(Exponential x <$> (try (L.symbol "^") *> parseExponent))
(Exponential x <$> (try (L.symbol "^") *>
(parseExplicitExp <|> parseFiniteNatExp)))
<|> (return (Identity x))
parseExponent :: MonadParser m => m (Vector Text)
parseExponent = L.braces $ do
parseExplicitExp :: MonadParser m => m Exponent
parseExplicitExp = L.braces $ do
names <- (V.modify V.sort . V.fromList) <$> L.name `sepBy` L.comma
let iter (unique :: Bool, last :: Maybe Text) (current :: Text) =
let sameAsLast = last == Just current
......@@ -121,7 +128,10 @@ parseExponent = L.braces $ do
unless allUnique $
fail "exponential: domain must be uniquely defined"
return names
return (ExplicitExp names)
parseFiniteNatExp :: MonadParser m => m Exponent
parseFiniteNatExp = FiniteNatExp <$> L.decimal
-- Index into coproduct and corresponding product value
data SumValue a = SumValue Int (ProductValue a)
......@@ -243,18 +253,37 @@ parseFactor (Const (FiniteNatSet n)) = do
parseFactor (Identity inner) = do
successor <- inner
return (IdValue (), Just [(successor, 0)])
parseFactor (Exponential inner names) = L.braces $ do
successors <- ((,) <$> someName names <*> (L.colon *> inner)) `sepBy` L.comma
parseFactor (Exponential inner exp) = L.braces $ do
successors <- ((,) <$> parseExpValue exp
<*> (L.colon *> inner))
`sepBy` L.comma
let allIdxUsedOnce = [0..length names-1] == sort (map fst successors)
let allIdxUsedOnce = (allExpValues exp) == sort (map fst successors)
unless allIdxUsedOnce $
fail ("exponential: map must be well-defined on " ++ show names)
fail ("exponential: map must be well-defined on " ++ showExp exp)
return ( ExponentialValue (V.replicate (length successors) ())
, Just (map swap successors)
)
parseExpValue :: MonadParser m => Exponent -> m Int
parseExpValue (ExplicitExp names) = someName names
parseExpValue (FiniteNatExp n) = do
x <- L.decimal
unless (x < n) $ -- L.decimal returns only positive ints
fail ("Value " ++ show x ++
"is out of bounds. (must be between 0 and " ++ show n ++ ")")
return x
allExpValues :: Exponent -> [Int]
allExpValues (ExplicitExp names) = [0..length names-1]
allExpValues (FiniteNatExp n) = [0..n-1]
showExp :: Exponent -> String
showExp (ExplicitExp names) = show names
showExp (FiniteNatExp n) = "{0.." ++ show n ++ "}"
someName :: MonadParser m => Vector Text -> m Int
someName v =
(V.ifoldr (\i new old -> (L.symbol new *> pure i) <|> old) empty v)
......
......@@ -103,24 +103,24 @@ functorExpressionSpec = describe "functorExpression" $ do
it "parses an exponential" $ do
p "X^{a,b}"
`shouldParse` (Functor 1 (mkPoly [[Exponential Variable (v ["a", "b"])]]))
`shouldParse` (Functor 1 (mkPoly [[e Variable ["a", "b"]]]))
it "parses an exponential under a product" $ do
p "X^{a} x X" `shouldParse`
(Functor 1 (mkPoly [[Exponential Variable (v ["a"]), ident]]))
(Functor 1 (mkPoly [[e Variable ["a"], ident]]))
p "XxX^{a}" `shouldParse`
(Functor 1 (mkPoly [[ident, Exponential Variable (v ["a"])]]))
(Functor 1 (mkPoly [[ident, e Variable ["a"]]]))
it "parses an exponential under a coproduct" $ do
p "X^{a} + X" `shouldParse`
(Functor 1 (mkPoly [[Exponential Variable (v ["a"])], [ident]]))
(Functor 1 (mkPoly [[e Variable ["a"]], [ident]]))
p "X + X^{a}" `shouldParse`
(Functor 1 (mkPoly [[ident], [Exponential Variable (v ["a"])]]))
(Functor 1 (mkPoly [[ident], [e Variable ["a"]]]))
it "parses a deply nested exponential" $ do
p "X^{a}xX + X" `shouldParse`
(Functor 1 (mkPoly [[Exponential Variable (v ["a"]), ident], [ident]]))
(Functor 1 (mkPoly [[e Variable ["a"], ident], [ident]]))
it "errors if exponential has non-uniquely defined domain" $
p `shouldFailOn` "X^{a, a}"
......@@ -147,6 +147,15 @@ functorExpressionSpec = describe "functorExpression" $ do
p "55" `shouldParse` (Functor 1 (mkPoly [[Const (FiniteNatSet 55)]]))
p `shouldFailOn` "-2"
it "allows to use explicit sets of a certain size as exponents" $ do
p "X^2" `shouldParse`
(Functor 1 (mkPoly [[Exponential Variable (FiniteNatExp 2)]]))
p "X^100" `shouldParse`
(Functor 1 (mkPoly [[Exponential Variable (FiniteNatExp 100)]]))
it "disallows negative exponents" $ do
p `shouldFailOn` "X^-1"
data SomeFunctor a where
SomeFunctor :: (Eq1 f, Typeable f, Show1 f) => f a -> SomeFunctor a
......@@ -176,6 +185,9 @@ prefixParser = prefix (L.symbol "P" >> return PrefixFunctor)
c :: [Text] -> Factor a
c = Const . ExplicitSet . V.fromList
e :: a -> [Text] -> Factor a
e inner = Exponential inner . ExplicitExp . V.fromList
parseMorphismPointSpec :: Spec
parseMorphismPointSpec = describe "parseMorphismPoint" $ do
let morphp fexpr input = snd <$> parseMorphisms (Functor 1 fexpr) "" input
......@@ -237,20 +249,20 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
encoding [(1, mkVal 0 [ConstValue 0])] []
it "parses an exponential" $ do
morphp (mkPoly [[Exponential Variable (v ["a"])]]) "x: {a: x}"
morphp (mkPoly [[e Variable ["a"]]]) "x: {a: x}"
`shouldParse`
encoding [(1, mkVal 0 [ExponentialValue (v [()])])] [(0, (1, (0, 0)), 0)]
it "fails to parse an exponential that isn't totally defined" $ do
morphp (mkPoly [[Exponential Variable (v ["a", "b"])]])
morphp (mkPoly [[e Variable ["a", "b"]]])
`shouldFailOn` "x: {a: x}"
it "fails to parse an exponential that isn't uniquely defined" $ do
morphp (mkPoly [[Exponential Variable (v ["a", "b"])]])
morphp (mkPoly [[e Variable ["a", "b"]]])
`shouldFailOn` "x: {a: x, b: x, b: x}"
it "parses an exponential under a coproduct" $ do
morphp (mkPoly [[Exponential Variable (v ["a", "b"])], [Identity Variable]])
morphp (mkPoly [[e Variable ["a", "b"]], [Identity Variable]])
"x: inj0 {a: x, b: y}\ny: inj1 y"
`shouldParse`
(encoding
......@@ -290,6 +302,17 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
morphp f `shouldFailOn` "x: 4"
morphp f `shouldFailOn` "x: 10"
it "parses an exponential with FiniteNatExp" $ do
morphp (mkPoly [[Exponential Variable (FiniteNatExp 2)]]) "x: {0: x, 1: x}"
`shouldParse`
(encoding
[(1, mkVal 0 [ExponentialValue (v [(), ()])])]
[(0, (1, (0, 0)), 0), (0, (1, (0, 1)), 0)])
it "requires all values of the exponent set for FiniteNatExp" $ do
morphp (mkPoly [[Exponential Variable (FiniteNatExp 2)]])
`shouldFailOn` "x: {0: x}"
refineSpec :: Spec
refineSpec = describe "refining" $ do
let morphp fexpr input = snd <$> parseMorphisms (Functor 1 fexpr) "" input
......@@ -320,7 +343,7 @@ refineSpec = describe "refining" $ do
it "correctly distinguishes different exponential values" $ do
-- {a,b} + X^2
let f = mkPoly [[c ["A", "B"]], [Exponential Variable (v ["i", "j"])]]
let f = mkPoly [[c ["A", "B"]], [e Variable ["i", "j"]]]
let res = morphp f
"a: inj 0 (A)\n\
\b: inj 0 (B)\n\
......
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