From ca86ed612c075f60874d99a3b6875e2c2387cfff Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Sat, 14 Sep 2019 20:37:42 -0700 Subject: [PATCH] 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 --- dhall/src/Dhall.hs | 266 +++++++++++++++++++++++------- dhall/tests/Dhall/Test/Dhall.hs | 66 +++++--- dhall/tests/recursive/expr0.dhall | 5 +- dhall/tests/recursive/expr1.dhall | 4 +- 4 files changed, 260 insertions(+), 81 deletions(-) diff --git a/dhall/src/Dhall.hs b/dhall/src/Dhall.hs index 3fed153..5e17516 100644 --- a/dhall/src/Dhall.hs +++ b/dhall/src/Dhall.hs @@ -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. diff --git a/dhall/tests/Dhall/Test/Dhall.hs b/dhall/tests/Dhall/Test/Dhall.hs index 3e951d4..fdc6654 100644 --- a/dhall/tests/Dhall/Test/Dhall.hs +++ b/dhall/tests/Dhall/Test/Dhall.hs @@ -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 diff --git a/dhall/tests/recursive/expr0.dhall b/dhall/tests/recursive/expr0.dhall index 06d4428..34e507b 100644 --- a/dhall/tests/recursive/expr0.dhall +++ b/dhall/tests/recursive/expr0.dhall @@ -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 }) diff --git a/dhall/tests/recursive/expr1.dhall b/dhall/tests/recursive/expr1.dhall index 8f6fa04..89ad5c0 100644 --- a/dhall/tests/recursive/expr1.dhall +++ b/dhall/tests/recursive/expr1.dhall @@ -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 })