Skip to content

Commit

Permalink
multiple definitions in a let
Browse files Browse the repository at this point in the history
  • Loading branch information
@lukaszcz
lukaszcz committed Jul 12, 2024
1 parent 74977f5 commit 1afc43a
Show file tree
Hide file tree
Showing 5 changed files with 70 additions and 37 deletions.
9 changes: 7 additions & 2 deletions src/Juvix/Compiler/Backend/Isabelle/Language.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -132,6 +136,7 @@ data ConstrApp = ConstrApp

makeLenses ''Application
makeLenses ''Let
makeLenses ''LetClause
makeLenses ''If
makeLenses ''Case
makeLenses ''CaseBranch
Expand Down
11 changes: 8 additions & 3 deletions src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
71 changes: 46 additions & 25 deletions src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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 ->
Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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))
Expand Down
13 changes: 7 additions & 6 deletions src/Juvix/Compiler/Internal/Data/InfoTable.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -40,7 +40,8 @@ functionInfoFromFunctionDef FunctionDef {..} =
_functionInfoCoercion = _funDefCoercion,
_functionInfoInstance = _funDefInstance,
_functionInfoTerminating = _funDefTerminating,
_functionInfoPragmas = _funDefPragmas
_functionInfoPragmas = _funDefPragmas,
_functionInfoIsLocal = isLocal
}

inductiveInfoFromInductiveDef :: InductiveDef -> InductiveInfo
Expand All @@ -62,7 +63,7 @@ extendWithReplExpression e =
infoFunctions
( HashMap.union
( HashMap.fromList
[ (f ^. funDefName, functionInfoFromFunctionDef f)
[ (f ^. funDefName, functionInfoFromFunctionDef True f)
| f <- letFunctionDefs e
]
)
Expand Down Expand Up @@ -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
]
Expand Down
3 changes: 2 additions & 1 deletion src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,8 @@ data FunctionInfo = FunctionInfo
_functionInfoCoercion :: Bool,
_functionInfoBuiltin :: Maybe BuiltinFunction,
_functionInfoArgsInfo :: [ArgInfo],
_functionInfoPragmas :: Pragmas
_functionInfoPragmas :: Pragmas,
_functionInfoIsLocal :: Bool
}
deriving stock (Generic)

Expand Down

0 comments on commit 1afc43a

Please sign in to comment.