Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@janmasrovira
janmasrovira committed Sep 12, 2024
1 parent 26ea94b commit c627acc
Showing 1 changed file with 167 additions and 74 deletions.
241 changes: 167 additions & 74 deletions src/Juvix/Compiler/Concrete/Translation/FromSource.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,30 @@ import Juvix.Prelude.Pretty
prettyText,
)

data FunctionSyntaxOptions = FunctionSyntaxOptions
{ _funAllowOmitType :: Bool,
_funAllowInstance :: Bool
}

data FunctionLhs = FunctionLhs
{ _funLhsInstance :: Maybe KeywordRef,
_funLhsCoercion :: Maybe KeywordRef,
_funLhsName :: FunctionName 'Parsed,
_funLhsArgs :: [SigArg 'Parsed],
_funLhsColonKw :: Irrelevant (Maybe KeywordRef),
_funLhsRetType :: Maybe (ExpressionType 'Parsed),
_funLhsTerminating :: Maybe KeywordRef,
_funLhsAfterLastArgOff :: Int
}

data MdModuleBuilder = MdModuleBuilder
{ _mdModuleBuilder :: Module 'Parsed 'ModuleTop,
_mdModuleBuilderBlocksLengths :: [Int]
}

makeLenses ''MdModuleBuilder
makeLenses ''FunctionLhs
makeLenses ''FunctionSyntaxOptions

type JudocStash = State (Maybe (Judoc 'Parsed))

Expand Down Expand Up @@ -390,13 +408,13 @@ replInput =
-- Symbols and names
--------------------------------------------------------------------------------

symbol :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Symbol
symbol :: (Members '[ParserResultBuilder] r) => ParsecS r Symbol
symbol = uncurry (flip WithLoc) <$> identifierL

dottedSymbol :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (NonEmpty Symbol)
dottedSymbol :: (Members '[ParserResultBuilder] r) => ParsecS r (NonEmpty Symbol)
dottedSymbol = fmap (uncurry (flip WithLoc)) <$> dottedIdentifier

name :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Name
name :: (Members '[ParserResultBuilder] r) => ParsecS r Name
name = do
parts <- dottedSymbol
return $ case nonEmptyUnsnoc parts of
Expand Down Expand Up @@ -467,10 +485,25 @@ l <?|> r = do
r
P.withRecovery (const recover) (P.try l)

recoverStashes :: (Members '[PragmasStash, JudocStash] r) => ParsecS r a -> ParsecS r a
recoverStashes r = do
p <- P.lift (get @(Maybe ParsedPragmas))
j <- P.lift (get @(Maybe (Judoc 'Parsed)))
res <- r
P.lift $ do
put p
put j
return res

statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Statement 'Parsed)
statement = P.label "<top level statement>" $ do
optional_ stashJudoc
optional_ stashPragmas
let funSyntax =
FunctionSyntaxOptions
{ _funAllowInstance = True,
_funAllowOmitType = False
}
ms <-
optional
( StatementImport <$> import_
Expand All @@ -480,7 +513,7 @@ statement = P.label "<top level statement>" $ do
<|> StatementModule <$> moduleDef
<|> StatementAxiom <$> axiomDef Nothing
<|> builtinStatement
<|> StatementFunctionDef <$> functionDefinition False True Nothing
<|> StatementFunctionDef <$> functionDefinition funSyntax Nothing
)
case ms of
Just s -> return s
Expand Down Expand Up @@ -649,7 +682,13 @@ builtinFunctionDef ::
(Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
WithLoc BuiltinFunction ->
ParsecS r (FunctionDef 'Parsed)
builtinFunctionDef = functionDefinition False True . Just
builtinFunctionDef = functionDefinition funSyntax . Just
where
funSyntax =
FunctionSyntaxOptions
{ _funAllowInstance = True,
_funAllowOmitType = False
}

builtinStatement :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Statement 'Parsed)
builtinStatement = do
Expand Down Expand Up @@ -988,7 +1027,12 @@ pnamedArgumentFunctionDef ::
pnamedArgumentFunctionDef = do
optional_ stashJudoc
optional_ stashPragmas
fun <- functionDefinition True False Nothing
let funSyntax =
FunctionSyntaxOptions
{ _funAllowOmitType = True,
_funAllowInstance = False
}
fun <- functionDefinition funSyntax Nothing
return
NamedArgumentFunctionDef
{ _namedArgumentFunctionDef = fun
Expand Down Expand Up @@ -1165,7 +1209,13 @@ letFunDef ::
ParsecS r (FunctionDef 'Parsed)
letFunDef = do
optional_ stashPragmas
functionDefinition True False Nothing
functionDefinition funSyntax Nothing
where
funSyntax =
FunctionSyntaxOptions
{ _funAllowOmitType = True,
_funAllowInstance = False
}

letStatement :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (LetStatement 'Parsed)
letStatement =
Expand Down Expand Up @@ -1356,87 +1406,113 @@ getPragmas = P.lift $ do
put (Nothing @ParsedPragmas)
return j

functionDefinition ::
forall r.
(Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
Bool ->
Bool ->
Maybe (WithLoc BuiltinFunction) ->
ParsecS r (FunctionDef 'Parsed)
functionDefinition allowOmitType allowInstance _signBuiltin = P.label "<function definition>" $ do
_signTerminating <- optional (kw kwTerminating)
functionDefinitionLhs :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => FunctionSyntaxOptions -> ParsecS r FunctionLhs
functionDefinitionLhs opts = P.label "<function definition>" $ do
let allowInstance = opts ^. funAllowInstance
allowOmitType = opts ^. funAllowOmitType
_funLhsTerminating <- optional (kw kwTerminating)
off <- P.getOffset
_signCoercion <- optional (kw kwCoercion)
unless (allowInstance || isNothing _signCoercion) $
_funLhsCoercion <- optional (kw kwCoercion)
unless (allowInstance || isNothing _funLhsCoercion) $
parseFailure off "coercion not allowed here"
off0 <- P.getOffset
_signInstance <- optional (kw kwInstance)
unless (allowInstance || isNothing _signInstance) $
_funLhsInstance <- optional (kw kwInstance)
unless (allowInstance || isNothing _funLhsInstance) $
parseFailure off0 "instance not allowed here"
when (isJust _signCoercion && isNothing _signInstance) $
when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
parseFailure off0 "expected: instance"
_signName <- symbol
_signArgs <- many parseArg
off' <- P.getOffset
_signColonKw <-
_funLhsName <- symbol
_funLhsArgs <- many parseArg
_funLhsAfterLastArgOff <- P.getOffset
_funLhsColonKw <-
Irrelevant
<$> if
| allowOmitType -> optional (kw kwColon)
| otherwise -> Just <$> kw kwColon
_signRetType <-
case _signColonKw ^. unIrrelevant of
_funLhsRetType <-
case _funLhsColonKw ^. unIrrelevant of
Just {} -> Just <$> parseExpressionAtoms
Nothing -> return Nothing
return
FunctionLhs
{ _funLhsInstance,
_funLhsCoercion,
_funLhsAfterLastArgOff,
_funLhsName,
_funLhsArgs,
_funLhsColonKw,
_funLhsRetType,
_funLhsTerminating
}

parseArg :: forall r. (Members '[ParserResultBuilder, JudocStash, PragmasStash] r) => ParsecS r (SigArg 'Parsed)
parseArg = do
(openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do
(opn, impl) <- implicitOpen
let parseArgumentName :: ParsecS r (Argument 'Parsed) =
ArgumentSymbol <$> symbol
<|> ArgumentWildcard <$> wildcard
let parseArgumentNameColon :: ParsecS r (Argument 'Parsed, Irrelevant KeywordRef) = P.try $ do
n <- parseArgumentName
c <- Irrelevant <$> kw kwColon
return (n, c)
(ns :: SigArgNames 'Parsed, c) <- case impl of
ImplicitInstance -> do
ma <- optional parseArgumentNameColon
return $ case ma of
Just (ns', c') -> (SigArgNames (pure ns'), Just c')
Nothing -> (SigArgNamesInstance, Nothing)
Implicit -> do
ns <- SigArgNames <$> some1 parseArgumentName
c <- optional (Irrelevant <$> kw kwColon)
return (ns, c)
Explicit -> do
ns <- SigArgNames <$> some1 parseArgumentName
c <- Just . Irrelevant <$> kw kwColon
return (ns, c)
return (opn, ns, impl, c)
_sigArgType <- case _sigArgImplicit of
Implicit
| isNothing _sigArgColon ->
return Nothing
_ ->
Just <$> parseExpressionAtoms
_sigArgDefault <- optional $ do
_argDefaultAssign <- Irrelevant <$> kw kwAssign
_argDefaultValue <- parseExpressionAtoms
return ArgDefault {..}
closeDelim <- implicitClose _sigArgImplicit
let _sigArgDelims = Irrelevant (openDelim, closeDelim)
return SigArg {..}

functionDefinition ::
forall r.
(Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
FunctionSyntaxOptions ->
Maybe (WithLoc BuiltinFunction) ->
ParsecS r (FunctionDef 'Parsed)
functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
FunctionLhs {..} <- functionDefinitionLhs opts
_signDoc <- getJudoc
_signPragmas <- getPragmas
_signBody <- parseBody
unless
( isJust (_signColonKw ^. unIrrelevant)
|| (P.isBodyExpression _signBody && null _signArgs)
( isJust (_funLhsColonKw ^. unIrrelevant)
|| (P.isBodyExpression _signBody && null _funLhsArgs)
)
$ parseFailure off' "expected result type"
return FunctionDef {..}
$ parseFailure _funLhsAfterLastArgOff "expected result type"
return
FunctionDef
{ _signName = _funLhsName,
_signArgs = _funLhsArgs,
_signColonKw = _funLhsColonKw,
_signRetType = _funLhsRetType,
_signTerminating = _funLhsTerminating,
_signInstance = _funLhsInstance,
_signCoercion = _funLhsCoercion,
..
}
where
parseArg :: ParsecS r (SigArg 'Parsed)
parseArg = do
(openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do
(opn, impl) <- implicitOpen
let parseArgumentName :: ParsecS r (Argument 'Parsed) =
ArgumentSymbol <$> symbol
<|> ArgumentWildcard <$> wildcard
let parseArgumentNameColon :: ParsecS r (Argument 'Parsed, Irrelevant KeywordRef) = P.try $ do
n <- parseArgumentName
c <- Irrelevant <$> kw kwColon
return (n, c)
(ns :: SigArgNames 'Parsed, c) <- case impl of
ImplicitInstance -> do
ma <- optional parseArgumentNameColon
return $ case ma of
Just (ns', c') -> (SigArgNames (pure ns'), Just c')
Nothing -> (SigArgNamesInstance, Nothing)
Implicit -> do
ns <- SigArgNames <$> some1 parseArgumentName
c <- optional (Irrelevant <$> kw kwColon)
return (ns, c)
Explicit -> do
ns <- SigArgNames <$> some1 parseArgumentName
c <- Just . Irrelevant <$> kw kwColon
return (ns, c)
return (opn, ns, impl, c)
_sigArgType <- case _sigArgImplicit of
Implicit
| isNothing _sigArgColon ->
return Nothing
_ ->
Just <$> parseExpressionAtoms
_sigArgDefault <- optional $ do
_argDefaultAssign <- Irrelevant <$> kw kwAssign
_argDefaultValue <- parseExpressionAtoms
return ArgDefault {..}
closeDelim <- implicitClose _sigArgImplicit
let _sigArgDelims = Irrelevant (openDelim, closeDelim)
return SigArg {..}

parseBody :: ParsecS r (FunctionDefBody 'Parsed)
parseBody =
SigBodyExpression <$> bodyExpr
Expand Down Expand Up @@ -1480,7 +1556,7 @@ implicitOpenField =
(,ImplicitInstanceField) <$> kw delimDoubleBraceL
<|> (,ExplicitField) <$> kw delimParenL

implicitOpen :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (KeywordRef, IsImplicit)
implicitOpen :: (Members '[ParserResultBuilder] r) => ParsecS r (KeywordRef, IsImplicit)
implicitOpen =
(,ImplicitInstance) <$> kw delimDoubleBraceL
<|> (,Implicit) <$> kw delimBraceL
Expand Down Expand Up @@ -1654,7 +1730,7 @@ constructorDef _constructorInductiveName _constructorPipe = do
_constructorRhs <- pconstructorRhs
return ConstructorDef {..}

wildcard :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Wildcard
wildcard :: (Members '[ParserResultBuilder] r) => ParsecS r Wildcard
wildcard = Wildcard . snd <$> interval (kw kwWildcard)

patternAtomWildcardConstructor :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (WildcardConstructor 'Parsed)
Expand All @@ -1666,12 +1742,29 @@ patternAtomWildcardConstructor = P.try $ do
let _wildcardConstructorDelims = Irrelevant (l, r)
return WildcardConstructor {..}

-- | Used to report better errors when the user forgets the @ on a named
-- application. It tries to parse the lhs of a function definition (up to the
-- :=). If it succeeds, it reports an error.
checkNoNamedApplication :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r ()
checkNoNamedApplication = recoverStashes . P.try $ do
off <- P.getOffset
let funSyntax =
FunctionSyntaxOptions
{ _funAllowOmitType = True,
_funAllowInstance = False
}
lhs <- functionDefinitionLhs funSyntax
let funWord
| null (lhs ^. funLhsArgs) = "assignment"
| otherwise = "function definition"
parseFailure off ("Unexpected " <> funWord <> ".\nPerhaps you intended to use the @{ .. } syntax for named applications?")

patternAtomAnon :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
patternAtomAnon =
PatternAtomWildcard <$> wildcard
<|> PatternAtomDoubleBraces <$> doubleBraces parsePatternAtomsNested
<|> PatternAtomParens <$> parens parsePatternAtomsNested
<|> PatternAtomBraces <$> braces parsePatternAtomsNested
<|> PatternAtomBraces <$> braces (checkNoNamedApplication >> parsePatternAtomsNested)
<|> PatternAtomList <$> parseListPattern

patternAtomAt :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Symbol -> ParsecS r PatternBinding
Expand Down

0 comments on commit c627acc

Please sign in to comment.