From 299e4ee59a94349041af24065e071f9660932ebe Mon Sep 17 00:00:00 2001 From: ndwarshuis Date: Thu, 20 Apr 2023 00:09:51 -0400 Subject: [PATCH] add TH support for nested higher kinded types --- dhall/src/Dhall/TH.hs | 102 +++++++++++++++++++++----- dhall/tests/Dhall/Test/TH.hs | 28 +++++++ dhall/tests/th/HigherKindNested.dhall | 10 +++ 3 files changed, 123 insertions(+), 17 deletions(-) create mode 100644 dhall/tests/th/HigherKindNested.dhall diff --git a/dhall/src/Dhall/TH.hs b/dhall/src/Dhall/TH.hs index ed08d0334..f1f86ddf9 100644 --- a/dhall/src/Dhall/TH.hs +++ b/dhall/src/Dhall/TH.hs @@ -45,6 +45,7 @@ import Language.Haskell.TH.Syntax (DerivClause (..), DerivStrategy (..)) import qualified Data.List as List import qualified Data.Map as Map +import qualified Data.Maybe as Maybe import qualified Data.Set as Set import qualified Data.Text as Text import qualified Data.Time as Time @@ -131,8 +132,6 @@ toNestedHaskellType -> Q Type toNestedHaskellType typeParams haskellTypes = loop where - predicate dhallType haskellType = Core.judgmentallyEqual (code haskellType) dhallType - document dhallType = mconcat [ "Unsupported nested type\n" @@ -206,17 +205,91 @@ toNestedHaskellType typeParams haskellTypes = loop Var v | Just (V param index) <- List.find (v ==) typeParams -> do - let name = Syntax.mkName $ (Text.unpack param) ++ (show index) - - return (VarT name) + return $ VarT $ Syntax.mkName $ (Text.unpack param) ++ (show index) | otherwise -> fail $ message v - _ | Just haskellType <- List.find (predicate dhallType) haskellTypes -> do - let name = Syntax.mkName (Text.unpack (typeName haskellType)) + _ -> do + res <- mapM (judgementallyEqualNested dhallType) haskellTypes + + maybe (fail $ message dhallType) return $ Maybe.listToMaybe $ Maybe.catMaybes res + + haskellTypeToConT haskellType = ConT $ Syntax.mkName (Text.unpack (typeName haskellType)) + + judgementallyEqualNested dhallType haskellType = case partitionTypeVars (code haskellType) of + ([], haskellType') + | Core.judgmentallyEqual haskellType' dhallType -> + return $ Just $ haskellTypeToConT haskellType + + | otherwise -> return Nothing + + (params, bareHaskellType) + | Just nested <- gatherNestedVars Map.empty bareHaskellType dhallType -> do + let con = haskellTypeToConT haskellType + + nestedTypes <- mapM (toNestedHaskellType typeParams haskellTypes) + $ Maybe.mapMaybe (`Map.lookup` nested) params + + return $ Just $ foldr (flip AppT) con $ reverse nestedTypes + + | otherwise -> return Nothing + + gatherNestedVars nested haskellType dhallType = case (haskellType, dhallType) of + + -- if haskellType has a typevar, store whatever the dhallType has unless + -- this typevar already has an existing dhalltype which doesn't match + ((Var v), newDhallType) -> case Map.lookup v nested of + Just oldDhallType + | Core.judgmentallyEqual oldDhallType newDhallType -> Just nested + + | otherwise -> Nothing + + Nothing -> Just $ Map.insert v newDhallType nested - return (ConT name) - | otherwise -> fail $ message dhallType + -- iterate through all records one level down + (Record m1, Record m2) + | Dhall.Map.keysSet m1 == Dhall.Map.keysSet m2 + -> gatherNestedVarsAcross (Just nested) + $ Dhall.Map.elems + $ Dhall.Map.intersectionWith combineRec m1 m2 + + | otherwise -> Nothing + + -- ditto for unions, except here we need to check if each alternate + -- has either no type or a matching type + (Union m1, Union m2) + | Dhall.Map.keysSet m1 == Dhall.Map.keysSet m2 -> do + es <- sequence $ Dhall.Map.elems $ Dhall.Map.intersectionWith combineUnion m1 m2 + gatherNestedVarsAcross (Just nested) $ Maybe.catMaybes es + + | otherwise -> Nothing + + -- otherwise there is nothing to store and no further levels into which + -- to drill futher, so compare directly + (i, j) + | Core.judgmentallyEqual i j -> Just nested + + | otherwise -> Nothing + + gatherNestedVarsAcross nested [] = nested + gatherNestedVarsAcross Nothing _ = Nothing + gatherNestedVarsAcross (Just nested) ((ht, dt):rest) = + gatherNestedVarsAcross (gatherNestedVars nested ht dt) rest + + combineRec x y = (Core.recordFieldValue x, Core.recordFieldValue y) + + combineUnion (Just x) (Just y) = Just (Just (x, y)) -- two alts with types (valid) + combineUnion Nothing Nothing = Just Nothing -- two alts with no types (valid) + combineUnion _ _ = Nothing -- anything else (invalid) + + +-- | Split expression into type variables (from leading lambdas if present) and +-- its nested expression. +partitionTypeVars :: Expr s a -> ([Var], Expr s a) +partitionTypeVars = first (reverse . numberConsecutive) . go [] + where + go acc (Lam _ (FunctionBinding _ v _ _ _) rest) = go (v:acc) rest + go acc rest = (acc, rest) -- | A deriving clause for `Generic`. derivingGenericClause :: DerivClause @@ -251,14 +324,9 @@ toDeclaration -> Q [Dec] toDeclaration generateOptions@GenerateOptions{..} haskellTypes typ = case typ of - SingleConstructor{..} -> uncurry (fromSingle typeName constructorName) $ getTypeParams code - MultipleConstructors{..} -> uncurry (fromMulti typeName) $ getTypeParams code + SingleConstructor{..} -> uncurry (fromSingle typeName constructorName) $ partitionTypeVars code + MultipleConstructors{..} -> uncurry (fromMulti typeName) $ partitionTypeVars code where - getTypeParams = first numberConsecutive . getTypeParams_ [] - - getTypeParams_ acc (Lam _ (FunctionBinding _ v _ _ _) rest) = getTypeParams_ (v:acc) rest - getTypeParams_ acc rest = (acc, rest) - derivingClauses = [ derivingGenericClause | generateFromDhallInstance || generateToDhallInstance ] interpretOptions = generateToInterpretOptions generateOptions typ @@ -330,7 +398,7 @@ toDeclaration generateOptions@GenerateOptions{..} haskellTypes typ = -- | Number each variable, starting at 0 numberConsecutive :: [Text.Text] -> [Var] -numberConsecutive = snd . List.mapAccumR go Map.empty . reverse +numberConsecutive = reverse . snd . List.mapAccumR go Map.empty . reverse where go m k = let (i, m') = Map.updateLookupWithKey (\_ j -> Just $ j + 1) k m diff --git a/dhall/tests/Dhall/Test/TH.hs b/dhall/tests/Dhall/Test/TH.hs index b61a47e56..1ef7629fe 100644 --- a/dhall/tests/Dhall/Test/TH.hs +++ b/dhall/tests/Dhall/Test/TH.hs @@ -116,10 +116,16 @@ Dhall.TH.makeHaskellTypesWith (Dhall.TH.defaultGenerateOptions }) [ SingleConstructor "MyHKSingle" "HKSingle" "./tests/th/HigherKindSingle.dhall" , MultipleConstructors "MyHKUnion" "./tests/th/HigherKindUnion.dhall" + , SingleConstructor "MyHKInnerS" "HKInnerS" "(./tests/th/HigherKindNested.dhall).InnerS" + , MultipleConstructors "MyHKInnerU" "(./tests/th/HigherKindNested.dhall).InnerU" + , SingleConstructor "MyHKOuter" "HKOuter" "(./tests/th/HigherKindNested.dhall).Outer" ] type MyHKSingle_ = MyHKSingle Maybe Int type MyHKUnion_ = MyHKUnion Bool Int +type MyHKInnerS_ = MyHKInnerS Bool Data.Text.Text +type MyHKInnerU_ = MyHKInnerU Int Data.Text.Text +type MyHKOuter_ = MyHKOuter Bool Int deriving instance Eq MyHKSingle_ deriving instance Show MyHKSingle_ @@ -133,6 +139,24 @@ deriving instance Dhall.Generic MyHKUnion_ instance Dhall.FromDhall MyHKUnion_ instance Dhall.ToDhall MyHKUnion_ +deriving instance Eq MyHKInnerS_ +deriving instance Show MyHKInnerS_ +deriving instance Dhall.Generic MyHKInnerS_ +instance Dhall.FromDhall MyHKInnerS_ +instance Dhall.ToDhall MyHKInnerS_ + +deriving instance Eq MyHKInnerU_ +deriving instance Show MyHKInnerU_ +deriving instance Dhall.Generic MyHKInnerU_ +instance Dhall.FromDhall MyHKInnerU_ +instance Dhall.ToDhall MyHKInnerU_ + +deriving instance Eq MyHKOuter_ +deriving instance Show MyHKOuter_ +deriving instance Dhall.Generic MyHKOuter_ +instance Dhall.FromDhall MyHKOuter_ +instance Dhall.ToDhall MyHKOuter_ + testMakeHaskellTypesWith :: TestTree testMakeHaskellTypesWith = Tasty.HUnit.testCase "makeHaskellTypesWith" $ do let text0 = "let T = ./tests/th/example.dhall in T.A { x = True, y = [] : List Text }" @@ -167,6 +191,10 @@ testMakeHaskellTypesWith = Tasty.HUnit.testCase "makeHaskellTypesWith" $ do refHKUnion1 = MyBar 1 :: MyHKUnion_ myTest textHKUnion1 refHKUnion1 + let textHKOuter = "let T = (./tests/th/HigherKindNested.dhall) in T.Outer Bool Int { oFoo = { iFoo = True, iBar = \"\" }, oBar = T.InnerU.Ifoo +1 }" + refHKOuter = MyHKOuter { myObar = MyIfoo 1, myOfoo = (MyHKInnerS { myIbar = "", myIfoo = True }) } :: MyHKOuter_ + myTest textHKOuter refHKOuter + where myTest text ref = do expr <- Dhall.inputExpr text diff --git a/dhall/tests/th/HigherKindNested.dhall b/dhall/tests/th/HigherKindNested.dhall new file mode 100644 index 000000000..526e69fff --- /dev/null +++ b/dhall/tests/th/HigherKindNested.dhall @@ -0,0 +1,10 @@ +let InnerS = \(x : Type) -> \(y : Type) -> { ifoo : x, ibar : y } + +let InnerU = \(x : Type) -> \(y : Type) -> < Ifoo : x | Ibar : y > + +let Outer = + \(i : Type) -> + \(j : Type) -> + { ofoo : InnerS i Text, obar : InnerU j Text } + +in { InnerS, InnerU, Outer }