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

Add tests for morphism parser for exponential

parent d4ec4bfa
......@@ -187,6 +187,32 @@ parseMorphismPointSpec = describe "parseMorphismPoint" $ do
morphp (mkPoly [[Const (v ["a"])]]) "x: a" `shouldParse`
encoding [(1, mkVal 0 [ConstValue 0])] []
it "parses an exponential" $ do
morphp (mkPoly [[Exponential Variable (v ["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"])]])
`shouldFailOn` "x: {a: x}"
it "fails to parse an exponential that isn't uniquely defined" $ do
morphp (mkPoly [[Exponential Variable (v ["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]])
"x: inj0 {a: x, b: y}\ny: inj1 y"
`shouldParse`
(encoding
[ (1, mkVal 0 [ExponentialValue (v [(), ()])])
, (1, mkVal 1 [IdValue ()])
]
[ (0, (1, (0, 0)), 0)
, (0, (1, (0, 1)), 1)
, (1, (1, (0, 0)), 1)
])
refineSpec :: Spec
refineSpec = describe "refining" $ do
let morphp fexpr input = snd <$> parseMorphisms (Functor 1 fexpr) "" input
......
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