From ff748b988e6106a68b95ac25351741b940a0e92f Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 16 Jan 2023 14:13:17 +0000 Subject: [PATCH] Do not filter implicit args in internal to core translation (#1728) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The internal to core translation was removing implicit arguments from function definitions and applications. This is incorrect as the implicit bindings are required when translating the following (in `csuc`, the binding of the implicit argument is required in an application on the rhs): ``` Num : Type; Num := {A : Type} → (A → A) → A → A; csuc : Num → Num; csuc n {_} f := f ∘ n {_} f; ``` Apart from removing this filter from function and application translation, this required the following changes: ConstructorInfo: The _constructorArgsNum field must include the number of type parameters of its inductive type. PatternConstructorApp: The pattern arguments must include wildcards for the implicit type parameters passed to the constructor. BuiltinIf: The BuiltinIf expression is passed an implicit type argument that must be removed when translating to Core if. LitString: A literal string is a function with an implcit type argument. So this must be a translated to a lambda where the type argument is ignored. Fixes https://github.com/anoma/juvix/issues/1714 --- .../Compiler/Core/Translation/FromInternal.hs | 102 ++++++++++-------- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 3 + test/Internal/Eval/Positive.hs | 7 +- tests/Internal/positive/Church.juvix | 21 ++++ tests/Internal/positive/out/Church.out | 1 + tests/Internal/positive/out/QuickSort.out | 2 +- 6 files changed, 87 insertions(+), 49 deletions(-) create mode 100644 tests/Internal/positive/Church.juvix create mode 100644 tests/Internal/positive/out/Church.out diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 291311f610..0c3b25f185 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -21,9 +21,6 @@ import Juvix.Extra.Strings qualified as Str unsupported :: Text -> a unsupported thing = error ("Internal to Core: Not yet supported: " <> thing) -isExplicit :: Internal.PatternArg -> Bool -isExplicit = (== Internal.Explicit) . (^. Internal.patternArgIsImplicit) - -- Translation of a Name into the identifier index used in the Core InfoTable mkIdentIndex :: Name -> Text mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId) @@ -184,16 +181,19 @@ goConstructor sym ctor = do mblt <- mBuiltin tag <- ctorTag mblt ty <- ctorType + argsNum' <- argsNum + let info = ConstructorInfo - { _constructorName = ctor ^. Internal.inductiveConstructorName . nameText, - _constructorLocation = Just $ ctor ^. Internal.inductiveConstructorName . nameLoc, + { _constructorName = ctorName ^. nameText, + _constructorLocation = Just $ ctorName ^. nameLoc, _constructorTag = tag, _constructorType = ty, - _constructorArgsNum = length (ctor ^. Internal.inductiveConstructorParameters), + _constructorArgsNum = argsNum', _constructorInductive = sym, _constructorBuiltin = mblt } + registerConstructor (mkIdentIndex (ctor ^. Internal.inductiveConstructorName)) info return info where @@ -203,6 +203,9 @@ goConstructor sym ctor = do . HashMap.lookupDefault impossible (ctor ^. Internal.inductiveConstructorName) <$> asks (^. Internal.infoConstructors) + ctorName :: Internal.Name + ctorName = ctor ^. Internal.inductiveConstructorName + ctorTag :: Maybe Internal.BuiltinConstructor -> Sem r Tag ctorTag = \case Just Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue) @@ -215,10 +218,15 @@ goConstructor sym ctor = do ctorType = runReader initIndexTable - ( Internal.constructorType (ctor ^. Internal.inductiveConstructorName) + ( Internal.constructorType ctorName >>= goExpression ) + argsNum :: Sem r Int + argsNum = do + (indParams, ctorArgs) <- InternalTyped.lookupConstructorArgTypes ctorName + return (length indParams + length ctorArgs) + goMutualBlock :: forall r. Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r => @@ -268,25 +276,24 @@ goFunctionDef (f, sym) = do forM_ mbody (registerIdentNode sym) where mkBody :: Sem r Node - mkBody = - if - | nExplicitPatterns == 0 -> runReader initIndexTable (goExpression (f ^. Internal.funDefClauses . _head1 . Internal.clauseBody)) - | otherwise -> - ( do - let values :: [Node] - values = mkVar Info.empty <$> vs - indexTable :: IndexTable - indexTable = IndexTable {_indexTableVarsNum = nExplicitPatterns, _indexTableVars = mempty} - ms <- mapM (runReader indexTable . goFunctionClause) (f ^. Internal.funDefClauses) - let match = mkMatch' (fromList values) (toList ms) - return $ foldr (\_ n -> mkLambda' n) match vs - ) + mkBody + | nPatterns == 0 = runReader initIndexTable (goExpression (f ^. Internal.funDefClauses . _head1 . Internal.clauseBody)) + | otherwise = + ( do + let values :: [Node] + values = mkVar Info.empty <$> vs + indexTable :: IndexTable + indexTable = IndexTable {_indexTableVarsNum = nPatterns, _indexTableVars = mempty} + ms <- mapM (runReader indexTable . goFunctionClause) (f ^. Internal.funDefClauses) + let match = mkMatch' (fromList values) (toList ms) + return $ foldr (\_ n -> mkLambda' n) match vs + ) -- Assumption: All clauses have the same number of patterns - nExplicitPatterns :: Int - nExplicitPatterns = length $ filter isExplicit (f ^. Internal.funDefClauses . _head1 . Internal.clausePatterns) + nPatterns :: Int + nPatterns = length (f ^. Internal.funDefClauses . _head1 . Internal.clausePatterns) vs :: [Index] - vs = take nExplicitPatterns [0 ..] + vs = take nPatterns [0 ..] goLambda :: forall r. @@ -393,19 +400,24 @@ fromPattern :: fromPattern = \case Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) mkDynamic') wildcard) Internal.PatternConstructorApp c -> do - let n = c ^. Internal.constrAppConstructor - explicitPatterns = - (^. Internal.patternArgPattern) - <$> filter - isExplicit - (c ^. Internal.constrAppParameters) - args <- mapM fromPattern explicitPatterns + (indParams, _) <- InternalTyped.lookupConstructorArgTypes n + patternArgs <- mapM fromPattern patterns + let indArgs = replicate (length indParams) wildcard + args = indArgs ++ patternArgs m <- getIdent identIndex case m of Just (IdentConstr tag) -> return $ PatConstr (PatternConstr (setInfoLocation (n ^. nameLoc) (setInfoName (n ^. nameText) Info.empty)) tag args) Just _ -> error ("internal to core: not a constructor " <> txt) Nothing -> error ("internal to core: undeclared identifier: " <> txt) where + n :: Name + n = c ^. Internal.constrAppConstructor + + patterns :: [Internal.Pattern] + patterns = + (^. Internal.patternArgPattern) + <$> (c ^. Internal.constrAppParameters) + identIndex :: Text identIndex = mkIdentIndex (c ^. Internal.constrAppConstructor) @@ -419,13 +431,11 @@ getPatternVars :: Internal.Pattern -> [Name] getPatternVars = \case Internal.PatternVariable n -> [n] Internal.PatternConstructorApp c -> - concatMap getPatternVars explicitPatterns + concatMap getPatternVars patterns where - explicitPatterns = + patterns = (^. Internal.patternArgPattern) - <$> filter - isExplicit - (c ^. Internal.constrAppParameters) + <$> (c ^. Internal.constrAppParameters) goPatterns :: forall r. @@ -461,22 +471,22 @@ goFunctionClause :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r => Internal.FunctionClause -> Sem r MatchBranch -goFunctionClause clause = +goFunctionClause clause = do local (over indexTableVars (HashMap.union patternArgs)) (goPatterns (clause ^. Internal.clauseBody) ps) where - explicitPatternArgs :: [Internal.PatternArg] - explicitPatternArgs = filter isExplicit (clause ^. Internal.clausePatterns) + internalPatternArgs :: [Internal.PatternArg] + internalPatternArgs = clause ^. Internal.clausePatterns ps :: [Internal.Pattern] - ps = (^. Internal.patternArgPattern) <$> explicitPatternArgs + ps = (^. Internal.patternArgPattern) <$> internalPatternArgs patternArgs :: HashMap NameId Index patternArgs = HashMap.fromList (first (^. nameId) <$> patternArgNames) where patternArgNames :: [(Name, Index)] - patternArgNames = catFstMaybes (first (^. Internal.patternArgName) <$> zip explicitPatternArgs [0 ..]) + patternArgNames = catFstMaybes (first (^. Internal.patternArgName) <$> zip internalPatternArgs [0 ..]) catFstMaybes :: [(Maybe a, b)] -> [(a, b)] catFstMaybes = mapMaybe f @@ -586,16 +596,14 @@ goApplication :: Internal.Application -> Sem r Node goApplication a = do - (f, args) <- Internal.unfoldPolyApplication a - let exprArgs :: Sem r [Node] + let (f, args) = second toList (Internal.unfoldApplication a) + exprArgs :: Sem r [Node] exprArgs = mapM goExpression args app :: Sem r Node app = do fExpr <- goExpression f - case a ^. Internal.appImplicit of - Internal.Implicit -> return fExpr - Internal.Explicit -> mkApps' fExpr <$> exprArgs + mkApps' fExpr <$> exprArgs case f of Internal.ExpressionIden (Internal.IdenFunction n) -> do @@ -605,14 +613,14 @@ goApplication a = do sym <- getBoolSymbol as <- exprArgs case as of - (v : b1 : b2 : xs) -> return (mkApps' (mkIf' sym v b1 b2) xs) + (_ : v : b1 : b2 : xs) -> return (mkApps' (mkIf' sym v b1 b2) xs) _ -> error "if must be called with 3 arguments" _ -> app _ -> app goLiteral :: Symbol -> LiteralLoc -> Node goLiteral intToNat l = case l ^. withLocParam of - Internal.LitString s -> mkLitConst (ConstString s) + Internal.LitString s -> mkLambda' (mkLitConst (ConstString s)) Internal.LitInteger i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i)) where mkLitConst :: ConstantValue -> Node diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 3ef80cd190..5f4301a166 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -102,6 +102,9 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes) lookupConstructor :: Member (Reader InfoTable) r => Name -> Sem r ConstructorInfo lookupConstructor f = HashMap.lookupDefault impossible f <$> asks (^. infoConstructors) +lookupConstructorArgTypes :: Member (Reader InfoTable) r => Name -> Sem r ([VarName], [Expression]) +lookupConstructorArgTypes = fmap constructorArgTypes . lookupConstructor + lookupInductive :: Member (Reader InfoTable) r => InductiveName -> Sem r InductiveInfo lookupInductive f = HashMap.lookupDefault impossible f <$> asks (^. infoInductives) diff --git a/test/Internal/Eval/Positive.hs b/test/Internal/Eval/Positive.hs index bc0db921b3..024e618c6f 100644 --- a/test/Internal/Eval/Positive.hs +++ b/test/Internal/Eval/Positive.hs @@ -168,5 +168,10 @@ tests = "Higher Order Lambda" $(mkRelDir ".") $(mkRelFile "HigherOrderLambda.juvix") - $(mkRelFile "out/HigherOrderLambda.out") + $(mkRelFile "out/HigherOrderLambda.out"), + PosTest + "Type Aliases" + $(mkRelDir ".") + $(mkRelFile "Church.juvix") + $(mkRelFile "out/Church.out") ] diff --git a/tests/Internal/positive/Church.juvix b/tests/Internal/positive/Church.juvix new file mode 100644 index 0000000000..a3801a87d8 --- /dev/null +++ b/tests/Internal/positive/Church.juvix @@ -0,0 +1,21 @@ +module Church; + +open import Stdlib.Prelude; + +Num : Type; +Num := {A : Type} → (A → A) → A → A; + +czero : Num; +czero {_} f x := x; + +csuc : Num → Num; +csuc n {_} f := f ∘ n {_} f; + +toNat : Num → Nat; +toNat n := n {_} ((+) one) zero; + +main : IO; +main := + printNatLn (toNat (csuc (czero))); + +end; diff --git a/tests/Internal/positive/out/Church.out b/tests/Internal/positive/out/Church.out new file mode 100644 index 0000000000..55312977f8 --- /dev/null +++ b/tests/Internal/positive/out/Church.out @@ -0,0 +1 @@ +suc zero diff --git a/tests/Internal/positive/out/QuickSort.out b/tests/Internal/positive/out/QuickSort.out index dd9cdc57fe..6d04fd0060 100644 --- a/tests/Internal/positive/out/QuickSort.out +++ b/tests/Internal/positive/out/QuickSort.out @@ -1 +1 @@ -:: (suc (suc zero)) (:: (suc (suc (suc zero))) (:: (suc (suc (suc (suc zero)))) (:: (suc (suc (suc (suc (suc zero))))) (:: (suc (suc (suc (suc (suc (suc zero)))))) (:: (suc (suc (suc (suc (suc (suc (suc zero))))))) nil))))) +:: (Nat) (suc (suc zero)) (:: (Nat) (suc (suc (suc zero))) (:: (Nat) (suc (suc (suc (suc zero)))) (:: (Nat) (suc (suc (suc (suc (suc zero))))) (:: (Nat) (suc (suc (suc (suc (suc (suc zero)))))) (:: (Nat) (suc (suc (suc (suc (suc (suc (suc zero))))))) (nil (Nat)))))))