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

Implement morphism parser for exponentials

Adds a second `Int` component to `Label Polynomial` that specifies the
index into the exponential.
parent 68fc692e
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
......@@ -12,11 +13,14 @@ module MA.Functors.Polynomial
, FactorValue(..)
) where
import Data.Bifunctor
import Control.Monad
import Data.Bifunctor
import Data.List (sortBy)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe (catMaybes, maybeToList)
import Data.Maybe (fromMaybe)
import Data.Ord (comparing)
import Data.Tuple (swap)
import Data.Text (Text)
import Data.Vector (Vector)
......@@ -24,6 +28,7 @@ import qualified Data.Vector as V
import Text.Megaparsec
import Data.Eq.Deriving (deriveEq1)
import Text.Show.Deriving (deriveShow1)
import Lens.Micro
import MA.Coalgebra.Parser
import MA.Coalgebra.RefinementTypes
......@@ -44,6 +49,7 @@ newtype Product a = Product (NonEmpty (Factor a))
data Factor a
= Const (Vector Text)
| Identity a
| Exponential a (Vector Text)
deriving (Functor, Foldable, Traversable)
$(deriveEq1 ''Factor)
......@@ -91,6 +97,7 @@ data ProductValue a =
data FactorValue a
= ConstValue Int
| IdValue a
| ExponentialValue (Vector a)
deriving (Eq, Ord, Show, Functor)
......@@ -98,8 +105,7 @@ data Three = ToRest | ToCompound | ToSub
deriving (Show, Eq, Ord, Enum)
type instance H1 Polynomial = SumValue ()
type instance Label Polynomial = Int -- Index of edge product (independent of
-- toplevel-sum)
type instance Label Polynomial = (Int, Int)
type instance Weight Polynomial = SumValue Bool -- H2
type instance H3 Polynomial = SumValue Three
......@@ -142,33 +148,49 @@ parseSum (Sum summands) i = do
-- | Parse either a single factor without parens or a tuple.
parseProduct1 ::
MonadParser m => Product (m a) -> m (ProductValue (), [(a, Int)])
MonadParser m => Product (m a) -> m (ProductValue (), [(a, (Int, Int))])
parseProduct1 product@(Product (factor :| [])) =
let mkProduct = bimap (ProductValue . V.singleton) (maybeToList . fmap (,0))
let mkProduct f = f & _1 %~ (ProductValue . V.singleton)
& _2 %~ (_Just . each . _2 %~ (0,) <&> fromMaybe [])
in (mkProduct <$> parseFactor factor) <|> parseProduct product
parseProduct1 other = parseProduct other
parseProduct ::
MonadParser m => Product (m a) -> m (ProductValue (), [(a, Int)])
MonadParser m => Product (m a) -> m (ProductValue (), [(a, (Int, 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..]
labeledSuccessors =
zipWith
(\x i -> x & _Just . traversed . _2 %~ (i,) & fromMaybe [])
successors
[0..]
return ( ProductValue (V.fromList h1) , catMaybes labeledSuccessors)
return ( ProductValue (V.fromList h1) , concat labeledSuccessors)
----------- Factor parser
parseFactor :: MonadParser m => Factor (m a) -> m (FactorValue (), Maybe a)
parseFactor :: MonadParser m => Factor (m a) -> m (FactorValue (), Maybe [(a, Int)])
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)
return (IdValue (), Just [(successor, 0)])
parseFactor (Exponential inner names) = L.braces $ do
successors <- sortBy (comparing fst) <$> ((,) <$> someName names <*> (L.colon *> inner)) `sepBy` L.comma
let allIdxUsedOnce = [0..length names-1] == map fst successors
unless allIdxUsedOnce $
fail ("exponential: map must be well-defined on " ++ show names)
return ( ExponentialValue (V.replicate (length successors) ())
, Just (map swap successors)
)
someName :: MonadParser m => Vector Text -> m Int
someName v =
......@@ -187,11 +209,16 @@ instance RefinementInterface Polynomial where
val h3 = (fmap (== ToSub) h3, h3, fmap (== ToCompound) h3)
up :: ([Label Polynomial], Weight Polynomial) -> H3 Polynomial
up (labels, weight) = fmapIndex (\i bi -> bi +? (i `elem` labels)) weight
up (labels, weight) = fmapIndex (\i j bi -> bi +? ((i,j) `elem` labels)) weight
(+?) :: Bool -> Bool -> Three
(+?) a b = toEnum (fromEnum a + fromEnum b)
fmapIndex :: (Int -> a -> b) -> SumValue a -> SumValue b
fmapIndex :: forall a b. (Int -> Int -> a -> b) -> SumValue a -> SumValue b
fmapIndex f (SumValue s (ProductValue factors)) =
SumValue s (ProductValue (V.imap (fmap . f) factors))
SumValue s (ProductValue (V.imap fmapFactor factors))
where
fmapFactor :: Int -> FactorValue a -> FactorValue b
fmapFactor i (ExponentialValue as) = ExponentialValue (V.imap (f i) as)
fmapFactor i other = fmap (f i 0) other
......@@ -139,7 +139,7 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
it "parses the identity" $
morphp (mkPoly [[Identity Variable]]) "x: inj 0 (y)\ny: inj 0 (x)" `shouldParse`
encoding [(1, mkVal 0 [IdValue ()]), (1, mkVal 0 [IdValue ()])] [(0, (1, 0), 1), (1, (1, 0), 0)]
encoding [(1, mkVal 0 [IdValue ()]), (1, mkVal 0 [IdValue ()])] [(0, (1, (0, 0)), 1), (1, (1, (0,0)), 0)]
it "gives a useful error if the injection index is out of bounds" $ do
morphp (mkPoly [[Const (v ["a"])]]) `shouldFailOn `"x: inj 5 (a)"
......@@ -147,11 +147,11 @@ 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)), 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), (0, (1, (1, 0)), 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`
......@@ -163,13 +163,13 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
"x: inj 0 (y)\ny: inj 1 (a, x)" `shouldParse`
encoding
[(1, mkVal 0 [IdValue ()]), (1, mkVal 1 [ConstValue 0, IdValue ()])]
[(0, (1, 0), 1), (1, (1, 1), 0)]
[(0, (1, (0, 0)), 1), (1, (1, (1, 0)), 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)]
encoding [(1, mkVal 0 [IdValue (), IdValue ()])] [(0, (1, (0, 0)), 0), (0, (1, (1, 0)), 0)]
it "doesn't confuse a constant called inj and an injection" $ do
morphp (mkPoly [[Const (v ["injection"])]]) "x: injection" `shouldParse`
......
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