Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove function clause from Internal #2389

Merged
merged 12 commits into from
Sep 29, 2023
5 changes: 3 additions & 2 deletions src/Juvix/Compiler/Builtins/Effect.hs
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,9 @@ registerFun fi = do
a =% b = (a ==% b) freeVars
clauses :: [(Expression, Expression)]
clauses =
[ (clauseLhsAsExpression c, c ^. clauseBody)
| c <- toList (fi ^. funInfoDef . funDefClauses)
[ (clauseLhsAsExpression op (toList pats), body)
| Just cls <- [unfoldLambdaClauses (fi ^. funInfoDef . funDefBody)],
(pats, body) <- toList cls
]
case zipExactMay (fi ^. funInfoClauses) clauses of
Nothing -> error "builtin has the wrong number of clauses"
Expand Down
1 change: 1 addition & 0 deletions src/Juvix/Compiler/Concrete/Language.hs
Original file line number Diff line number Diff line change
Expand Up @@ -358,6 +358,7 @@ deriving stock instance (Ord (FixitySyntaxDef 'Scoped))
data FixityDef = FixityDef
{ _fixityDefSymbol :: S.Symbol,
_fixityDefFixity :: Fixity,
-- | Used internally for printing parentheses.
_fixityDefPrec :: Int
}
deriving stock (Show, Eq, Ord)
Expand Down
7 changes: 5 additions & 2 deletions src/Juvix/Compiler/Core/Translation/FromInternal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -312,7 +312,7 @@ preFunctionDef f = do
Nothing ->
map
getPatternName
(head (f ^. Internal.funDefClauses) ^. Internal.clausePatterns)
(fst (Internal.unfoldLambda (f ^. Internal.funDefBody)))

normalizeBuiltinName :: Maybe BuiltinFunction -> Text -> Text
normalizeBuiltinName blt name = case blt of
Expand Down Expand Up @@ -378,7 +378,10 @@ mkFunBody ::
Internal.FunctionDef ->
Sem r Node
mkFunBody ty f =
mkBody ty (f ^. Internal.funDefName . nameLoc) (fmap (\c -> (c ^. Internal.clausePatterns, c ^. Internal.clauseBody)) (f ^. Internal.funDefClauses))
mkBody
ty
(f ^. Internal.funDefName . nameLoc)
(pure (Internal.unfoldLambda (f ^. Internal.funDefBody)))

mkBody ::
forall r.
Expand Down
22 changes: 13 additions & 9 deletions src/Juvix/Compiler/Internal/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ genFieldProjection ::
Int ->
Sem r FunctionDef
genFieldProjection _funDefName info fieldIx = do
clause <- genClause
body' <- genBody
let (inductiveParams, constrArgs) = constructorArgTypes info
implicity = constructorImplicity info
saturatedTy = unnamedParameter' implicity (constructorReturnType info)
Expand All @@ -94,18 +94,22 @@ genFieldProjection _funDefName info fieldIx = do
_funDefInstance = False,
_funDefBuiltin = Nothing,
_funDefPragmas = mempty,
_funDefClauses = pure clause,
_funDefBody = body',
_funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
..
}
where
genClause :: Sem r FunctionClause
genClause = do
genBody :: Sem r Expression
genBody = do
(pat, vars) <- genConstructorPattern (getLoc _funDefName) info
let body = toExpression (vars !! fieldIx)
return
FunctionClause
{ _clauseName = _funDefName,
_clausePatterns = [pat],
_clauseBody = body
cl =
LambdaClause
{ _lambdaPatterns = pure pat,
_lambdaBody = body
}
return . ExpressionLambda $
Lambda
{ _lambdaType = Nothing,
_lambdaClauses = pure cl
}
32 changes: 20 additions & 12 deletions src/Juvix/Compiler/Internal/Extra/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -158,24 +158,17 @@ subsHoles s = over leafExpressions helper
ExpressionInstanceHole h -> fromMaybe e (s ^. at h)
_ -> e

instance HasExpressions FunctionClause where
leafExpressions f c = do
_clauseBody <- leafExpressions f (c ^. clauseBody)
_clausePatterns <- traverse (leafExpressions f) (c ^. clausePatterns)
pure FunctionClause {_clauseName = c ^. clauseName, ..}

instance HasExpressions Example where
leafExpressions f = traverseOf exampleExpression (leafExpressions f)

instance HasExpressions FunctionDef where
-- leafExpressions f (FunctionDef name ty clauses bi) = do
leafExpressions f FunctionDef {..} = do
clauses' <- traverse (leafExpressions f) _funDefClauses
body' <- leafExpressions f _funDefBody
ty' <- leafExpressions f _funDefType
examples' <- traverse (leafExpressions f) _funDefExamples
pure
FunctionDef
{ _funDefClauses = clauses',
{ _funDefBody = body',
_funDefType = ty',
_funDefExamples = examples',
_funDefTerminating,
Expand Down Expand Up @@ -316,6 +309,21 @@ viewConstructorType = first (map (^. paramType)) . unfoldFunType
constructorArgs :: Expression -> [Expression]
constructorArgs = fst . viewConstructorType

unfoldLambdaClauses :: Expression -> Maybe (NonEmpty (NonEmpty PatternArg, Expression))
unfoldLambdaClauses t = do
ExpressionLambda Lambda {..} <- return t
let mkClause :: LambdaClause -> (NonEmpty PatternArg, Expression)
mkClause LambdaClause {..} = first (appendList _lambdaPatterns) (unfoldLambda _lambdaBody)
return (mkClause <$> _lambdaClauses)

-- Unfolds *single* clause lambdas
unfoldLambda :: Expression -> ([PatternArg], Expression)
unfoldLambda t = case t of
ExpressionLambda Lambda {..}
| LambdaClause {..} :| [] <- _lambdaClauses ->
first (toList _lambdaPatterns <>) (unfoldLambda _lambdaBody)
_ -> ([], t)

-- | a -> (b -> c) ==> ([a, b], c)
unfoldFunType :: Expression -> ([FunctionParameter], Expression)
unfoldFunType t = case t of
Expand Down Expand Up @@ -513,9 +521,9 @@ leftEq a b free =
. evalState (mempty @(HashMap Name Name))
$ matchExpressions (toExpression a) (toExpression b)

clauseLhsAsExpression :: FunctionClause -> Expression
clauseLhsAsExpression cl =
foldApplication (toExpression (cl ^. clauseName)) (map toApplicationArg (cl ^. clausePatterns))
clauseLhsAsExpression :: Name -> [PatternArg] -> Expression
clauseLhsAsExpression clName pats =
foldApplication (toExpression clName) (map toApplicationArg pats)

infix 4 ==%

Expand Down
7 changes: 1 addition & 6 deletions src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,7 @@ goFunctionDefHelper f = do
when (f ^. funDefInstance) $
goInstance f
goExpression (Just (f ^. funDefName)) (f ^. funDefType)
mapM_ (goFunctionClause (f ^. funDefName)) (f ^. funDefClauses)
goExpression (Just (f ^. funDefName)) (f ^. funDefBody)

-- constructors of an inductive type depend on the inductive type, not the other
-- way round; an inductive type depends on the types of its constructors
Expand All @@ -204,11 +204,6 @@ goConstructorDef indName c = do
addEdge (c ^. inductiveConstructorName) indName
goExpression (Just indName) (c ^. inductiveConstructorType)

goFunctionClause :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionClause -> Sem r ()
goFunctionClause p c = do
mapM_ (goPattern (Just p)) (c ^. clausePatterns)
goExpression (Just p) (c ^. clauseBody)

goPattern :: forall r. (Member (State DependencyGraph) r) => Maybe Name -> PatternArg -> Sem r ()
goPattern n p = case p ^. patternArgPattern of
PatternVariable {} -> return ()
Expand Down
19 changes: 3 additions & 16 deletions src/Juvix/Compiler/Internal/Language.hs
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ data FunctionDef = FunctionDef
{ _funDefName :: FunctionName,
_funDefType :: Expression,
_funDefExamples :: [Example],
_funDefClauses :: NonEmpty FunctionClause,
_funDefBody :: Expression,
_funDefTerminating :: Bool,
_funDefInstance :: Bool,
_funDefBuiltin :: Maybe BuiltinFunction,
Expand All @@ -96,15 +96,6 @@ data FunctionDef = FunctionDef

instance Hashable FunctionDef

data FunctionClause = FunctionClause
{ _clauseName :: FunctionName,
_clausePatterns :: [PatternArg],
_clauseBody :: Expression
}
deriving stock (Eq, Generic, Data)

instance Hashable FunctionClause

data Iden
= IdenFunction Name
| IdenConstructor Name
Expand Down Expand Up @@ -214,7 +205,7 @@ data Lambda = Lambda
deriving stock (Eq, Generic, Data)

data LambdaClause = LambdaClause
{ _lambdaPatterns :: NonEmpty PatternArg, -- only explicit patterns are allowed
{ _lambdaPatterns :: NonEmpty PatternArg,
_lambdaBody :: Expression
}
deriving stock (Eq, Generic, Data)
Expand Down Expand Up @@ -327,7 +318,6 @@ makeLenses ''Example
makeLenses ''PatternArg
makeLenses ''Import
makeLenses ''FunctionDef
makeLenses ''FunctionClause
makeLenses ''InductiveDef
makeLenses ''AxiomDef
makeLenses ''ModuleBody'
Expand Down Expand Up @@ -438,11 +428,8 @@ instance HasLoc LambdaClause where
instance HasLoc Lambda where
getLoc l = getLocSpan (l ^. lambdaClauses)

instance HasLoc FunctionClause where
getLoc f = getLoc (f ^. clauseName) <> getLoc (f ^. clauseBody)

instance HasLoc FunctionDef where
getLoc f = getLoc (f ^. funDefName) <> getLocSpan (f ^. funDefClauses)
getLoc f = getLoc (f ^. funDefName) <> getLoc (f ^. funDefBody)

instance HasLoc MutualBlockLet where
getLoc (MutualBlockLet defs) = getLocSpan defs
Expand Down
12 changes: 2 additions & 10 deletions src/Juvix/Compiler/Internal/Pretty/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -238,26 +238,18 @@ instance PrettyCode FunctionDef where
builtin' <- fmap (kwBuiltin <+>) <$> mapM ppCode (f ^. funDefBuiltin)
funDefName' <- ppCode (f ^. funDefName)
funDefType' <- ppCode (f ^. funDefType)
clauses' <- mapM ppCode (f ^. funDefClauses)
body' <- ppCode (f ^. funDefBody)
return $
builtin'
<?+> funDefName'
<+> kwColon
<+> funDefType'
<> hardline
<> vsep (toList clauses')
<> oneLineOrNext (kwAssign <+> body')

instance PrettyCode PreLetStatement where
ppCode = \case
PreLetFunctionDef f -> ppCode f

instance PrettyCode FunctionClause where
ppCode c = do
funName <- ppCode (c ^. clauseName)
clausePatterns' <- hsepMaybe <$> mapM ppCodeAtom (c ^. clausePatterns)
clauseBody' <- ppCode (c ^. clauseBody)
return $ nest 2 (funName <+?> clausePatterns' <+> kwAssign <+> clauseBody')

instance PrettyCode Import where
ppCode i = do
name' <- ppCode (i ^. importModule . moduleIxModule . moduleName)
Expand Down
32 changes: 19 additions & 13 deletions src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -435,28 +435,34 @@ goTopFunctionDef FunctionDef {..} = do
_funDefType <- goDefType
_funDefExamples <- goExamples _signDoc
_funDefPragmas <- goPragmas _signPragmas
_funDefClauses <- goBody
_funDefBody <- goBody
let fun = Internal.FunctionDef {..}
whenJust _signBuiltin (registerBuiltinFunction fun . (^. withLocParam))
return fun
where
goBody :: Sem r (NonEmpty Internal.FunctionClause)
goBody :: Sem r Internal.Expression
goBody = do
commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs
let _clauseName = goSymbol _signName
goClause :: FunctionClause 'Scoped -> Sem r Internal.FunctionClause
let goClause :: FunctionClause 'Scoped -> Sem r Internal.LambdaClause
goClause FunctionClause {..} = do
let _clauseName = goSymbol _signName
_clauseBody <- goExpression _clausenBody
extraPatterns <- toList <$> (mapM goPatternArg _clausenPatterns)
let _clausePatterns = commonPatterns <> extraPatterns
return Internal.FunctionClause {..}
_lambdaBody <- goExpression _clausenBody
extraPatterns <- mapM goPatternArg _clausenPatterns
let _lambdaPatterns = prependList commonPatterns extraPatterns
return Internal.LambdaClause {..}
case _signBody of
SigBodyExpression body -> do
_clauseBody <- goExpression body
let _clausePatterns = commonPatterns
return (pure Internal.FunctionClause {..})
SigBodyClauses cls -> mapM goClause cls
body' <- goExpression body
return $ case nonEmpty commonPatterns of
Nothing -> body'
Just _lambdaPatterns -> do
let _lambdaBody = body'
_lambdaType :: Maybe Internal.Expression = Nothing
_lambdaClauses = pure Internal.LambdaClause {..}
Internal.ExpressionLambda Internal.Lambda {..}
SigBodyClauses cls -> do
_lambdaClauses <- mapM goClause cls
let _lambdaType :: Maybe Internal.Expression = Nothing
return (Internal.ExpressionLambda Internal.Lambda {..})

goDefType :: Sem r Internal.Expression
goDefType = do
Expand Down
Loading