Skip to content

Commit

Permalink
Remove function clause from Internal (#2389)
Browse files Browse the repository at this point in the history
- closes #2363
  • Loading branch information
janmasrovira authored Sep 29, 2023
1 parent 0230a7b commit 2d4de1a
Show file tree
Hide file tree
Showing 15 changed files with 126 additions and 152 deletions.
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

0 comments on commit 2d4de1a

Please sign in to comment.