Simplify `Inject`/`Interpret` for 1-field records (#1315)
* Simplify `Inject`/`Interpret` for 1-field records Fixes https://github.com/dhall-lang/dhall-haskell/issues/346 Now a Haskell type like: ```haskell data Example = Foo Bool | Bar Text ``` ... corresponds to this Dhall type: ```dhall { Foo : Bool | Bar : Text } ``` * Fix documentation * Add additional test cases ... as suggested by @sjakobi * Test all permutations of: * 0, 1, or 2 fields * Fields of type `()` or `Double` * Named or anonymous fields
This commit is contained in:
Gabriel Gonzalez
mergify[bot]
parent
fddce0b8cf
commit
ca86ed612c
|
|
@ -967,7 +967,7 @@ instance Interpret (f (Result f)) => Interpret (Result f) where
|
|||
-- > \(Expr : Type)
|
||||
-- > -> let ExprF =
|
||||
-- > < LitF :
|
||||
-- > { _1 : Natural }
|
||||
-- > Natural
|
||||
-- > | AddF :
|
||||
-- > { _1 : Expr, _2 : Expr }
|
||||
-- > | MulF :
|
||||
|
|
@ -975,7 +975,7 @@ instance Interpret (f (Result f)) => Interpret (Result f) where
|
|||
-- > >
|
||||
-- >
|
||||
-- > in \(Fix : ExprF -> Expr)
|
||||
-- > -> let Lit = \(x : Natural) -> Fix (ExprF.LitF { _1 = x })
|
||||
-- > -> let Lit = \(x : Natural) -> Fix (ExprF.LitF x)
|
||||
-- >
|
||||
-- > let Add =
|
||||
-- > \(x : Expr)
|
||||
|
|
@ -1222,46 +1222,132 @@ instance GenericInterpret U1 where
|
|||
|
||||
expected = Record (Dhall.Map.fromList [])
|
||||
|
||||
instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :*: g) where
|
||||
genericAutoWith options = do
|
||||
Type extractL expectedL <- genericAutoWith options
|
||||
Type extractR expectedR <- genericAutoWith options
|
||||
let ktsL = unsafeExpectRecord "genericAutoWith (:*:)"expectedL
|
||||
let ktsR = unsafeExpectRecord "genericAutoWith (:*:)"expectedR
|
||||
pure
|
||||
(Type
|
||||
{ extract = liftA2 (liftA2 (:*:)) extractL extractR
|
||||
, expected = Record (Dhall.Map.union ktsL ktsR)
|
||||
}
|
||||
)
|
||||
|
||||
getSelName :: Selector s => M1 i s f a -> State Int String
|
||||
getSelName :: Selector s => M1 i s f a -> State Int Text
|
||||
getSelName n = case selName n of
|
||||
"" -> do i <- get
|
||||
put (i + 1)
|
||||
pure ("_" ++ show i)
|
||||
nn -> pure nn
|
||||
pure (Data.Text.pack ("_" ++ show i))
|
||||
nn -> pure (Data.Text.pack nn)
|
||||
|
||||
instance (GenericInterpret (f :*: g), GenericInterpret (h :*: i)) => GenericInterpret ((f :*: g) :*: (h :*: i)) where
|
||||
genericAutoWith options = do
|
||||
Type extractL expectedL <- genericAutoWith options
|
||||
Type extractR expectedR <- genericAutoWith options
|
||||
|
||||
let ktsL = unsafeExpectRecord "genericAutoWith (:*:)" expectedL
|
||||
let ktsR = unsafeExpectRecord "genericAutoWith (:*:)" expectedR
|
||||
|
||||
let expected = Record (Dhall.Map.union ktsL ktsR)
|
||||
|
||||
let extract expression =
|
||||
liftA2 (:*:) (extractL expression) (extractR expression)
|
||||
|
||||
return (Type {..})
|
||||
|
||||
instance (GenericInterpret (f :*: g), Selector s, Interpret a) => GenericInterpret ((f :*: g) :*: M1 S s (K1 i a)) where
|
||||
genericAutoWith options@InterpretOptions{..} = do
|
||||
let nR :: M1 S s (K1 i a) r
|
||||
nR = undefined
|
||||
|
||||
nameR <- fmap fieldModifier (getSelName nR)
|
||||
|
||||
Type extractL expectedL <- genericAutoWith options
|
||||
|
||||
let Type extractR expectedR = autoWith options
|
||||
|
||||
let ktsL = unsafeExpectRecord "genericAutoWith (:*:)" expectedL
|
||||
|
||||
let expected = Record (Dhall.Map.insert nameR expectedR ktsL)
|
||||
|
||||
let extract expression = do
|
||||
let die = typeError expected expression
|
||||
|
||||
case expression of
|
||||
RecordLit kvs ->
|
||||
case Dhall.Map.lookup nameR kvs of
|
||||
Just expressionR ->
|
||||
liftA2 (:*:)
|
||||
(extractL expression)
|
||||
(fmap (M1 . K1) (extractR expressionR))
|
||||
_ -> die
|
||||
_ -> die
|
||||
|
||||
return (Type {..})
|
||||
|
||||
instance (Selector s, Interpret a, GenericInterpret (f :*: g)) => GenericInterpret (M1 S s (K1 i a) :*: (f :*: g)) where
|
||||
genericAutoWith options@InterpretOptions{..} = do
|
||||
let nL :: M1 S s (K1 i a) r
|
||||
nL = undefined
|
||||
|
||||
nameL <- fmap fieldModifier (getSelName nL)
|
||||
|
||||
let Type extractL expectedL = autoWith options
|
||||
|
||||
Type extractR expectedR <- genericAutoWith options
|
||||
|
||||
let ktsR = unsafeExpectRecord "genericAutoWith (:*:)" expectedR
|
||||
|
||||
let expected = Record (Dhall.Map.insert nameL expectedL ktsR)
|
||||
|
||||
let extract expression = do
|
||||
let die = typeError expected expression
|
||||
|
||||
case expression of
|
||||
RecordLit kvs ->
|
||||
case Dhall.Map.lookup nameL kvs of
|
||||
Just expressionL ->
|
||||
liftA2 (:*:)
|
||||
(fmap (M1 . K1) (extractL expressionL))
|
||||
(extractR expression)
|
||||
_ -> die
|
||||
_ -> die
|
||||
|
||||
return (Type {..})
|
||||
|
||||
instance (Selector s1, Selector s2, Interpret a1, Interpret a2) => GenericInterpret (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where
|
||||
genericAutoWith options@InterpretOptions{..} = do
|
||||
let nL :: M1 S s1 (K1 i1 a1) r
|
||||
nL = undefined
|
||||
|
||||
let nR :: M1 S s2 (K1 i2 a2) r
|
||||
nR = undefined
|
||||
|
||||
nameL <- fmap fieldModifier (getSelName nL)
|
||||
nameR <- fmap fieldModifier (getSelName nR)
|
||||
|
||||
let Type extractL expectedL = autoWith options
|
||||
let Type extractR expectedR = autoWith options
|
||||
|
||||
instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where
|
||||
genericAutoWith opts@(InterpretOptions {..}) = do
|
||||
name <- getSelName n
|
||||
let expected =
|
||||
Record (Dhall.Map.fromList [(key, expected')])
|
||||
where
|
||||
key = fieldModifier (Data.Text.pack name)
|
||||
let extract expr@(RecordLit m) =
|
||||
let name' = fieldModifier (Data.Text.pack name)
|
||||
extract'' e = fmap (M1 . K1) (extract' e)
|
||||
lookupRes = Dhall.Map.lookup name' m
|
||||
typeError' = typeError expected expr
|
||||
in Data.Maybe.maybe typeError' extract'' lookupRes
|
||||
extract expr = typeError expected expr
|
||||
pure (Type {..})
|
||||
where
|
||||
n :: M1 i s f a
|
||||
n = undefined
|
||||
Record
|
||||
(Dhall.Map.fromList
|
||||
[ (nameL, expectedL)
|
||||
, (nameR, expectedR)
|
||||
]
|
||||
)
|
||||
|
||||
Type extract' expected' = autoWith opts
|
||||
let extract expression = do
|
||||
let die = typeError expected expression
|
||||
|
||||
case expression of
|
||||
RecordLit kvs -> do
|
||||
case liftA2 (,) (Dhall.Map.lookup nameL kvs) (Dhall.Map.lookup nameR kvs) of
|
||||
Just (expressionL, expressionR) ->
|
||||
liftA2 (:*:)
|
||||
(fmap (M1 . K1) (extractL expressionL))
|
||||
(fmap (M1 . K1) (extractR expressionR))
|
||||
Nothing -> die
|
||||
_ -> die
|
||||
|
||||
return (Type {..})
|
||||
|
||||
instance Interpret a => GenericInterpret (M1 S s (K1 i a)) where
|
||||
genericAutoWith options = do
|
||||
let Type { extract = extract', ..} = autoWith options
|
||||
|
||||
let extract expression = fmap (M1 . K1) (extract' expression)
|
||||
|
||||
return (Type {..})
|
||||
|
||||
{-| An @(InputType a)@ represents a way to marshal a value of type @\'a\'@ from
|
||||
Haskell into Dhall
|
||||
|
|
@ -1460,6 +1546,12 @@ instance GenericInject f => GenericInject (M1 C c f) where
|
|||
res <- genericInjectWith options
|
||||
pure (contramap unM1 res)
|
||||
|
||||
instance Inject a => GenericInject (M1 S s (K1 i a)) where
|
||||
genericInjectWith options = do
|
||||
let res = injectWith options
|
||||
|
||||
pure (contramap (unK1 . unM1) res)
|
||||
|
||||
instance (Constructor c1, Constructor c2, GenericInject f1, GenericInject f2) => GenericInject (M1 C c1 f1 :+: M1 C c2 f2) where
|
||||
genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..})
|
||||
where
|
||||
|
|
@ -1577,27 +1669,101 @@ instance (GenericInject (f :+: g), GenericInject (h :+: i)) => GenericInject ((f
|
|||
ktsL = unsafeExpectUnion "genericInjectWith (:+:)" declaredL
|
||||
ktsR = unsafeExpectUnion "genericInjectWith (:+:)" declaredR
|
||||
|
||||
instance (GenericInject f, GenericInject g) => GenericInject (f :*: g) where
|
||||
instance (GenericInject (f :*: g), GenericInject (h :*: i)) => GenericInject ((f :*: g) :*: (h :*: i)) where
|
||||
genericInjectWith options = do
|
||||
InputType embedInL declaredInL <- genericInjectWith options
|
||||
InputType embedInR declaredInR <- genericInjectWith options
|
||||
InputType embedL declaredL <- genericInjectWith options
|
||||
InputType embedR declaredR <- genericInjectWith options
|
||||
|
||||
let embed (l :*: r) =
|
||||
RecordLit (Dhall.Map.union mapL mapR)
|
||||
where
|
||||
mapL =
|
||||
unsafeExpectRecordLit "genericInjectWith (:*:)" (embedInL l)
|
||||
unsafeExpectRecordLit "genericInjectWith (:*:)" (embedL l)
|
||||
|
||||
mapR =
|
||||
unsafeExpectRecordLit "genericInjectWith (:*:)" (embedInR r)
|
||||
unsafeExpectRecordLit "genericInjectWith (:*:)" (embedR r)
|
||||
|
||||
let declared = Record (Dhall.Map.union mapL mapR)
|
||||
where
|
||||
mapL = unsafeExpectRecord "genericInjectWith (:*:)" declaredInL
|
||||
mapR = unsafeExpectRecord "genericInjectWith (:*:)" declaredInR
|
||||
mapL = unsafeExpectRecord "genericInjectWith (:*:)" declaredL
|
||||
mapR = unsafeExpectRecord "genericInjectWith (:*:)" declaredR
|
||||
|
||||
pure (InputType {..})
|
||||
|
||||
instance (GenericInject (f :*: g), Selector s, Inject a) => GenericInject ((f :*: g) :*: M1 S s (K1 i a)) where
|
||||
genericInjectWith options@InterpretOptions{..} = do
|
||||
let nR :: M1 S s (K1 i a) r
|
||||
nR = undefined
|
||||
|
||||
nameR <- fmap fieldModifier (getSelName nR)
|
||||
|
||||
InputType embedL declaredL <- genericInjectWith options
|
||||
|
||||
let InputType embedR declaredR = injectWith options
|
||||
|
||||
let embed (l :*: M1 (K1 r)) =
|
||||
RecordLit (Dhall.Map.insert nameR (embedR r) mapL)
|
||||
where
|
||||
mapL =
|
||||
unsafeExpectRecordLit "genericInjectWith (:*:)" (embedL l)
|
||||
|
||||
let declared = Record (Dhall.Map.insert nameR declaredR mapL)
|
||||
where
|
||||
mapL = unsafeExpectRecord "genericInjectWith (:*:)" declaredL
|
||||
|
||||
return (InputType {..})
|
||||
|
||||
instance (Selector s, Inject a, GenericInject (f :*: g)) => GenericInject (M1 S s (K1 i a) :*: (f :*: g)) where
|
||||
genericInjectWith options@InterpretOptions{..} = do
|
||||
let nL :: M1 S s (K1 i a) r
|
||||
nL = undefined
|
||||
|
||||
nameL <- fmap fieldModifier (getSelName nL)
|
||||
|
||||
let InputType embedL declaredL = injectWith options
|
||||
|
||||
InputType embedR declaredR <- genericInjectWith options
|
||||
|
||||
let embed (M1 (K1 l) :*: r) =
|
||||
RecordLit (Dhall.Map.insert nameL (embedL l) mapR)
|
||||
where
|
||||
mapR =
|
||||
unsafeExpectRecordLit "genericInjectWith (:*:)" (embedR r)
|
||||
|
||||
let declared = Record (Dhall.Map.insert nameL declaredL mapR)
|
||||
where
|
||||
mapR = unsafeExpectRecord "genericInjectWith (:*:)" declaredR
|
||||
|
||||
return (InputType {..})
|
||||
|
||||
instance (Selector s1, Selector s2, Inject a1, Inject a2) => GenericInject (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where
|
||||
genericInjectWith options@InterpretOptions{..} = do
|
||||
let nL :: M1 S s1 (K1 i1 a1) r
|
||||
nL = undefined
|
||||
|
||||
let nR :: M1 S s2 (K1 i2 a2) r
|
||||
nR = undefined
|
||||
|
||||
nameL <- fmap fieldModifier (getSelName nL)
|
||||
nameR <- fmap fieldModifier (getSelName nR)
|
||||
|
||||
let InputType embedL declaredL = injectWith options
|
||||
let InputType embedR declaredR = injectWith options
|
||||
|
||||
let embed (M1 (K1 l) :*: M1 (K1 r)) =
|
||||
RecordLit
|
||||
(Dhall.Map.fromList
|
||||
[ (nameL, embedL l), (nameR, embedR r) ]
|
||||
)
|
||||
|
||||
let declared =
|
||||
Record
|
||||
(Dhall.Map.fromList
|
||||
[ (nameL, declaredL), (nameR, declaredR) ]
|
||||
)
|
||||
|
||||
return (InputType {..})
|
||||
|
||||
instance GenericInject U1 where
|
||||
genericInjectWith _ = pure (InputType {..})
|
||||
where
|
||||
|
|
@ -1605,20 +1771,6 @@ instance GenericInject U1 where
|
|||
|
||||
declared = Record mempty
|
||||
|
||||
instance (Selector s, Inject a) => GenericInject (M1 S s (K1 i a)) where
|
||||
genericInjectWith opts@(InterpretOptions {..}) = do
|
||||
name <- fieldModifier . Data.Text.pack <$> getSelName n
|
||||
let embed (M1 (K1 x)) =
|
||||
RecordLit (Dhall.Map.singleton name (embedIn x))
|
||||
let declared =
|
||||
Record (Dhall.Map.singleton name declaredIn)
|
||||
pure (InputType {..})
|
||||
where
|
||||
n :: M1 i s f a
|
||||
n = undefined
|
||||
|
||||
InputType embedIn declaredIn = injectWith opts
|
||||
|
||||
{-| The 'RecordType' applicative functor allows you to build a 'Type' parser
|
||||
from a Dhall record.
|
||||
|
||||
|
|
|
|||
|
|
@ -161,7 +161,10 @@ data NonEmptyUnion = N0 Bool | N1 Natural | N2 Text
|
|||
data Enum = E0 | E1 | E2
|
||||
deriving (Eq, Generic, Inject, Interpret, Show)
|
||||
|
||||
data Mixed = M0 Bool | M1 | M2 ()
|
||||
data Records = R0 {} | R1 { a :: () } | R2 { x :: Double } | R3 { a :: (), b :: () } | R4 { x :: Double, y :: Double }
|
||||
deriving (Eq, Generic, Inject, Interpret, Show)
|
||||
|
||||
data Products = P0 | P1 () | P2 Double | P3 () () | P4 Double Double
|
||||
deriving (Eq, Generic, Inject, Interpret, Show)
|
||||
|
||||
deriving instance Interpret ()
|
||||
|
|
@ -169,48 +172,73 @@ deriving instance Interpret ()
|
|||
shouldHandleUnionsCorrectly :: TestTree
|
||||
shouldHandleUnionsCorrectly =
|
||||
testGroup "Handle union literals"
|
||||
[ "λ(x : < N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >) → x"
|
||||
[ "λ(x : < N0 : Bool | N1 : Natural | N2 : Text >) → x"
|
||||
`shouldPassThrough` [ N0 True, N1 5, N2 "ABC" ]
|
||||
, "λ(x : < E0 | E1 | E2 >) → x"
|
||||
`shouldPassThrough` [ E0, E1, E2 ]
|
||||
, "λ(x : < M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >) → x"
|
||||
`shouldPassThrough` [ M0 True, M1, M2 () ]
|
||||
, "λ(x : < R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >) → x"
|
||||
`shouldPassThrough` [ R0 {}, R1 { a = () }, R2 { x = 1.0 }, R3 { a = (), b = () }, R4 { x = 1.0, y = 2.0 } ]
|
||||
, "λ(x : < P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >) → x"
|
||||
`shouldPassThrough` [ P0 , P1 (), P2 1.0, P3 () (), P4 1.0 2.0 ]
|
||||
|
||||
, "(< N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >).N0 { _1 = True }"
|
||||
, "(< N0 : Bool | N1 : Natural | N2 : Text >).N0 True"
|
||||
`shouldMarshalInto` N0 True
|
||||
, "(< N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >).N1 { _1 = 5 }"
|
||||
, "(< N0 : Bool | N1 : Natural | N2 : Text >).N1 5"
|
||||
`shouldMarshalInto` N1 5
|
||||
, "(< N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >).N2 { _1 = \"ABC\" }"
|
||||
, "(< N0 : Bool | N1 : Natural | N2 : Text >).N2 \"ABC\""
|
||||
`shouldMarshalInto` N2 "ABC"
|
||||
|
||||
, "(< E0 | E1 | E2>).E0" `shouldMarshalInto` E0
|
||||
, "(< E0 | E1 | E2>).E1" `shouldMarshalInto` E1
|
||||
, "(< E0 | E1 | E2>).E2" `shouldMarshalInto` E2
|
||||
|
||||
, "(< M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >).M0 { _1 = True }"
|
||||
`shouldMarshalInto` M0 True
|
||||
, "(< M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >).M1"
|
||||
`shouldMarshalInto` M1
|
||||
, "(< M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >).M2 { _1 = {=} }"
|
||||
`shouldMarshalInto` M2 ()
|
||||
, "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R0"
|
||||
`shouldMarshalInto` R0
|
||||
, "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R1"
|
||||
`shouldMarshalInto` R1 { a = () }
|
||||
, "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R2 1.0"
|
||||
`shouldMarshalInto` R2 { x = 1.0 }
|
||||
, "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R3 { a = {=}, b = {=} }"
|
||||
`shouldMarshalInto` R3 { a = (), b = () }
|
||||
, "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R4 { x = 1.0, y = 2.0 }"
|
||||
`shouldMarshalInto` R4 { x = 1.0, y = 2.0 }
|
||||
|
||||
, "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P0"
|
||||
`shouldMarshalInto` P0
|
||||
, "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P1"
|
||||
`shouldMarshalInto` P1 ()
|
||||
, "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P2 1.0"
|
||||
`shouldMarshalInto` P2 1.0
|
||||
, "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P3 { _1 = {=}, _2 = {=} }"
|
||||
`shouldMarshalInto` P3 () ()
|
||||
, "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P4 { _1 = 1.0, _2 = 2.0 }"
|
||||
`shouldMarshalInto` P4 1.0 2.0
|
||||
|
||||
, N0 True
|
||||
`shouldInjectInto`
|
||||
"(< N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >).N0 { _1 = True }"
|
||||
"(< N0 : Bool | N1 : Natural | N2 : Text >).N0 True"
|
||||
, N1 5
|
||||
`shouldInjectInto`
|
||||
"(< N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >).N1 { _1 = 5 }"
|
||||
"(< N0 : Bool | N1 : Natural | N2 : Text >).N1 5"
|
||||
, N2 "ABC"
|
||||
`shouldInjectInto`
|
||||
"(< N0 : { _1 : Bool } | N1 : { _1 : Natural } | N2 : { _1 : Text } >).N2 { _1 = \"ABC\" }"
|
||||
"(< N0 : Bool | N1 : Natural | N2 : Text >).N2 \"ABC\""
|
||||
|
||||
, E0 `shouldInjectInto` "< E0 | E1 | E2 >.E0"
|
||||
, E1 `shouldInjectInto` "< E0 | E1 | E2 >.E1"
|
||||
, E2 `shouldInjectInto` "< E0 | E1 | E2 >.E2"
|
||||
|
||||
, M0 True `shouldInjectInto` "(< M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >).M0 { _1 = True }"
|
||||
, M1 `shouldInjectInto` "(< M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >).M1"
|
||||
, M2 () `shouldInjectInto` "(< M0 : { _1 : Bool } | M1 | M2 : { _1 : {} } >).M2 { _1 = {=} }"
|
||||
, R0 `shouldInjectInto` "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R0"
|
||||
, R1 { a = () } `shouldInjectInto` "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R1"
|
||||
, R2 { x = 1.0 } `shouldInjectInto` "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R2 1.0"
|
||||
, R3 { a = (), b = () } `shouldInjectInto` "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R3 { a = {=}, b = {=} }"
|
||||
, R4 { x = 1.0, y = 2.0 } `shouldInjectInto` "< R0 | R1 | R2 : Double | R3 : { a : {}, b : {} } | R4 : { x : Double, y : Double } >.R4 { x = 1.0, y = 2.0 }"
|
||||
|
||||
, P0 `shouldInjectInto` "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P0"
|
||||
, P1 () `shouldInjectInto` "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P1"
|
||||
, P2 1.0 `shouldInjectInto` "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P2 1.0"
|
||||
, P3 () () `shouldInjectInto` "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P3 { _1 = {=}, _2 = {=} }"
|
||||
, P4 1.0 2.0 `shouldInjectInto` "< P0 | P1 | P2 : Double | P3 : { _1 : {}, _2 : {} } | P4 : { _1 : Double, _2 : Double } >.P4 { _1 = 1.0, _2 = 2.0 }"
|
||||
]
|
||||
where
|
||||
code `shouldPassThrough` values = testCase "Pass through" $ do
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
λ(Expr : Type)
|
||||
→ let ExprF =
|
||||
< LitF :
|
||||
{ _1 : Natural }
|
||||
< LitF : Natural
|
||||
| AddF :
|
||||
{ _1 : Expr, _2 : Expr }
|
||||
| MulF :
|
||||
|
|
@ -9,7 +8,7 @@
|
|||
>
|
||||
|
||||
in λ(Fix : ExprF → Expr)
|
||||
→ let Lit = λ(x : Natural) → Fix (ExprF.LitF { _1 = x })
|
||||
→ let Lit = λ(x : Natural) → Fix (ExprF.LitF x)
|
||||
|
||||
let Add =
|
||||
λ(x : Expr) → λ(y : Expr) → Fix (ExprF.AddF { _1 = x, _2 = y })
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
λ(a : Type)
|
||||
→ let ExprF =
|
||||
< LitF :
|
||||
{ _1 : Natural }
|
||||
Natural
|
||||
| AddF :
|
||||
{ _1 : a, _2 : a }
|
||||
| MulF :
|
||||
|
|
@ -9,7 +9,7 @@
|
|||
>
|
||||
|
||||
in λ(a : ExprF → a)
|
||||
→ let Lit = λ(x : Natural) → a (ExprF.LitF { _1 = x })
|
||||
→ let Lit = λ(x : Natural) → a (ExprF.LitF x)
|
||||
|
||||
let Add = λ(x : a@1) → λ(y : a@1) → a (ExprF.AddF { _1 = x, _2 = y })
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue