From 1afc43a711981375e80cfce17d639dfbeb458d34 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 12 Jul 2024 17:16:29 +0200 Subject: [PATCH] multiple definitions in a let --- .../Compiler/Backend/Isabelle/Language.hs | 9 ++- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 11 ++- .../Backend/Isabelle/Translation/FromTyped.hs | 71 ++++++++++++------- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 13 ++-- .../Compiler/Store/Internal/Data/InfoTable.hs | 3 +- 5 files changed, 70 insertions(+), 37 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index a42b385710..a0e130c1e0 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs @@ -77,11 +77,15 @@ data Binop = Binop } data Let = Let - { _letVar :: Name, - _letValue :: Expression, + { _letClauses :: NonEmpty LetClause, _letBody :: Expression } +data LetClause = LetClause + { _letClauseName :: Name, + _letClauseValue :: Expression + } + data If = If { _ifValue :: Expression, _ifBranchTrue :: Expression, @@ -132,6 +136,7 @@ data ConstrApp = ConstrApp makeLenses ''Application makeLenses ''Let +makeLenses ''LetClause makeLenses ''If makeLenses ''Case makeLenses ''CaseBranch diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 87fb9fea8e..cec7ae5a64 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -104,12 +104,17 @@ instance PrettyCode Binop where r <- ppRightExpression _binopFixity _binopRight return $ l <+> op <+> r +instance PrettyCode LetClause where + ppCode LetClause {..} = do + name <- ppCode _letClauseName + val <- ppCode _letClauseValue + return $ name <+> "=" <+> align val + instance PrettyCode Let where ppCode Let {..} = do - name <- ppCode _letVar - val <- ppCode _letValue + cls <- mapM ppCode _letClauses body <- ppCode _letBody - return $ align $ kwLet <> blockIndent (name <+> "=" <+> align val) <> kwIn <+> body + return $ align $ kwLet <> blockIndent (vsep (punctuate semi (toList cls))) <> kwIn <+> body instance PrettyCode If where ppCode If {..} = do diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index c9b7b9a791..262cb1f845 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -290,6 +290,18 @@ goModule onlyTypes infoTable Internal.Module {..} = nmap <- asks (^. nameMap) return $ fromMaybe name $ HashMap.lookup name nmap + localName :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => Name -> Name -> Sem r a -> Sem r a + localName v v' = + local (over nameSet (HashSet.insert (v' ^. namePretty))) + . local (over nameMap (HashMap.insert v v')) + + localNames :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => [(Name, Name)] -> Sem r a -> Sem r a + localNames vs e = foldl' (flip (uncurry localName)) e vs + + withLocalNames :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => NameSet -> NameMap -> Sem r a -> Sem r a + withLocalNames nset nmap = + local (const nset) . local (const nmap) + goExpression' :: Internal.Expression -> Expression goExpression' = goExpression'' (NameSet mempty) (NameMap mempty) @@ -314,7 +326,8 @@ goModule onlyTypes infoTable Internal.Module {..} = goIden :: Internal.Iden -> Sem r Expression goIden iden = case iden of Internal.IdenFunction name -> do - return $ ExprIden (goFunName name) + name' <- lookupName name + return $ ExprIden (goFunName name') Internal.IdenConstructor name -> case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of Just ctrInfo -> @@ -556,40 +569,49 @@ goModule onlyTypes infoTable Internal.Module {..} = -- TODO: binders goLet :: Internal.Let -> Sem r Expression - goLet Internal.Let {..} = go (concatMap toFunDefs (toList _letClauses)) + goLet Internal.Let {..} = do + let fdefs = concatMap toFunDefs (toList _letClauses) + cls <- mapM goFunDef fdefs + let ns = zipExact (map (^. Internal.funDefName) fdefs) (map (^. letClauseName) cls) + expr <- localNames ns $ goExpression _letExpression + return $ + ExprLet + Let + { _letClauses = nonEmpty' cls, + _letBody = expr + } where toFunDefs :: Internal.LetClause -> [Internal.FunctionDef] toFunDefs = \case Internal.LetFunDef d -> [d] Internal.LetMutualBlock Internal.MutualBlockLet {..} -> toList _mutualLet - go :: [Internal.FunctionDef] -> Sem r Expression - go = \case - d : defs' -> goFunDef d =<< go defs' - [] -> goExpression _letExpression - - goFunDef :: Internal.FunctionDef -> Expression -> Sem r Expression - goFunDef Internal.FunctionDef {..} expr = do - val <- goExpression _funDefBody + goFunDef :: Internal.FunctionDef -> Sem r LetClause + goFunDef Internal.FunctionDef {..} = do + nset <- asks (^. nameSet) + let name' = overNameText (disambiguate nset) _funDefName + val <- localName _funDefName name' $ goExpression _funDefBody return $ - ExprLet - Let - { _letVar = _funDefName, - _letValue = val, - _letBody = expr - } + LetClause + { _letClauseName = name', + _letClauseValue = val + } goUniverse :: Internal.SmallUniverse -> Sem r Expression goUniverse _ = return ExprUndefined - -- TODO: binders goSimpleLambda :: Internal.SimpleLambda -> Sem r Expression goSimpleLambda Internal.SimpleLambda {..} = do - body <- goExpression _slambdaBody + nset <- asks (^. nameSet) + let v = _slambdaBinder ^. Internal.sbinderVar + v' = overNameText (disambiguate nset) v + body <- + localName v v' $ + goExpression _slambdaBody return $ ExprLambda Lambda - { _lambdaVar = _slambdaBinder ^. Internal.sbinderVar, + { _lambdaVar = v', _lambdaType = Just $ goType $ _slambdaBinder ^. Internal.sbinderType, _lambdaBody = body } @@ -619,9 +641,8 @@ goModule onlyTypes infoTable Internal.Module {..} = nset <- asks (^. nameSet) let v' = overNameText (disambiguate nset) v body <- - local (over nameSet (HashSet.insert (v' ^. namePretty))) - . local (over nameMap (HashMap.insert v v')) - $ goLams vs + localName v v' $ + goLams vs return $ ExprLambda Lambda @@ -662,7 +683,7 @@ goModule onlyTypes infoTable Internal.Module {..} = { _tupleComponents = nonEmpty' pats } return (pat, nset, nmap) - body <- local (const nset) $ local (const nmap) $ goExpression _lambdaBody + body <- withLocalNames nset nmap $ goExpression _lambdaBody return $ CaseBranch { _caseBranchPattern = pat, @@ -683,7 +704,7 @@ goModule onlyTypes infoTable Internal.Module {..} = goCaseBranch :: Internal.CaseBranch -> Sem r CaseBranch goCaseBranch Internal.CaseBranch {..} = do (pat, nset, nmap) <- goPatternArg' _caseBranchPattern - rhs <- local (const nset) $ local (const nmap) $ goCaseBranchRhs _caseBranchRhs + rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs return $ CaseBranch { _caseBranchPattern = pat, @@ -861,7 +882,7 @@ goModule onlyTypes infoTable Internal.Module {..} = names :: HashSet Text names = HashSet.fromList $ - map (^. Internal.functionInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoFunctions)) + map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions))) ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors)) ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives)) ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms)) diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 52fd03c396..ead8de0b89 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -30,8 +30,8 @@ import Juvix.Compiler.Store.Internal.Data.TypesTable import Juvix.Compiler.Store.Internal.Language import Juvix.Prelude -functionInfoFromFunctionDef :: FunctionDef -> FunctionInfo -functionInfoFromFunctionDef FunctionDef {..} = +functionInfoFromFunctionDef :: Bool -> FunctionDef -> FunctionInfo +functionInfoFromFunctionDef isLocal FunctionDef {..} = FunctionInfo { _functionInfoName = _funDefName, _functionInfoType = _funDefType, @@ -40,7 +40,8 @@ functionInfoFromFunctionDef FunctionDef {..} = _functionInfoCoercion = _funDefCoercion, _functionInfoInstance = _funDefInstance, _functionInfoTerminating = _funDefTerminating, - _functionInfoPragmas = _funDefPragmas + _functionInfoPragmas = _funDefPragmas, + _functionInfoIsLocal = isLocal } inductiveInfoFromInductiveDef :: InductiveDef -> InductiveInfo @@ -62,7 +63,7 @@ extendWithReplExpression e = infoFunctions ( HashMap.union ( HashMap.fromList - [ (f ^. funDefName, functionInfoFromFunctionDef f) + [ (f ^. funDefName, functionInfoFromFunctionDef True f) | f <- letFunctionDefs e ] ) @@ -127,10 +128,10 @@ computeInternalModuleInfoTable m = InfoTable {..} _infoFunctions :: HashMap Name FunctionInfo _infoFunctions = HashMap.fromList $ - [ (f ^. funDefName, functionInfoFromFunctionDef f) + [ (f ^. funDefName, functionInfoFromFunctionDef False f) | StatementFunction f <- mutuals ] - <> [ (f ^. funDefName, functionInfoFromFunctionDef f) + <> [ (f ^. funDefName, functionInfoFromFunctionDef True f) | s <- ss, f <- letFunctionDefs s ] diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index 74f98df2bc..fa14921335 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs @@ -26,7 +26,8 @@ data FunctionInfo = FunctionInfo _functionInfoCoercion :: Bool, _functionInfoBuiltin :: Maybe BuiltinFunction, _functionInfoArgsInfo :: [ArgInfo], - _functionInfoPragmas :: Pragmas + _functionInfoPragmas :: Pragmas, + _functionInfoIsLocal :: Bool } deriving stock (Generic)