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

Allow to use bounded naturals as set for constants

This allows to use `1`, `55`, etc as constant sets.
parent 5b50f0a5
......@@ -55,6 +55,7 @@ newtype Product a = Product (NonEmpty (Factor a))
data ConstSet
= IntSet
| NatSet
| FiniteNatSet Int
| ExplicitSet (Vector Text)
deriving (Show, Eq)
......@@ -100,6 +101,7 @@ parseConstExpr :: MonadParser m => m ConstSet
parseConstExpr =
((L.symbol "Z" <|> L.symbol "ℤ") >> return IntSet) <|>
((L.symbol "N" <|> L.symbol "ℕ") >> return NatSet) <|>
(FiniteNatSet <$> L.decimal) <|>
((ExplicitSet . V.fromList) <$> (L.braces (L.name `sepBy` L.comma)))
parseIdOrExp :: MonadParser m => m a -> m (Factor a)
......@@ -228,10 +230,16 @@ parseFactor (Const (ExplicitSet names)) = do
return (h1, Nothing) -- const has no successors
parseFactor (Const IntSet) = do
x <- L.signed L.decimal
return (ConstValue x, Nothing) -- same here
return (ConstValue x, Nothing)
parseFactor (Const NatSet) = do
x <- L.decimal
return (ConstValue x, Nothing) -- and here
return (ConstValue x, Nothing)
parseFactor (Const (FiniteNatSet n)) = do
x <- L.decimal
unless (x < n) $
fail ("out of range constant: " ++ show x ++
"(must be between 0 and " ++ show n ++ ")")
return (ConstValue x, Nothing)
parseFactor (Identity inner) = do
successor <- inner
return (IdValue (), Just [(successor, 0)])
......
......@@ -142,6 +142,11 @@ functorExpressionSpec = describe "functorExpression" $ do
p "N" `shouldParse` (Functor 1 (mkPoly [[Const NatSet]]))
p "ℕ" `shouldParse` (Functor 1 (mkPoly [[Const NatSet]]))
it "allows to use explicit sets of a certain size as constants" $ do
p "2" `shouldParse` (Functor 1 (mkPoly [[Const (FiniteNatSet 2)]]))
p "55" `shouldParse` (Functor 1 (mkPoly [[Const (FiniteNatSet 55)]]))
p `shouldFailOn` "-2"
data SomeFunctor a where
SomeFunctor :: (Eq1 f, Typeable f, Show1 f) => f a -> SomeFunctor a
......@@ -265,13 +270,25 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
morphp (mkPoly [[Const IntSet]]) "x: -3\ny:-77" `shouldParse`
(encoding [(1, mkVal 0 [ConstValue (-3)]), (1, mkVal 0 [ConstValue (-77)])] [])
it "allows positive numbers as constants for naturls set" $ do
it "allows positive numbers as constants for naturals set" $ do
morphp (mkPoly [[Const NatSet]]) "x: 5\ny:30" `shouldParse`
(encoding [(1, mkVal 0 [ConstValue 5]), (1, mkVal 0 [ConstValue 30])] [])
it "doesn't allow negative numbers as constants for naturls set" $ do
it "doesn't allow negative numbers as constants for naturals set" $ do
morphp (mkPoly [[Const NatSet]]) `shouldFailOn` "x: -35\ny:-77"
it "allows numbers in the correct range as constants for FiniteNatSet" $ do
let f = mkPoly [[Const (FiniteNatSet 4)]]
morphp f "x: 0" `shouldParse` (encoding [(1, mkVal 0 [ConstValue 0])] [])
morphp f `shouldSucceedOn` "x: 1"
morphp f `shouldSucceedOn` "x: 2"
morphp f `shouldSucceedOn` "x: 3"
it "disallows numbers outside bounds for FiniteNatSet" $ do
let f = mkPoly [[Const (FiniteNatSet 4)]]
morphp f `shouldFailOn` "x: -1"
morphp f `shouldFailOn` "x: 4"
morphp f `shouldFailOn` "x: 10"
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