anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-03 13:03:25 +03:00
Code Issues Projects Releases Wiki Activity

Support implicit arguments (#144)

Browse Source 
* work in progress towards implicit arguments

* Wip towards implicit types

* improve arity checker

* Add version of SimpleFungibleToken with implicit arguments

* guess arity of body before checking the lhs of a clause

* add ArityUnknown and fix some tests

* wip: proper errors in arity checker

* fix bugs, improve errors and add tests

* format

* set hlint version to 3.4 in the ci

* update pre-commit version to 3.0.0

* minor changes

* added more revisions

* minor

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This commit is contained in:
janmasrovira 2022-06-13 14:25:22 +02:00 committed by GitHub
parent 3396c52fa2
commit 2cf3f85439
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
73 changed files with 1647 additions and 821 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
.github/workflows/ci.yml vendored
View File

@ -72,7 +72,7 @@ jobs:
- name: 'Set up HLint'
uses: rwe/actions-hlint-setup@v1
with:
version: '3.1.6'
version: '3.4'
- name: 'Run HLint'
uses: rwe/actions-hlint-run@v2.0.1
with:
@ -84,27 +84,27 @@ jobs:
steps:
- uses: actions/checkout@v2
- uses: actions/setup-python@v2
- uses: pre-commit/action@v2.0.3
- uses: pre-commit/action@v3.0.0
with:
extra_args:
trailing-whitespace --all-files
- uses: pre-commit/action@v2.0.3
- uses: pre-commit/action@v3.0.0
with:
extra_args:
end-of-file-fixer --all-files
- uses: pre-commit/action@v2.0.3
- uses: pre-commit/action@v3.0.0
with:
extra_args:
check-yaml --all-files
- uses: pre-commit/action@v2.0.3
- uses: pre-commit/action@v3.0.0
with:
extra_args:
check-added-large-files --all-files
- uses: pre-commit/action@v2.0.3
- uses: pre-commit/action@v3.0.0
with:
extra_args:
check-case-conflict --all-files
- uses: pre-commit/action@v2.0.3
- uses: pre-commit/action@v3.0.0
with:
extra_args:
mixed-line-ending --all-files

2
app/App.hs
View File

@ -30,7 +30,7 @@ runAppIO g = interpret $ \case
| g ^. globalOnlyErrors -> return ()
| otherwise -> embed (putStrLn t)
ExitMiniJuvixError e -> do
(embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors))) e
(embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors)) (g ^. globalOnlyErrors)) e
embed exitFailure
ExitMsg exitCode t -> embed (putStrLn t >> exitWith exitCode)

11
app/Commands/MicroJuvix.hs
View File

@ -6,6 +6,7 @@ import Options.Applicative
data MicroJuvixCommand
= Pretty
| TypeCheck MicroJuvixTypeOptions
| Arity
newtype MicroJuvixTypeOptions = MicroJuvixTypeOptions
{ _microJuvixTypePrint :: Bool
@ -18,15 +19,25 @@ parseMicroJuvixCommand =
hsubparser $
mconcat
[ commandPretty,
commandArity,
commandTypeCheck
]
where
commandArity :: Mod CommandFields MicroJuvixCommand
commandArity = command "arity" arityInfo
commandPretty :: Mod CommandFields MicroJuvixCommand
commandPretty = command "pretty" prettyInfo
commandTypeCheck :: Mod CommandFields MicroJuvixCommand
commandTypeCheck = command "typecheck" typeCheckInfo
arityInfo :: ParserInfo MicroJuvixCommand
arityInfo =
info
(pure Arity)
(progDesc "Translate a MiniJuvix file to MicroJuvix and insert holes")
prettyInfo :: ParserInfo MicroJuvixCommand
prettyInfo =
info

4
app/Main.hs
View File

@ -19,6 +19,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper
import MiniJuvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as MicroArity
import MiniJuvix.Syntax.MicroJuvix.Pretty qualified as Micro
import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroTyped
import MiniJuvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
@ -133,6 +134,9 @@ runCommand cmdWithOpts = do
{ Micro._optShowNameIds = globalOpts ^. globalShowNameIds
}
App.renderStdOut (Micro.ppOut ppOpts micro)
MicroJuvix Arity -> do
micro <- head . (^. MicroArity.resultModules) <$> runPipeline (upToMicroJuvixArity entryPoint)
App.renderStdOut (Micro.ppOut Micro.defaultOptions micro)
MicroJuvix (TypeCheck localOpts) -> do
res <- runPipeline (upToMicroJuvixTyped entryPoint)
say "Well done! It type checks"

1
minijuvix-mode/minijuvix-mode.el
View File

@ -29,6 +29,7 @@
(with-eval-after-load 'evil
(evil-define-key 'normal minijuvix-mode-map (kbd "SPC m l") 'minijuvix-load)
(evil-define-key 'normal minijuvix-mode-map (kbd "SPC m g") 'minijuvix-goto-definition)
(evil-define-key 'normal minijuvix-mode-map (kbd "g d") 'minijuvix-goto-definition)
(evil-normalize-keymaps))))
)

20
src/MiniJuvix/Pipeline.hs
View File

@ -13,6 +13,7 @@ import MiniJuvix.Prelude
import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
import MiniJuvix.Syntax.Concrete.Parser qualified as Parser
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
import MiniJuvix.Syntax.MicroJuvix.ArityChecker qualified as MicroJuvix
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix
import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroJuvix
@ -77,11 +78,17 @@ upToMicroJuvix ::
Sem r MicroJuvix.MicroJuvixResult
upToMicroJuvix = upToAbstract >=> pipelineMicroJuvix
upToMicroJuvixArity ::
Members '[Files, NameIdGen, Error MiniJuvixError] r =>
EntryPoint ->
Sem r MicroJuvix.MicroJuvixArityResult
upToMicroJuvixArity = upToMicroJuvix >=> pipelineMicroJuvixArity
upToMicroJuvixTyped ::
Members '[Files, NameIdGen, Error MiniJuvixError] r =>
EntryPoint ->
Sem r MicroJuvix.MicroJuvixTypedResult
upToMicroJuvixTyped = upToMicroJuvix >=> pipelineMicroJuvixTyped
upToMicroJuvixTyped = upToMicroJuvixArity >=> pipelineMicroJuvixTyped
upToMonoJuvix ::
Members '[Files, NameIdGen, Error MiniJuvixError] r =>
@ -116,9 +123,10 @@ pipelineScoper ::
pipelineScoper = mapError (MiniJuvixError @Scoper.ScoperError) . Scoper.entryScoper
pipelineAbstract ::
Members '[Error MiniJuvixError] r =>
Scoper.ScoperResult ->
Sem r Abstract.AbstractResult
pipelineAbstract = Abstract.entryAbstract
pipelineAbstract = mapError (MiniJuvixError @Scoper.ScoperError) . Abstract.entryAbstract
pipelineMicroJuvix ::
Members '[Error MiniJuvixError] r =>
@ -126,9 +134,15 @@ pipelineMicroJuvix ::
Sem r MicroJuvix.MicroJuvixResult
pipelineMicroJuvix = mapError (MiniJuvixError @MicroJuvix.TerminationError) . MicroJuvix.entryMicroJuvix
pipelineMicroJuvixArity ::
Members '[Error MiniJuvixError, NameIdGen] r =>
MicroJuvix.MicroJuvixResult ->
Sem r MicroJuvix.MicroJuvixArityResult
pipelineMicroJuvixArity = mapError (MiniJuvixError @MicroJuvix.ArityCheckerError) . MicroJuvix.entryMicroJuvixArity
pipelineMicroJuvixTyped ::
Members '[Files, NameIdGen, Error MiniJuvixError] r =>
MicroJuvix.MicroJuvixResult ->
MicroJuvix.MicroJuvixArityResult ->
Sem r MicroJuvix.MicroJuvixTypedResult
pipelineMicroJuvixTyped =
mapError (MiniJuvixError @MicroJuvix.TypeCheckerError) . MicroJuvix.entryMicroJuvixTyped

16
src/MiniJuvix/Prelude/Error/GenericError.hs
View File

@ -38,13 +38,13 @@ class ToGenericError a where
errorIntervals :: ToGenericError e => e -> [Interval]
errorIntervals = (^. genericErrorIntervals) . genericError
render :: ToGenericError e => Bool -> e -> Text
render ansi err
render :: ToGenericError e => Bool -> Bool -> e -> Text
render ansi endChar err
| ansi = helper Ansi.renderStrict (toAnsiDoc gMsg)
| otherwise = helper renderStrict (toTextDoc gMsg)
where
helper :: (SimpleDocStream a -> Text) -> Doc a -> Text
helper f x = (f . layoutPretty defaultLayoutOptions) (header <> x <> endChar)
helper f x = (f . layoutPretty defaultLayoutOptions) (header <> x <> lastChar)
g :: GenericError
g = genericError err
@ -55,16 +55,18 @@ render ansi err
header :: Doc a
header = genericErrorHeader g
endChar :: Doc a
endChar = "ת"
lastChar :: Doc a
lastChar
| endChar = "ת"
| otherwise = ""
-- | Render the error to Text.
renderText :: ToGenericError e => e -> Text
renderText = render False
renderText = render False False
-- | Render the error with Ansi formatting (if any).
renderAnsiText :: ToGenericError e => e -> Text
renderAnsiText = render True
renderAnsiText = render True False
printErrorAnsi :: ToGenericError e => e -> IO ()
printErrorAnsi = hPutStrLn stderr . renderAnsiText

16
src/MiniJuvix/Prelude/Pretty.hs
View File

@ -87,3 +87,19 @@ hsepMaybe :: Foldable f => f (Doc a) -> Maybe (Doc a)
hsepMaybe l
| null l = Nothing
| otherwise = Just (hsep l)
ordinal :: Int -> Doc a
ordinal = \case
1 -> "first"
2 -> "second"
3 -> "third"
4 -> "fourth"
5 -> "fifth"
6 -> "sixth"
7 -> "seventh"
8 -> "eighth"
9 -> "ninth"
10 -> "tenth"
11 -> "eleventh"
12 -> "twelfth"
n -> pretty n <> "th"

13
src/MiniJuvix/Syntax/Abstract/Language.hs
View File

@ -2,6 +2,8 @@ module MiniJuvix.Syntax.Abstract.Language
( module MiniJuvix.Syntax.Abstract.Language,
module MiniJuvix.Syntax.Concrete.Language,
module MiniJuvix.Syntax.Hole,
module MiniJuvix.Syntax.Wildcard,
module MiniJuvix.Syntax.IsImplicit,
)
where
@ -11,7 +13,9 @@ import MiniJuvix.Syntax.Concrete.Name qualified as C
import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
import MiniJuvix.Syntax.Fixity
import MiniJuvix.Syntax.Hole
import MiniJuvix.Syntax.IsImplicit
import MiniJuvix.Syntax.Universe
import MiniJuvix.Syntax.Wildcard
type TopModuleName = S.TopModulePath
@ -110,7 +114,7 @@ data Expression
deriving stock (Eq, Show)
instance HasAtomicity Expression where
atomicity e = case e of
atomicity = \case
ExpressionIden {} -> Atom
ExpressionHole {} -> Atom
ExpressionUniverse u -> atomicity u
@ -132,7 +136,8 @@ data MatchAlt = MatchAlt
data Application = Application
{ _appLeft :: Expression,
_appRight :: Expression
_appRight :: Expression,
_appImplicit :: IsImplicit
}
deriving stock (Eq, Show)
@ -152,6 +157,7 @@ data LambdaClause = LambdaClause
data FunctionParameter = FunctionParameter
{ _paramName :: Maybe VarName,
_paramUsage :: Usage,
_paramImplicit :: IsImplicit,
_paramType :: Expression
}
deriving stock (Eq, Show)
@ -175,8 +181,9 @@ data ConstructorApp = ConstructorApp
data Pattern
= PatternVariable VarName
| PatternConstructorApp ConstructorApp
| PatternWildcard
| PatternWildcard Wildcard
| PatternEmpty
| PatternBraces Pattern
deriving stock (Eq, Show)
data InductiveDef = InductiveDef

6
src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
View File

@ -8,10 +8,11 @@ import MiniJuvix.Prelude
import MiniJuvix.Syntax.Abstract.Language
patternVariables :: Pattern -> [VarName]
patternVariables pat = case pat of
patternVariables = \case
PatternVariable v -> [v]
PatternWildcard {} -> []
PatternEmpty {} -> []
PatternBraces b -> patternVariables b
PatternConstructorApp app -> appVariables app
appVariables :: ConstructorApp -> [VarName]
@ -20,13 +21,14 @@ appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
smallerPatternVariables :: Pattern -> [VarName]
smallerPatternVariables = \case
PatternVariable {} -> []
PatternBraces b -> smallerPatternVariables b
PatternWildcard {} -> []
PatternEmpty {} -> []
PatternConstructorApp app -> appVariables app
viewApp :: Expression -> (Expression, [Expression])
viewApp e = case e of
ExpressionApplication (Application l r) ->
ExpressionApplication (Application l r _) ->
second (`snoc` r) (viewApp l)
_ -> (e, [])

13
src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
View File

@ -73,6 +73,11 @@ kwColonOmega = keyword Str.colonOmegaUnicode
parensCond :: Bool -> Doc Ann -> Doc Ann
parensCond t d = if t then parens d else d
implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann
implicitDelim = \case
Implicit -> braces
Explicit -> parens
ppPostExpression ::
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
Fixity ->
@ -116,9 +121,11 @@ instance PrettyCode Iden where
ppCode = ppSCode . idenName
instance PrettyCode Application where
ppCode (Application l r) = do
ppCode (Application l r i) = do
l' <- ppLeftExpression appFixity l
r' <- ppRightExpression appFixity r
r' <- case i of
Explicit -> ppRightExpression appFixity r
Implicit -> implicitDelim i <$> ppCode r
return $ l' <+> r'
instance PrettyCode Universe where
@ -147,7 +154,7 @@ instance PrettyCode FunctionParameter where
paramName' <- ppSCode n
paramType' <- ppCode _paramType
paramUsage' <- ppCode _paramUsage
return $ parens (paramName' <+> paramUsage' <+> paramType')
return $ implicitDelim _paramImplicit (paramName' <+> paramUsage' <+> paramType')
instance PrettyCode Function where
ppCode Function {..} = do

17
src/MiniJuvix/Syntax/Concrete/Language.hs
View File

@ -7,12 +7,14 @@ module MiniJuvix.Syntax.Concrete.Language
module MiniJuvix.Syntax.Concrete.Loc,
module MiniJuvix.Syntax.Hole,
module MiniJuvix.Syntax.Concrete.LiteralLoc,
module MiniJuvix.Syntax.IsImplicit,
module MiniJuvix.Syntax.Backends,
module MiniJuvix.Syntax.ForeignBlock,
module MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn,
module MiniJuvix.Syntax.Concrete.PublicAnn,
module MiniJuvix.Syntax.Concrete.ModuleIsTop,
module MiniJuvix.Syntax.Concrete.Language.Stage,
module MiniJuvix.Syntax.Wildcard,
module MiniJuvix.Syntax.Fixity,
module MiniJuvix.Syntax.Usage,
module MiniJuvix.Syntax.Universe,
@ -36,8 +38,10 @@ import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
import MiniJuvix.Syntax.Fixity
import MiniJuvix.Syntax.ForeignBlock
import MiniJuvix.Syntax.Hole
import MiniJuvix.Syntax.IsImplicit
import MiniJuvix.Syntax.Universe
import MiniJuvix.Syntax.Usage
import MiniJuvix.Syntax.Wildcard
import Prelude (show)
--------------------------------------------------------------------------------
@ -280,7 +284,8 @@ data Pattern
| PatternApplication PatternApp
| PatternInfixApplication PatternInfixApp
| PatternPostfixApplication PatternPostfixApp
| PatternWildcard
| PatternBraces Pattern
| PatternWildcard Wildcard
| PatternEmpty
deriving stock (Show, Eq, Ord)
@ -291,7 +296,8 @@ instance HasAtomicity Pattern where
PatternApplication {} -> Aggregate appFixity
PatternInfixApplication a -> Aggregate (getFixity a)
PatternPostfixApplication p -> Aggregate (getFixity p)
PatternWildcard -> Atom
PatternWildcard {} -> Atom
PatternBraces {} -> Atom
PatternEmpty -> Atom
--------------------------------------------------------------------------------
@ -305,9 +311,10 @@ data PatternScopedIden
data PatternAtom (s :: Stage)
= PatternAtomIden (PatternAtomIdenType s)
| PatternAtomWildcard
| PatternAtomWildcard Wildcard
| PatternAtomEmpty
| PatternAtomParens (PatternAtoms s)
| PatternAtomBraces (PatternAtoms s)
data PatternAtoms (s :: Stage) = PatternAtoms
{ _patternAtoms :: NonEmpty (PatternAtom s),
@ -542,6 +549,7 @@ data Expression
| ExpressionLiteral LiteralLoc
| ExpressionFunction (Function 'Scoped)
| ExpressionHole (HoleType 'Scoped)
| ExpressionBraces (WithLoc Expression)
deriving stock (Show, Eq, Ord)
instance HasAtomicity Expression where
@ -556,6 +564,7 @@ instance HasAtomicity Expression where
ExpressionLiteral {} -> Atom
ExpressionMatch {} -> Atom
ExpressionLetBlock {} -> Atom
ExpressionBraces {} -> Atom
ExpressionUniverse {} -> Atom
ExpressionFunction {} -> Aggregate funFixity
@ -616,6 +625,7 @@ deriving stock instance
data FunctionParameter (s :: Stage) = FunctionParameter
{ _paramName :: Maybe (SymbolType s),
_paramUsage :: Maybe Usage,
_paramImplicit :: IsImplicit,
_paramType :: ExpressionType s
}
@ -912,6 +922,7 @@ data ExpressionAtom (s :: Stage)
= AtomIdentifier (IdentifierType s)
| AtomLambda (Lambda s)
| AtomHole (HoleType s)
| AtomBraces (WithLoc (ExpressionType s))
| AtomLetBlock (LetBlock s)
| AtomUniverse Universe
| AtomFunction (Function s)

17
src/MiniJuvix/Syntax/Concrete/Lexer.hs
View File

@ -94,6 +94,11 @@ interval ma = do
end <- curLoc
return (res, mkInterval start end)
withLoc :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (WithLoc a)
withLoc ma = do
(a, i) <- interval ma
return (WithLoc i a)
keyword :: Members '[Reader ParserParams, InfoTableBuilder] r => Text -> ParsecS r ()
keyword kw = do
l <- symbolInterval kw
@ -130,9 +135,6 @@ dot = P.char '.'
dottedIdentifier :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (NonEmpty (Text, Interval))
dottedIdentifier = lexeme $ P.sepBy1 bareIdentifier dot
braces :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
braces = between (symbol "{") (symbol "}")
allKeywords :: Members '[Reader ParserParams, InfoTableBuilder] r => [ParsecS r ()]
allKeywords =
[ kwAssignment,
@ -170,6 +172,12 @@ allKeywords =
kwWildcard
]
lbrace :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
lbrace = symbol "{"
rbrace :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
rbrace = symbol "}"
lparen :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
lparen = symbol "("
@ -179,6 +187,9 @@ rparen = symbol ")"
parens :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
parens = between lparen rparen
braces :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
braces = between (symbol "{") (symbol "}")
kwAssignment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii

22
src/MiniJuvix/Syntax/Concrete/Loc.hs
View File

@ -64,14 +64,36 @@ instance Hashable Interval
class HasLoc t where
getLoc :: t -> Interval
getLocSpan :: HasLoc t => NonEmpty t -> Interval
getLocSpan = foldr1 (<>) . fmap getLoc
-- | Assumes the file is the same
instance Semigroup Interval where
Interval f s e <> Interval _f s' e' = Interval f (min s s') (max e e')
data WithLoc a = WithLoc
{ _withLocInt :: Interval,
_withLocParam :: a
}
deriving stock (Show)
makeLenses ''Interval
makeLenses ''FileLoc
makeLenses ''Loc
makeLenses ''Pos
makeLenses ''WithLoc
instance HasLoc (WithLoc a) where
getLoc = (^. withLocInt)
instance Eq a => Eq (WithLoc a) where
(==) = (==) `on` (^. withLocParam)
instance Ord a => Ord (WithLoc a) where
compare = compare `on` (^. withLocParam)
instance Functor WithLoc where
fmap = over withLocParam
singletonInterval :: Loc -> Interval
singletonInterval l =

30
src/MiniJuvix/Syntax/Concrete/Parser.hs
View File

@ -177,7 +177,7 @@ import_ = do
expressionAtom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (ExpressionAtom 'Parsed)
expressionAtom =
do AtomLiteral <$> P.try literal
AtomLiteral <$> P.try literal
<|> (AtomIdentifier <$> name)
<|> (AtomUniverse <$> universe)
<|> (AtomLambda <$> lambda)
@ -187,6 +187,8 @@ expressionAtom =
<|> (AtomFunArrow <$ kwRightArrow)
<|> (AtomHole <$> hole)
<|> parens (AtomParens <$> parseExpressionAtoms)
-- TODO: revise this try. Necessary to avoid confusion with match
<|> P.try (braces (AtomBraces <$> withLoc parseExpressionAtoms))
parseExpressionAtoms ::
Members '[Reader ParserParams, InfoTableBuilder] r =>
@ -309,16 +311,26 @@ axiomDef = do
-- Function expression
--------------------------------------------------------------------------------
implicitOpen :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r IsImplicit
implicitOpen =
lbrace $> Implicit
<|> lparen $> Explicit
implicitClose :: Members '[Reader ParserParams, InfoTableBuilder] r => IsImplicit -> ParsecS r ()
implicitClose = \case
Implicit -> rbrace
Explicit -> rparen
functionParam :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (FunctionParameter 'Parsed)
functionParam = do
(_paramName, _paramUsage) <- P.try $ do
lparen
(_paramName, _paramUsage, _paramImplicit) <- P.try $ do
impl <- implicitOpen
n <- pName
u <- pUsage
return (n, u)
return (n, u, impl)
_paramType <- parseExpressionAtoms
rparen
return $ FunctionParameter {..}
implicitClose _paramImplicit
return FunctionParameter {..}
where
pName :: ParsecS r (Maybe Symbol)
pName =
@ -399,6 +411,9 @@ constructorDef = do
_constructorType <- parseExpressionAtoms
return InductiveConstructorDef {..}
wildcard :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Wildcard
wildcard = Wildcard . snd <$> interval kwWildcard
--------------------------------------------------------------------------------
-- Pattern section
--------------------------------------------------------------------------------
@ -406,8 +421,9 @@ constructorDef = do
patternAtom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (PatternAtom 'Parsed)
patternAtom =
PatternAtomIden <$> name
<|> PatternAtomWildcard <$ kwWildcard
<|> PatternAtomWildcard <$> wildcard
<|> (PatternAtomParens <$> parens parsePatternAtoms)
<|> (PatternAtomBraces <$> braces parsePatternAtoms)
parsePatternAtoms :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (PatternAtoms 'Parsed)
parsePatternAtoms = do

2
src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs
View File

@ -12,6 +12,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
data ScoperError
= ErrParser MegaParsecError
| ErrInfixParser InfixError
| ErrAppLeftImplicit AppLeftImplicit
| ErrInfixPattern InfixErrorP
| ErrMultipleDeclarations MultipleDeclarations
| ErrLacksTypeSig LacksTypeSig
@ -37,6 +38,7 @@ instance ToGenericError ScoperError where
genericError = \case
ErrParser e -> genericError e
ErrInfixParser e -> genericError e
ErrAppLeftImplicit e -> genericError e
ErrInfixPattern e -> genericError e
ErrMultipleDeclarations e -> genericError e
ErrLacksTypeSig e -> genericError e

21
src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
View File

@ -277,6 +277,27 @@ instance ToGenericError NotInScope where
instance HasLoc NotInScope where
getLoc = getLoc . (^. notInScopeSymbol)
newtype AppLeftImplicit = AppLeftImplicit
{ _appLeftImplicit :: WithLoc Expression
}
deriving stock (Show)
makeLenses ''AppLeftImplicit
instance ToGenericError AppLeftImplicit where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLoc (e ^. appLeftImplicit)
msg =
"The expression" <+> ppCode (e ^. appLeftImplicit) <+> "cannot appear by itself."
<> line
<> "It needs to be the argument of a function expecting an implicit argument."
newtype ModuleNotInScope = ModuleNotInScope
{ _moduleNotInScopeName :: Name
}

36
src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
View File

@ -173,6 +173,11 @@ braces = enclose kwBraceL kwBraceR
parens :: Doc Ann -> Doc Ann
parens = enclose kwParenL kwParenR
implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann
implicitDelim = \case
Implicit -> braces
Explicit -> parens
doubleQuotes :: Doc Ann -> Doc Ann
doubleQuotes = enclose kwDQuote kwDQuote
@ -512,13 +517,23 @@ instance SingI s => PrettyCode (TypeSignature s) where
instance SingI s => PrettyCode (Function s) where
ppCode :: forall r. Members '[Reader Options] r => Function s -> Sem r (Doc Ann)
ppCode Function {..} = do
funParameter' <- ppFunParameter _funParameter
funParameter' <- ppCode _funParameter
funReturn' <- ppRightExpression' funFixity _funReturn
return $ funParameter' <+> kwArrowR <+> funReturn'
where
ppRightExpression' = case sing :: SStage s of
SParsed -> ppRightExpression
SScoped -> ppRightExpression
instance SingI s => PrettyCode (FunctionParameter s) where
ppCode FunctionParameter {..} = do
case _paramName of
Nothing -> ppLeftExpression' funFixity _paramType
Just n -> do
paramName' <- annDef n <$> ppSymbol n
paramType' <- ppExpression _paramType
return $ implicitDelim _paramImplicit (paramName' <+> ppUsage _paramUsage <+> paramType')
where
ppLeftExpression' = case sing :: SStage s of
SParsed -> ppLeftExpression
SScoped -> ppLeftExpression
@ -529,14 +544,6 @@ instance SingI s => PrettyCode (Function s) where
UsageNone -> kwColonZero
UsageOnce -> kwColonOne
UsageOmega -> kwColonOmega
ppFunParameter :: FunctionParameter s -> Sem r (Doc Ann)
ppFunParameter FunctionParameter {..} = do
case _paramName of
Nothing -> ppLeftExpression' funFixity _paramType
Just n -> do
paramName' <- annDef n <$> ppSymbol n
paramType' <- ppExpression _paramType
return $ parens (paramName' <+> ppUsage _paramUsage <+> paramType')
instance PrettyCode Universe where
ppCode (Universe n) = return $ kwType <+?> (pretty <$> n)
@ -646,9 +653,10 @@ instance SingI s => PrettyCode (PatternAtom s) where
PatternAtomIden n -> case sing :: SStage s of
SParsed -> ppCode n
SScoped -> ppCode n
PatternAtomWildcard -> return kwWildcard
PatternAtomWildcard {} -> return kwWildcard
PatternAtomEmpty -> return $ parens mempty
PatternAtomParens p -> parens <$> ppCode p
PatternAtomBraces p -> braces <$> ppCode p
instance SingI s => PrettyCode (PatternAtoms s) where
ppCode (PatternAtoms ps _) = hsep . toList <$> mapM ppCode ps
@ -710,11 +718,15 @@ instance PrettyCode ScopedIden where
ScopedFunction f -> ppCode f
ScopedConstructor c -> ppCode c
instance PrettyCode c => PrettyCode (WithLoc c) where
ppCode = ppCode . (^. withLocParam)
instance PrettyCode Expression where
ppCode e = case e of
ExpressionIdentifier n -> ppCode n
ExpressionHole w -> ppHole w
ExpressionParensIdentifier n -> parens <$> ppCode n
ExpressionBraces b -> braces <$> ppCode b
ExpressionApplication a -> ppCode a
ExpressionInfixApplication a -> ppCode a
ExpressionPostfixApplication a -> ppCode a
@ -733,8 +745,9 @@ instance PrettyCode Pattern where
l' <- ppLeftExpression appFixity l
r' <- ppRightExpression appFixity r
return $ l' <+> r'
PatternWildcard -> return kwWildcard
PatternWildcard {} -> return kwWildcard
PatternEmpty -> return $ parens mempty
PatternBraces p -> braces <$> ppCode p
PatternConstructor constr -> ppCode constr
PatternInfixApplication i -> ppPatternInfixApp i
PatternPostfixApplication i -> ppPatternPostfixApp i
@ -812,6 +825,7 @@ instance SingI s => PrettyCode (ExpressionAtom s) where
AtomFunArrow -> return kwArrowR
AtomMatch m -> ppCode m
AtomParens e -> parens <$> ppExpression e
AtomBraces e -> braces <$> ppExpression (e ^. withLocParam)
AtomHole w -> ppHole w
instance SingI s => PrettyCode (ExpressionAtoms s) where

56
src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
View File

@ -911,6 +911,7 @@ checkFunction Function {..} = do
FunctionParameter
{ _paramName = paramName',
_paramUsage = _paramUsage,
_paramImplicit = _paramImplicit,
_paramType = paramType'
}
where
@ -1088,10 +1089,11 @@ checkPatternAtom ::
PatternAtom 'Parsed ->
Sem r (PatternAtom 'Scoped)
checkPatternAtom p = case p of
PatternAtomWildcard -> return PatternAtomWildcard
PatternAtomWildcard i -> return (PatternAtomWildcard i)
PatternAtomEmpty -> return PatternAtomEmpty
PatternAtomParens e -> PatternAtomParens <$> checkPatternAtoms e
PatternAtomIden n -> PatternAtomIden <$> checkPatternName n
PatternAtomBraces n -> PatternAtomBraces <$> checkPatternAtoms n
checkName ::
Members '[Error ScoperError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r =>
@ -1112,6 +1114,7 @@ checkExpressionAtom e = case e of
AtomUniverse uni -> return (AtomUniverse uni)
AtomFunction fun -> AtomFunction <$> checkFunction fun
AtomParens par -> AtomParens <$> checkParens par
AtomBraces br -> AtomBraces <$> traverseOf withLocParam checkParseExpressionAtoms br
AtomFunArrow -> return AtomFunArrow
AtomHole h -> AtomHole <$> checkHole h
AtomLiteral l -> return (AtomLiteral l)
@ -1206,9 +1209,10 @@ checkStatement s = case s of
-------------------------------------------------------------------------------
-- Infix Expression
-------------------------------------------------------------------------------
makeExpressionTable2 ::
ExpressionAtoms 'Scoped -> [[P.Operator Parse Expression]]
makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functionOp]]
makeExpressionTable2 (ExpressionAtoms atoms _) = [appOpExplicit] : operators ++ [[functionOp]]
where
operators = mkSymbolTable idens
idens :: [ScopedIden]
@ -1253,8 +1257,8 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functi
_ -> Nothing
-- Application by juxtaposition.
appOp :: P.Operator Parse Expression
appOp = P.InfixL (return app)
appOpExplicit :: P.Operator Parse Expression
appOpExplicit = P.InfixL (return app)
where
app :: Expression -> Expression -> Expression
app f x =
@ -1263,6 +1267,7 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functi
{ _applicationFunction = f,
_applicationParameter = x
}
-- Non-dependent function type: A → B
functionOp :: P.Operator Parse Expression
functionOp = P.InfixR (nonDepFun <$ P.single AtomFunArrow)
@ -1279,6 +1284,7 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functi
FunctionParameter
{ _paramName = Nothing,
_paramUsage = Nothing,
_paramImplicit = Explicit,
_paramType = a
}
@ -1325,6 +1331,7 @@ parseTerm =
<|> parseLiteral
<|> parseMatch
<|> parseLetBlock
<|> parseBraces
where
parseHole :: Parse Expression
parseHole = ExpressionHole <$> P.token lit mempty
@ -1391,6 +1398,14 @@ parseTerm =
| not (S.hasFixity (identifierName iden)) -> Just iden
_ -> Nothing
parseBraces :: Parse Expression
parseBraces = ExpressionBraces <$> P.token bracedExpr mempty
where
bracedExpr :: ExpressionAtom 'Scoped -> Maybe (WithLoc Expression)
bracedExpr = \case
AtomBraces l -> Just l
_ -> Nothing
parseParens :: Parse Expression
parseParens = P.token parenExpr mempty
where
@ -1457,7 +1472,13 @@ makePatternTable atom = [appOp] : operators
appOp = P.InfixL (return app)
where
app :: Pattern -> Pattern -> Pattern
app l = PatternApplication . PatternApp l
app l r =
PatternApplication
( PatternApp
{ _patAppLeft = l,
_patAppRight = r
}
)
parsePatternTerm ::
forall r.
@ -1469,6 +1490,7 @@ parsePatternTerm = do
parseNoInfixConstructor
<|> parseVariable
<|> parseParens pPat
<|> parseBraces pPat
<|> parseWildcard
<|> parseEmpty
where
@ -1486,12 +1508,12 @@ parsePatternTerm = do
_ -> Nothing
parseWildcard :: ParsePat Pattern
parseWildcard = PatternWildcard <$ P.satisfy isWildcard
parseWildcard = PatternWildcard <$> P.token isWildcard mempty
where
isWildcard :: PatternAtom 'Scoped -> Bool
isWildcard :: PatternAtom 'Scoped -> Maybe Wildcard
isWildcard s = case s of
PatternAtomWildcard -> True
_ -> False
PatternAtomWildcard i -> Just i
_ -> Nothing
parseEmpty :: ParsePat Pattern
parseEmpty = PatternEmpty <$ P.satisfy isEmpty
@ -1509,15 +1531,25 @@ parsePatternTerm = do
PatternAtomIden (PatternScopedVar sym) -> Just sym
_ -> Nothing
parseBraces :: ParsePat Pattern -> ParsePat Pattern
parseBraces patternParser = do
exprs <- P.token bracesPat mempty
case P.parse patternParser "" exprs of
Right r -> return (PatternBraces r)
Left {} -> mzero
where
bracesPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
bracesPat s = case s of
PatternAtomBraces (PatternAtoms ss _) -> Just (toList ss)
_ -> Nothing
parseParens :: ParsePat Pattern -> ParsePat Pattern
parseParens patternParser = do
exprs <- P.token parenPat mempty
case P.parse patternParser strPath exprs of
case P.parse patternParser "" exprs of
Right r -> return r
Left {} -> mzero
where
strPath :: FilePath
strPath = "inner parens"
parenPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
parenPat s = case s of
PatternAtomParens (PatternAtoms ss _) -> Just (toList ss)

8
src/MiniJuvix/Syntax/IsImplicit.hs Normal file
View File

@ -0,0 +1,8 @@
module MiniJuvix.Syntax.IsImplicit where
import MiniJuvix.Prelude
data IsImplicit = Explicit | Implicit
deriving stock (Show, Eq, Ord, Generic)
instance Hashable IsImplicit

403
src/MiniJuvix/Syntax/MicroJuvix/ArityChecker.hs Normal file
View File

@ -0,0 +1,403 @@
module MiniJuvix.Syntax.MicroJuvix.ArityChecker
( module MiniJuvix.Syntax.MicroJuvix.ArityChecker,
module MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult,
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error,
)
where
import MiniJuvix.Internal.NameIdGen
import MiniJuvix.Prelude hiding (fromEither)
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Arity
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.LocalVars
import MiniJuvix.Syntax.MicroJuvix.InfoTable
import MiniJuvix.Syntax.MicroJuvix.Language.Extra
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult
entryMicroJuvixArity ::
Members '[Error ArityCheckerError, NameIdGen] r =>
MicroJuvixResult ->
Sem r MicroJuvixArityResult
entryMicroJuvixArity res@MicroJuvixResult {..} = do
r <- runReader table (mapM checkModule _resultModules)
return
MicroJuvixArityResult
{ _resultMicroJuvixResult = res,
_resultModules = r
}
where
table :: InfoTable
table = buildTable _resultModules
checkModule ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
Module ->
Sem r Module
checkModule Module {..} = do
_moduleBody' <- checkModuleBody _moduleBody
return
Module
{ _moduleBody = _moduleBody',
..
}
checkModuleBody ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
ModuleBody ->
Sem r ModuleBody
checkModuleBody ModuleBody {..} = do
_moduleStatements' <- mapM checkStatement _moduleStatements
return
ModuleBody
{ _moduleStatements = _moduleStatements'
}
checkInclude ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
Include ->
Sem r Include
checkInclude = traverseOf includeModule checkModule
checkStatement ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
Statement ->
Sem r Statement
checkStatement s = case s of
StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
StatementInclude i -> StatementInclude <$> checkInclude i
StatementForeign {} -> return s
StatementInductive {} -> return s
StatementAxiom {} -> return s
checkFunctionDef ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
FunctionDef ->
Sem r FunctionDef
checkFunctionDef FunctionDef {..} = do
arity <- typeArity _funDefType
_funDefClauses' <- mapM (checkFunctionClause arity) _funDefClauses
return
FunctionDef
{ _funDefClauses = _funDefClauses',
..
}
checkFunctionClause ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
Arity ->
FunctionClause ->
Sem r FunctionClause
checkFunctionClause ari cl = do
hint <- guessArity (cl ^. clauseBody)
(patterns', locals, bodyAri) <- checkLhs loc hint ari (cl ^. clausePatterns)
body' <- runReader locals (checkExpression bodyAri (cl ^. clauseBody))
return
FunctionClause
{ _clauseName = cl ^. clauseName,
_clausePatterns = patterns',
_clauseBody = body'
}
where
name = cl ^. clauseName
loc = getLoc name
guessArity ::
forall r.
Members '[Reader InfoTable] r =>
Expression ->
Sem r (Maybe Arity)
guessArity = \case
ExpressionTyped {} -> impossible
ExpressionHole {} -> return Nothing
ExpressionFunction {} -> return (Just ArityUnit)
ExpressionLiteral {} -> return (Just arityLiteral)
ExpressionApplication a -> appHelper a
ExpressionIden i -> idenHelper i
where
idenHelper :: Iden -> Sem r (Maybe Arity)
idenHelper i = case i of
IdenVar {} -> return Nothing
_ -> Just <$> runReader (LocalVars mempty) (idenArity i)
appHelper :: Application -> Sem r (Maybe Arity)
appHelper a = do
f' <- arif
return (f' >>= \f'' -> foldArity <$> refine (unfoldArity f'') args)
where
(f, args) = second (map fst . toList) (unfoldApplication' a)
refine :: [ArityParameter] -> [IsImplicit] -> Maybe [ArityParameter]
refine ps as = case (ps, as) of
(ParamExplicit {} : ps', Explicit : as') -> refine ps' as'
(ParamImplicit {} : ps', Implicit : as') -> refine ps' as'
(ParamImplicit {} : ps', as'@(Explicit : _)) -> refine ps' as'
(ParamExplicit {} : _, Implicit : _) -> Nothing
(ps', []) -> Just ps'
([], _ : _) -> Nothing
arif :: Sem r (Maybe Arity)
arif = case f of
ExpressionHole {} -> return Nothing
ExpressionApplication {} -> impossible
ExpressionFunction {} -> return (Just ArityUnit)
ExpressionLiteral {} -> return (Just arityLiteral)
ExpressionTyped {} -> impossible
ExpressionIden i -> idenHelper i
arityLiteral :: Arity
arityLiteral = ArityUnit
checkLhs ::
forall r.
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r =>
Interval ->
Maybe Arity ->
Arity ->
[Pattern] ->
Sem r ([Pattern], LocalVars, Arity)
checkLhs loc hint ariSignature pats = do
(locals, (pats', bodyAri)) <- runState emptyLocalVars (goLhs ariSignature pats)
return (pats', locals, bodyAri)
where
-- returns the expanded patterns and the rest of the Arity (the arity of the
-- body once all the patterns have been processed).
-- Does not insert holes greedily. I.e. implicit wildcards are only inserted
-- between explicit parameters already in the pattern.
goLhs :: Arity -> [Pattern] -> Sem (State LocalVars ': r) ([Pattern], Arity)
goLhs a = \case
[] -> return $ case hint >>= tailHelper a of
Nothing -> ([], a)
Just tailUnderscores ->
let a' = foldArity (drop tailUnderscores (unfoldArity a))
in (replicate tailUnderscores wildcard, a')
lhs@(p : ps) -> case a of
ArityUnit ->
throw
( ErrLhsTooManyPatterns
LhsTooManyPatterns
{ _lhsTooManyPatternsRemaining = p :| ps
}
)
ArityUnknown -> do
p' <- checkPattern ArityUnknown p
first (p' :) <$> goLhs ArityUnknown ps
ArityFunction (FunctionArity l r) ->
case (getPatternBraces p, l) of
(Just b, ParamImplicit) -> do
b' <- checkPattern (arityParameter l) b
first (b' :) <$> goLhs r ps
(Just x, ParamExplicit {}) ->
throw
( ErrExpectedExplicitPattern
ExpectedExplicitPattern
{ _expectedExplicitPattern = x
}
)
(Nothing, ParamImplicit) ->
first (wildcard :) <$> goLhs r lhs
(Nothing, ParamExplicit pa) -> do
p' <- checkPattern pa p
first (p' :) <$> goLhs r ps
where
wildcard :: Pattern
wildcard = PatternBraces (PatternWildcard (Wildcard loc))
tailHelper :: Arity -> Arity -> Maybe Int
tailHelper a target
| notNull a' && all (== ParamImplicit) a' = Just (length a')
| otherwise = Nothing
where
a' = dropSuffix target' (unfoldArity a)
target' = unfoldArity target
getPatternBraces :: Pattern -> Maybe Pattern
getPatternBraces p = case p of
PatternBraces {} -> Just p
_ -> Nothing
checkPattern ::
Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r =>
Arity ->
Pattern ->
Sem r Pattern
checkPattern ari = \case
PatternBraces p -> checkPattern ari p
PatternVariable v -> addArity v ari $> PatternVariable v
PatternWildcard i -> return (PatternWildcard i)
PatternConstructorApp c -> case ari of
ArityUnit -> PatternConstructorApp <$> checkConstructorApp c
ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c
ArityFunction {} ->
throw
( ErrPatternFunction
PatternFunction
{ _patternFunction = c
}
)
checkConstructorApp ::
forall r.
Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r =>
ConstructorApp ->
Sem r ConstructorApp
checkConstructorApp ca@(ConstructorApp c ps) = do
args <- (^. constructorInfoArgs) <$> lookupConstructor c
arities <- mapM typeArity args
let n = length arities
lps = length ps
when
(n /= lps)
( throw
( ErrWrongConstructorAppLength
WrongConstructorAppLength
{ _wrongConstructorAppLength = ca,
_wrongConstructorAppLengthExpected = n
}
)
)
ps' <- zipWithM checkPattern arities ps
return (ConstructorApp c ps')
idenArity :: Members '[Reader LocalVars, Reader InfoTable] r => Iden -> Sem r Arity
idenArity = \case
IdenFunction f -> lookupFunction f >>= typeArity . (^. functionInfoDef . funDefType)
IdenConstructor c -> constructorType c >>= typeArity
IdenVar v -> getLocalArity v
IdenAxiom a -> lookupAxiom a >>= typeArity . (^. axiomInfoType)
IdenInductive i -> inductiveType i >>= typeArity
typeArity :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Arity
typeArity = go
where
go :: Type -> Sem r Arity
go = \case
TypeIden i -> goIden i
TypeApp {} -> return ArityUnit
TypeFunction f -> ArityFunction <$> goFun f
TypeAbs f -> ArityFunction <$> goAbs f
TypeHole {} -> return ArityUnknown
TypeUniverse {} -> return ArityUnit
TypeAny {} -> return ArityUnknown
goIden :: TypeIden -> Sem r Arity
goIden = \case
TypeIdenVariable {} -> return ArityUnknown
TypeIdenInductive {} -> return ArityUnit
TypeIdenAxiom ax -> do
ty <- (^. axiomInfoType) <$> lookupAxiom ax
go ty
goFun :: Function -> Sem r FunctionArity
goFun (Function l r) = do
l' <- ParamExplicit <$> go l
r' <- go r
return
FunctionArity
{ _functionArityLeft = l',
_functionArityRight = r'
}
goAbs :: TypeAbstraction -> Sem r FunctionArity
goAbs t = do
r' <- go (t ^. typeAbsBody)
return (FunctionArity l r')
where
l :: ArityParameter
l = case t ^. typeAbsImplicit of
Implicit -> ParamImplicit
Explicit -> ParamExplicit ArityUnit
checkExpression ::
forall r.
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r =>
Arity ->
Expression ->
Sem r Expression
checkExpression hintArity expr = case expr of
ExpressionIden {} -> appHelper expr []
ExpressionApplication a -> goApp a
ExpressionLiteral {} -> return expr
ExpressionFunction {} -> return expr
ExpressionHole {} -> return expr
ExpressionTyped {} -> impossible
where
goApp :: Application -> Sem r Expression
goApp = uncurry appHelper . second toList . unfoldApplication'
appHelper :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression
appHelper fun args = do
args' :: [(IsImplicit, Expression)] <- case fun of
ExpressionHole {} -> mapM (secondM (checkExpression ArityUnknown)) args
ExpressionIden i -> do
ari <- idenArity i
let argsAris :: [Arity]
argsAris = map toArity (unfoldArity ari)
toArity :: ArityParameter -> Arity
toArity = \case
ParamExplicit a -> a
ParamImplicit -> ArityUnit
mapM
(secondM (uncurry checkExpression))
[(i', (a, e')) | (a, (i', e')) <- zip (argsAris ++ repeat ArityUnknown) args]
>>= addHoles (getLoc i) hintArity ari
ExpressionLiteral {} -> error "TODO literals on the left of an application"
ExpressionFunction f ->
throw
( ErrFunctionApplied
FunctionApplied
{ _functionAppliedFunction = f,
_functionAppliedArguments = args
}
)
ExpressionApplication {} -> impossible
ExpressionTyped {} -> impossible
return (foldApplication fun args')
where
addHoles ::
Interval ->
Arity ->
Arity ->
[(IsImplicit, Expression)] ->
Sem r [(IsImplicit, Expression)]
addHoles loc hint = go 0
where
go ::
Int ->
Arity ->
[(IsImplicit, Expression)] ->
Sem r [(IsImplicit, Expression)]
go idx ari goargs = case (ari, goargs) of
(ArityFunction (FunctionArity ParamImplicit r), (Implicit, e) : rest) ->
((Implicit, e) :) <$> go (succ idx) r rest
(ArityFunction (FunctionArity (ParamExplicit {}) r), (Explicit, e) : rest) ->
((Explicit, e) :) <$> go (succ idx) r rest
(ArityFunction (FunctionArity ParamImplicit _), [])
-- When there are no remaining arguments and the expected arity of the
-- expression matches the current arity we should *not* insert a hole.
| ari == hint -> return []
(ArityFunction (FunctionArity ParamImplicit r), _) -> do
h <- newHole loc
((Implicit, ExpressionHole h) :) <$> go (succ idx) r goargs
(ArityFunction (FunctionArity (ParamExplicit {}) _), (Implicit, _) : _) ->
throw
( ErrExpectedExplicitArgument
ExpectedExplicitArgument
{ _expectedExplicitArgumentApp = (fun, args),
_expectedExplicitArgumentIx = idx
}
)
(ArityUnit, []) -> return []
(ArityFunction (FunctionArity (ParamExplicit _) _), []) -> return []
(ArityUnit, _ : _) ->
throw
( ErrTooManyArguments
TooManyArguments
{ _tooManyArgumentsApp = (fun, args),
_tooManyArgumentsUnexpected = length goargs
}
)
(ArityUnknown, []) -> return []
(ArityUnknown, p : ps) -> (p :) <$> go (succ idx) ArityUnknown ps
newHole :: Member NameIdGen r => Interval -> Sem r Hole
newHole loc = (`Hole` loc) <$> freshNameId

45
src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Arity.hs Normal file
View File

@ -0,0 +1,45 @@
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Arity where
import MiniJuvix.Prelude
data Arity
= ArityUnit
| ArityFunction FunctionArity
| ArityUnknown
deriving stock (Eq)
data FunctionArity = FunctionArity
{ _functionArityLeft :: ArityParameter,
_functionArityRight :: Arity
}
deriving stock (Eq)
data ArityParameter
= ParamExplicit Arity
| ParamImplicit
deriving stock (Eq)
arityParameter :: ArityParameter -> Arity
arityParameter = \case
ParamImplicit -> ArityUnit
ParamExplicit a -> a
unfoldArity :: Arity -> [ArityParameter]
unfoldArity = go
where
go :: Arity -> [ArityParameter]
go = \case
ArityUnit -> []
ArityUnknown -> []
ArityFunction (FunctionArity l r) -> l : unfoldArity r
foldArity :: [ArityParameter] -> Arity
foldArity = go
where
go = \case
[] -> ArityUnit
(a : as) -> ArityFunction (FunctionArity l (go as))
where
l = case a of
ParamExplicit e -> ParamExplicit e
ParamImplicit -> ParamImplicit

28
src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error.hs Normal file
View File

@ -0,0 +1,28 @@
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error
( module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error,
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error.Types,
)
where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error.Types
data ArityCheckerError
= ErrWrongConstructorAppLength WrongConstructorAppLength
| ErrLhsTooManyPatterns LhsTooManyPatterns
| ErrExpectedExplicitPattern ExpectedExplicitPattern
| ErrExpectedExplicitArgument ExpectedExplicitArgument
| ErrPatternFunction PatternFunction
| ErrTooManyArguments TooManyArguments
| ErrFunctionApplied FunctionApplied
instance ToGenericError ArityCheckerError where
genericError :: ArityCheckerError -> GenericError
genericError = \case
ErrWrongConstructorAppLength e -> genericError e
ErrLhsTooManyPatterns e -> genericError e
ErrExpectedExplicitPattern e -> genericError e
ErrExpectedExplicitArgument e -> genericError e
ErrPatternFunction e -> genericError e
ErrTooManyArguments e -> genericError e
ErrFunctionApplied e -> genericError e

195
src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs Normal file
View File

@ -0,0 +1,195 @@
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error.Types where
-- import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
import MiniJuvix.Prelude
import MiniJuvix.Prelude.Pretty
import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
import MiniJuvix.Syntax.MicroJuvix.Language.Extra
data WrongConstructorAppLength = WrongConstructorAppLength
{ _wrongConstructorAppLength :: ConstructorApp,
_wrongConstructorAppLengthExpected :: Int
}
makeLenses ''WrongConstructorAppLength
instance ToGenericError WrongConstructorAppLength where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLoc (e ^. wrongConstructorAppLength)
msg =
"The constructor"
<+> ppCode (e ^. wrongConstructorAppLength . constrAppConstructor)
<+> "should have"
<+> arguments (e ^. wrongConstructorAppLengthExpected)
<> ", but has been given"
<+> pretty actual
actual :: Int
actual = length (e ^. wrongConstructorAppLength . constrAppParameters)
arguments :: Int -> Doc ann
arguments n = num <+> plural "argument" "arguments" n
where
num
| n == 0 = "no"
| otherwise = pretty n
newtype LhsTooManyPatterns = LhsTooManyPatterns
{ _lhsTooManyPatternsRemaining :: NonEmpty Pattern
}
makeLenses ''LhsTooManyPatterns
instance ToGenericError LhsTooManyPatterns where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLocSpan (e ^. lhsTooManyPatternsRemaining)
n = length (e ^. lhsTooManyPatternsRemaining)
howMany =
"The last" <+> case n of
1 -> "pattern"
_ -> pretty n <+> "patterns"
msg =
howMany <+> "on the left hand side of the function clause" <+> wasWere <+> "not expected"
wasWere
| n == 1 = "was"
| otherwise = "were"
newtype ExpectedExplicitPattern = ExpectedExplicitPattern
{ _expectedExplicitPattern :: Pattern
}
makeLenses ''ExpectedExplicitPattern
instance ToGenericError ExpectedExplicitPattern where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLoc (e ^. expectedExplicitPattern)
msg =
"Expected an explicit pattern but found an implicit pattern"
<+> ppCode (e ^. expectedExplicitPattern)
data ExpectedExplicitArgument = ExpectedExplicitArgument
{ _expectedExplicitArgumentApp :: (Expression, [(IsImplicit, Expression)]),
_expectedExplicitArgumentIx :: Int
}
makeLenses ''ExpectedExplicitArgument
instance ToGenericError ExpectedExplicitArgument where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
app@(f, args) = e ^. expectedExplicitArgumentApp
idx = e ^. expectedExplicitArgumentIx
arg :: Expression
arg = snd (toList args !! idx)
i = getLoc arg
msg =
"Expected an explicit argument as the" <+> ordinal (succ idx) <+> "argument of"
<+> ppCode f
<+> "but found"
<+> ppArg Implicit arg
<> "."
<> softline
<> "In the application"
<+> ppApp app
newtype PatternFunction = PatternFunction
{ _patternFunction :: ConstructorApp
}
makeLenses ''PatternFunction
instance ToGenericError PatternFunction where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLoc (e ^. patternFunction)
msg =
"Invalid pattern" <+> ppCode (e ^. patternFunction) <> "."
<+> "Function types cannot be pattern matched"
data TooManyArguments = TooManyArguments
{ _tooManyArgumentsApp :: (Expression, [(IsImplicit, Expression)]),
_tooManyArgumentsUnexpected :: Int
}
makeLenses ''TooManyArguments
instance ToGenericError TooManyArguments where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLocSpan (fromJust (nonEmpty (map snd unexpectedArgs)))
(fun, args) = e ^. tooManyArgumentsApp
numUnexpected :: Int
numUnexpected = e ^. tooManyArgumentsUnexpected
unexpectedArgs :: [(IsImplicit, Expression)]
unexpectedArgs = reverse . take numUnexpected . reverse $ args
ppUnexpectedArgs = hsep (map (uncurry ppArg) unexpectedArgs)
app :: Expression
app = foldApplication fun args
msg =
"Too many arguments in the application" <+> ppCode app <> "."
<+> "The last"
<+> numArguments
<> ", namely"
<+> ppUnexpectedArgs
<> ","
<+> wasNotExpected
numArguments :: Doc ann
numArguments = plural "argument" (pretty numUnexpected <+> "arguments") numUnexpected
wasNotExpected :: Doc ann
wasNotExpected
| numUnexpected == 1 = "was not expected"
| otherwise = "were not expected"
data FunctionApplied = FunctionApplied
{ _functionAppliedFunction :: FunctionExpression,
_functionAppliedArguments :: [(IsImplicit, Expression)]
}
makeLenses ''FunctionApplied
instance ToGenericError FunctionApplied where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLocSpan (fun :| map snd args)
args = e ^. functionAppliedArguments
fun = ExpressionFunction (e ^. functionAppliedFunction)
msg =
"A function type cannot be applied." <> softline
<> "In the application" <+> ppApp (fun, args)

24
src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/LocalVars.hs Normal file
View File

@ -0,0 +1,24 @@
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.LocalVars where
import Data.HashMap.Strict qualified as HashMap
import MiniJuvix.Prelude
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Arity
import MiniJuvix.Syntax.MicroJuvix.Language
newtype LocalVars = LocalVars
{ _localArities :: HashMap VarName Arity
}
makeLenses ''LocalVars
addArity :: Member (State LocalVars) r => VarName -> Arity -> Sem r ()
addArity v t = modify (over localArities (HashMap.insert v t))
getLocalArity :: Member (Reader LocalVars) r => VarName -> Sem r Arity
getLocalArity v = fromJust <$> asks (^. localArities . at v)
emptyLocalVars :: LocalVars
emptyLocalVars =
LocalVars
{ _localArities = mempty
}

10
src/MiniJuvix/Syntax/MicroJuvix/Error.hs
View File

@ -2,17 +2,18 @@ module MiniJuvix.Syntax.MicroJuvix.Error
( module MiniJuvix.Syntax.MicroJuvix.Error,
module MiniJuvix.Syntax.MicroJuvix.Error.Pretty,
module MiniJuvix.Syntax.MicroJuvix.Error.Types,
module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error,
)
where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error
import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
import MiniJuvix.Syntax.MicroJuvix.Error.Types
data TypeCheckerError
= ErrTooManyPatterns TooManyPatterns
| ErrWrongConstructorType WrongConstructorType
| ErrWrongConstructorAppArgs WrongConstructorAppArgs
= ErrWrongConstructorType WrongConstructorType
| ErrArity ArityCheckerError
| ErrWrongType WrongType
| ErrUnsolvedMeta UnsolvedMeta
| ErrExpectedFunctionType ExpectedFunctionType
@ -20,9 +21,8 @@ data TypeCheckerError
instance ToGenericError TypeCheckerError where
genericError :: TypeCheckerError -> GenericError
genericError = \case
ErrTooManyPatterns e -> genericError e
ErrWrongConstructorType e -> genericError e
ErrWrongConstructorAppArgs e -> genericError e
ErrArity e -> genericError e
ErrWrongType e -> genericError e
ErrUnsolvedMeta e -> genericError e
ErrExpectedFunctionType e -> genericError e

24
src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs
View File

@ -1,17 +1,26 @@
module MiniJuvix.Syntax.MicroJuvix.Error.Pretty
( module MiniJuvix.Syntax.MicroJuvix.Error.Pretty,
module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ann,
module MiniJuvix.Prelude.Pretty,
)
where
import MiniJuvix.Prelude
import MiniJuvix.Prelude.Pretty
import MiniJuvix.Syntax.Fixity
import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ann
import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi qualified as Ansi
import MiniJuvix.Syntax.MicroJuvix.Language.Extra
import MiniJuvix.Syntax.MicroJuvix.Pretty.Base qualified as Micro
ppCode :: Micro.PrettyCode c => c -> Doc Eann
ppCode = reAnnotate MicroAnn . Micro.runPrettyCode Micro.defaultOptions
ppCode = runPP . Micro.ppCode
ppAtom :: (Micro.PrettyCode c, HasAtomicity c) => c -> Doc Eann
ppAtom = runPP . Micro.ppCodeAtom
runPP :: Sem '[Reader Micro.Options] (Doc Micro.Ann) -> Doc Eann
runPP = highlight_ . reAnnotate MicroAnn . run . runReader Micro.defaultOptions
newtype PPOutput = PPOutput (Doc Eann)
@ -29,5 +38,14 @@ instance HasTextBackend PPOutput where
indent' :: Doc ann -> Doc ann
indent' = indent 2
highlight :: Doc Eann -> Doc Eann
highlight = annotate Highlight
highlight_ :: Doc Eann -> Doc Eann
highlight_ = annotate Highlight
ppApp :: (Expression, [(IsImplicit, Expression)]) -> Doc Eann
ppApp (fun, args) =
hsep (ppAtom fun : map (uncurry ppArg) args)
ppArg :: IsImplicit -> Expression -> Doc Eann
ppArg im arg = case im of
Implicit -> braces (ppCode arg)
Explicit -> ppAtom arg

2
src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs
View File

@ -11,5 +11,5 @@ renderAnsi = renderStrict . reAnnotateS stylize
stylize :: Eann -> AnsiStyle
stylize a = case a of
Highlight -> colorDull Red
Highlight -> bold
MicroAnn m -> M.stylize m

41
src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
View File

@ -13,7 +13,6 @@ data WrongConstructorType = WrongConstructorType
_wrongCtorTypeActual :: InductiveName,
_wrongCtorTypeFunName :: Name
}
deriving stock (Show)
makeLenses ''WrongConstructorType
@ -60,7 +59,6 @@ data WrongConstructorAppArgs = WrongConstructorAppArgs
_wrongCtorAppTypes :: [FunctionArgType],
_wrongCtorAppName :: Name
}
deriving stock (Show)
makeLenses ''WrongConstructorAppArgs
@ -98,7 +96,6 @@ data WrongType = WrongType
_wrongTypeExpectedType :: Type,
_wrongTypeInferredType :: Type
}
deriving stock (Show)
makeLenses ''WrongType
@ -112,7 +109,7 @@ instance ToGenericError WrongType where
where
i = getLoc (e ^. wrongTypeExpression)
msg =
"Type error near" <+> highlight (pretty (getLoc subjectExpr)) <> "."
"Type error near" <+> pretty (getLoc subjectExpr) <> "."
<> line
<> "The expression" <+> ppCode subjectExpr <+> "has type:"
<> line
@ -132,7 +129,6 @@ data ExpectedFunctionType = ExpectedFunctionType
_expectedFunctionTypeApp :: Expression,
_expectedFunctionTypeType :: Type
}
deriving stock (Show)
makeLenses ''ExpectedFunctionType
@ -146,7 +142,7 @@ instance ToGenericError ExpectedFunctionType where
where
i = getLoc (e ^. expectedFunctionTypeExpression)
msg =
"Type error near" <+> highlight (pretty (getLoc subjectExpr)) <> "."
"Type error near" <+> pretty (getLoc subjectExpr) <> "."
<> line
<> "In the expression:"
<> line
@ -157,36 +153,3 @@ instance ToGenericError ExpectedFunctionType where
<> indent' (ppCode (e ^. expectedFunctionTypeType))
subjectExpr :: Expression
subjectExpr = e ^. expectedFunctionTypeExpression
-- | A function definition clause matches too many arguments
data TooManyPatterns = TooManyPatterns
{ _tooManyPatternsClause :: FunctionClause,
_tooManyPatternsTypes :: [FunctionArgType]
}
deriving stock (Show)
makeLenses ''TooManyPatterns
instance ToGenericError TooManyPatterns where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
i = getLoc (e ^. tooManyPatternsClause . clauseName)
name :: Name
name = e ^. tooManyPatternsClause . clauseName
msg =
"Type error near" <+> highlight (pretty (name ^. nameDefined))
<> line
<> "In in the definition of" <+> ppCode name <+> "the function clause:"
<> line
<> indent' (ppCode (e ^. tooManyPatternsClause))
<> line
<> "matches too many patterns. It should match the following types:"
<> line
<> indent' (hsep (ppCode <$> (e ^. tooManyPatternsTypes)))

41
src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs
View File

@ -2,7 +2,7 @@ module MiniJuvix.Syntax.MicroJuvix.InfoTable where
import Data.HashMap.Strict qualified as HashMap
import MiniJuvix.Prelude
import MiniJuvix.Syntax.MicroJuvix.Language
import MiniJuvix.Syntax.MicroJuvix.Language.Extra
data ConstructorInfo = ConstructorInfo
{ _constructorInfoInductiveParameters :: [InductiveParameter],
@ -103,3 +103,42 @@ lookupFunction f = HashMap.lookupDefault impossible f <$> asks (^. infoFunctions
lookupAxiom :: Member (Reader InfoTable) r => Name -> Sem r AxiomInfo
lookupAxiom f = HashMap.lookupDefault impossible f <$> asks (^. infoAxioms)
inductiveType :: Member (Reader InfoTable) r => Name -> Sem r Type
inductiveType v = do
info <- lookupInductive v
let ps = info ^. inductiveInfoDef . inductiveParameters
return $
foldr
(\p k -> TypeAbs (TypeAbstraction (p ^. inductiveParamName) Explicit k))
TypeUniverse
ps
constructorArgTypes :: ConstructorInfo -> ([VarName], [Type])
constructorArgTypes i =
( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters),
i ^. constructorInfoArgs
)
constructorType :: Member (Reader InfoTable) r => Name -> Sem r Type
constructorType c = do
info <- lookupConstructor c
let (inductiveParams, constrArgs) = constructorArgTypes info
args =
map (\ty -> FunctionArgTypeAbstraction (Implicit, ty)) inductiveParams
++ map FunctionArgTypeType constrArgs
ind = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
saturatedTy =
foldl'
( \t v ->
TypeApp
( TypeApplication
{ _typeAppLeft = t,
_typeAppRight = TypeIden (TypeIdenVariable v),
_typeAppImplicit = Implicit
}
)
)
ind
inductiveParams
return (foldFunType args saturatedTy)

54
src/MiniJuvix/Syntax/MicroJuvix/Language.hs
View File

@ -3,18 +3,23 @@ module MiniJuvix.Syntax.MicroJuvix.Language
module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
module MiniJuvix.Syntax.Concrete.Scoped.Name,
module MiniJuvix.Syntax.Concrete.Loc,
module MiniJuvix.Syntax.IsImplicit,
module MiniJuvix.Syntax.Hole,
module MiniJuvix.Syntax.Wildcard,
module MiniJuvix.Syntax.Concrete.LiteralLoc,
)
where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.Concrete.Language (LiteralLoc)
import MiniJuvix.Syntax.Concrete.LiteralLoc
import MiniJuvix.Syntax.Concrete.Loc
import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
import MiniJuvix.Syntax.Fixity
import MiniJuvix.Syntax.ForeignBlock
import MiniJuvix.Syntax.Hole
import MiniJuvix.Syntax.IsImplicit
import MiniJuvix.Syntax.Wildcard
import Prettyprinter
type FunctionName = Name
@ -97,7 +102,6 @@ data FunctionClause = FunctionClause
_clausePatterns :: [Pattern],
_clauseBody :: Expression
}
deriving stock (Show)
data Iden
= IdenFunction Name
@ -105,19 +109,16 @@ data Iden
| IdenVar VarName
| IdenAxiom Name
| IdenInductive Name
deriving stock (Show)
data TypedExpression = TypedExpression
{ _typedType :: Type,
_typedExpression :: Expression
}
deriving stock (Show)
data FunctionExpression = FunctionExpression
{ _functionExpressionLeft :: Expression,
_functionExpressionRight :: Expression
}
deriving stock (Show)
data Expression
= ExpressionIden Iden
@ -126,19 +127,18 @@ data Expression
| ExpressionLiteral LiteralLoc
| ExpressionHole Hole
| ExpressionTyped TypedExpression
deriving stock (Show)
data Application = Application
{ _appLeft :: Expression,
_appRight :: Expression
_appRight :: Expression,
_appImplicit :: IsImplicit
}
deriving stock (Show)
data Function = Function
{ _funLeft :: Type,
_funRight :: Type
}
deriving stock (Show, Generic, Eq)
deriving stock (Eq, Generic)
instance Hashable Function
@ -147,18 +147,17 @@ data ConstructorApp = ConstructorApp
{ _constrAppConstructor :: Name,
_constrAppParameters :: [Pattern]
}
deriving stock (Show)
data Pattern
= PatternVariable VarName
| PatternConstructorApp ConstructorApp
| PatternWildcard
deriving stock (Show)
| PatternWildcard Wildcard
| PatternBraces Pattern
newtype InductiveParameter = InductiveParameter
{ _inductiveParamName :: VarName
}
deriving stock (Show, Eq)
deriving stock (Eq)
data InductiveDef = InductiveDef
{ _inductiveName :: InductiveName,
@ -175,23 +174,25 @@ data TypeIden
= TypeIdenInductive InductiveName
| TypeIdenAxiom AxiomName
| TypeIdenVariable VarName
deriving stock (Show, Eq, Generic)
deriving stock (Eq, Generic)
instance Hashable TypeIden
data TypeApplication = TypeApplication
{ _typeAppLeft :: Type,
_typeAppRight :: Type
_typeAppRight :: Type,
_typeAppImplicit :: IsImplicit
}
deriving stock (Show, Generic, Eq)
deriving stock (Generic, Eq)
instance Hashable TypeApplication
data TypeAbstraction = TypeAbstraction
{ _typeAbsVar :: VarName,
_typeAbsImplicit :: IsImplicit,
_typeAbsBody :: Type
}
deriving stock (Show, Eq, Generic)
deriving stock (Eq, Generic)
instance Hashable TypeAbstraction
@ -203,14 +204,13 @@ data Type
| TypeHole Hole
| TypeUniverse
| TypeAny
deriving stock (Eq, Show, Generic)
deriving stock (Eq, Generic)
instance Hashable Type
data FunctionArgType
= FunctionArgTypeAbstraction VarName
= FunctionArgTypeAbstraction (IsImplicit, VarName)
| FunctionArgTypeType Type
deriving stock (Show)
makeLenses ''Module
makeLenses ''Include
@ -276,6 +276,7 @@ instance HasAtomicity Pattern where
PatternConstructorApp a -> atomicity a
PatternVariable {} -> Atom
PatternWildcard {} -> Atom
PatternBraces {} -> Atom
instance HasLoc FunctionExpression where
getLoc (FunctionExpression l r) = getLoc l <> getLoc r
@ -296,3 +297,16 @@ instance HasLoc Iden where
IdenVar v -> getLoc v
IdenAxiom a -> getLoc a
IdenInductive a -> getLoc a
instance HasLoc Pattern where
getLoc = \case
PatternVariable v -> getLoc v
PatternConstructorApp a -> getLoc a
PatternBraces p -> getLoc p
PatternWildcard i -> getLoc i
instance HasLoc ConstructorApp where
getLoc (ConstructorApp c ps) =
case last <$> nonEmpty ps of
Just p -> getLoc c <> getLoc p
Nothing -> getLoc c

65
src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs
View File

@ -88,10 +88,10 @@ mkConcreteType = fmap ConcreteType . go
where
go :: Type -> Maybe Type
go t = case t of
TypeApp (TypeApplication l r) -> do
TypeApp (TypeApplication l r i) -> do
l' <- go l
r' <- go r
return (TypeApp (TypeApplication l' r'))
return (TypeApp (TypeApplication l' r' i))
TypeAny -> return TypeAny
TypeUniverse -> return TypeUniverse
TypeFunction (Function l r) -> do
@ -115,9 +115,9 @@ findHoles = go
go :: Type -> HashSet Hole
go = \case
TypeIden {} -> mempty
TypeApp (TypeApplication a b) -> go a <> go b
TypeApp (TypeApplication a b _) -> go a <> go b
TypeFunction (Function a b) -> go a <> go b
TypeAbs (TypeAbstraction _ t) -> go t
TypeAbs a -> go (a ^. typeAbsBody)
TypeHole h -> HashSet.singleton h
TypeUniverse -> mempty
TypeAny -> mempty
@ -145,7 +145,7 @@ typeAsExpression = go
TypeIdenAxiom a -> IdenAxiom a
TypeIdenVariable v -> IdenVar v
goApp :: TypeApplication -> Application
goApp (TypeApplication l r) = Application (go l) (go r)
goApp (TypeApplication l r i) = Application (go l) (go r) i
goFunction :: Function -> FunctionExpression
goFunction (Function l r) = FunctionExpression (go l) (go r)
@ -179,7 +179,7 @@ fillHoles m = goe
)
where
goApp :: Application -> Application
goApp (Application l r) = Application (goe l) (goe r)
goApp (Application l r i) = Application (goe l) (goe r) i
goFunction :: FunctionExpression -> FunctionExpression
goFunction (FunctionExpression l r) = FunctionExpression (goe l) (goe r)
goHole :: Hole -> Expression
@ -201,9 +201,9 @@ fillHolesType m = go
TypeHole h -> goHole h
where
goApp :: TypeApplication -> TypeApplication
goApp (TypeApplication l r) = TypeApplication (go l) (go r)
goApp (TypeApplication l r i) = TypeApplication (go l) (go r) i
goAbs :: TypeAbstraction -> TypeAbstraction
goAbs (TypeAbstraction v b) = TypeAbstraction v (go b)
goAbs (TypeAbstraction v i b) = TypeAbstraction v i (go b)
goFunction :: Function -> Function
goFunction (Function l r) = Function (go l) (go r)
goHole :: Hole -> Type
@ -235,10 +235,10 @@ expressionAsType = go
IdenAxiom a -> Just (TypeIdenAxiom a)
IdenInductive i -> Just (TypeIdenInductive i)
goApp :: Application -> Maybe TypeApplication
goApp (Application l r) = do
goApp (Application l r i) = do
l' <- go l
r' <- go r
return (TypeApplication l' r')
return (TypeApplication l' r' i)
substituteIndParams :: [(InductiveParameter, Type)] -> Type -> Type
substituteIndParams = substitution . HashMap.fromList . map (first (^. inductiveParamName))
@ -263,7 +263,8 @@ patternVariables :: Pattern -> [VarName]
patternVariables = \case
PatternVariable v -> [v]
PatternConstructorApp a -> goApp a
PatternWildcard -> []
PatternBraces b -> patternVariables b
PatternWildcard {} -> []
where
goApp :: ConstructorApp -> [VarName]
goApp (ConstructorApp _ ps) = concatMap patternVariables ps
@ -326,7 +327,7 @@ concreteTypeToExpr = go . (^. unconcreteType)
go = \case
TypeAbs {} -> impossible
TypeIden i -> ExpressionIden (goIden i)
TypeApp (TypeApplication l r) -> ExpressionApplication (Application (go l) (go r))
TypeApp (TypeApplication l r i) -> ExpressionApplication (Application (go l) (go r) i)
TypeFunction (Function l r) -> ExpressionFunction (FunctionExpression (go l) (go r))
TypeUniverse {} -> impossible
TypeAny {} -> impossible
@ -352,7 +353,7 @@ substitutionE m = go
ExpressionFunction f -> ExpressionFunction (goFunction f)
ExpressionTyped t -> ExpressionTyped (over typedExpression go t)
goApp :: Application -> Application
goApp (Application l r) = Application (go l) (go r)
goApp (Application l r i) = Application (go l) (go r) i
goFunction :: FunctionExpression -> FunctionExpression
goFunction (FunctionExpression l r) = FunctionExpression (go l) (go r)
goIden :: Iden -> Expression
@ -373,12 +374,16 @@ substitution m = go
TypeUniverse -> TypeUniverse
TypeAny -> TypeAny
TypeHole h -> TypeHole h
goApp :: TypeApplication -> TypeApplication
goApp (TypeApplication l r) = TypeApplication (go l) (go r)
goApp (TypeApplication l r i) = TypeApplication (go l) (go r) i
goAbs :: TypeAbstraction -> TypeAbstraction
goAbs (TypeAbstraction v b) = TypeAbstraction v (go b)
goAbs (TypeAbstraction v i b) = TypeAbstraction v i (go b)
goFunction :: Function -> Function
goFunction (Function l r) = Function (go l) (go r)
goIden :: TypeIden -> Type
goIden i = case i of
TypeIdenInductive {} -> TypeIden i
@ -394,14 +399,14 @@ foldFunType l r = case l of
(a : as) ->
let r' = foldFunType as r
in case a of
FunctionArgTypeAbstraction v -> TypeAbs (TypeAbstraction v r')
FunctionArgTypeAbstraction (i, v) -> TypeAbs (TypeAbstraction v i r')
FunctionArgTypeType t -> TypeFunction (Function t r')
-- | a -> (b -> c) ==> ([a, b], c)
unfoldFunType :: Type -> ([FunctionArgType], Type)
unfoldFunType t = case t of
TypeFunction (Function l r) -> first (FunctionArgTypeType l :) (unfoldFunType r)
TypeAbs (TypeAbstraction var r) -> first (FunctionArgTypeAbstraction var :) (unfoldFunType r)
TypeAbs (TypeAbstraction var i r) -> first (FunctionArgTypeAbstraction (i, var) :) (unfoldFunType r)
_ -> ([], t)
unfoldFunConcreteType :: ConcreteType -> ([ConcreteType], ConcreteType)
@ -414,28 +419,34 @@ unfoldFunConcreteType = bimap (map mkConcreteType') mkConcreteType' . go . (^. u
unfoldTypeAbsType :: Type -> ([VarName], Type)
unfoldTypeAbsType t = case t of
TypeAbs (TypeAbstraction var r) -> first (var :) (unfoldTypeAbsType r)
TypeAbs (TypeAbstraction var _ r) -> first (var :) (unfoldTypeAbsType r)
_ -> ([], t)
foldApplication :: Expression -> [Expression] -> Expression
foldExplicitApplication :: Expression -> [Expression] -> Expression
foldExplicitApplication f = foldApplication f . zip (repeat Explicit)
foldApplication :: Expression -> [(IsImplicit, Expression)] -> Expression
foldApplication f args = case args of
[] -> f
(a : as) -> foldApplication (ExpressionApplication (Application f a)) as
((i, a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as
unfoldApplication :: Application -> (Expression, NonEmpty Expression)
unfoldApplication (Application l' r') = second (|: r') (unfoldExpression l')
unfoldApplication' :: Application -> (Expression, NonEmpty (IsImplicit, Expression))
unfoldApplication' (Application l' r' i') = second (|: (i', r')) (unfoldExpression l')
where
unfoldExpression :: Expression -> (Expression, [Expression])
unfoldExpression :: Expression -> (Expression, [(IsImplicit, Expression)])
unfoldExpression e = case e of
ExpressionApplication (Application l r) ->
second (`snoc` r) (unfoldExpression l)
ExpressionApplication (Application l r i) ->
second (`snoc` (i, r)) (unfoldExpression l)
ExpressionTyped t -> unfoldExpression (t ^. typedExpression)
_ -> (e, [])
unfoldApplication :: Application -> (Expression, NonEmpty Expression)
unfoldApplication = fmap (fmap snd) . unfoldApplication'
unfoldTypeApplication :: TypeApplication -> (Type, NonEmpty Type)
unfoldTypeApplication (TypeApplication l' r') = second (|: r') (unfoldType l')
unfoldTypeApplication (TypeApplication l' r' _) = second (|: r') (unfoldType l')
where
unfoldType :: Type -> (Type, [Type])
unfoldType t = case t of
TypeApp (TypeApplication l r) -> second (`snoc` r) (unfoldType l)
TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l)
_ -> (t, [])

1
src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs
View File

@ -8,7 +8,6 @@ data LocalVars = LocalVars
{ _localTypes :: HashMap VarName Type,
_localTyMap :: HashMap VarName VarName
}
deriving stock (Show)
makeLenses ''LocalVars

18
src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs Normal file
View File

@ -0,0 +1,18 @@
module MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult
( module MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult,
)
where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.MicroJuvix.Language
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult (MicroJuvixResult)
data MicroJuvixArityResult = MicroJuvixArityResult
{ _resultMicroJuvixResult :: MicroJuvixResult,
_resultModules :: NonEmpty Module
}
makeLenses ''MicroJuvixArityResult
mainModule :: Lens' MicroJuvixArityResult Module
mainModule = resultModules . _head

4
src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs
View File

@ -7,10 +7,10 @@ where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.MicroJuvix.InfoTable
import MiniJuvix.Syntax.MicroJuvix.Language
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult (MicroJuvixResult)
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult (MicroJuvixArityResult)
data MicroJuvixTypedResult = MicroJuvixTypedResult
{ _resultMicroJuvixResult :: MicroJuvixResult,
{ _resultMicroJuvixArityResult :: MicroJuvixArityResult,
_resultModules :: NonEmpty Module
}

28
src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
View File

@ -52,15 +52,19 @@ instance PrettyCode Iden where
IdenInductive a -> ppCode a
instance PrettyCode TypeApplication where
ppCode (TypeApplication l r) = do
ppCode (TypeApplication l r i) = do
l' <- ppLeftExpression appFixity l
r' <- ppRightExpression appFixity r
return $ l' <+> r'
r' <- case i of
Explicit -> ppRightExpression appFixity r
Implicit -> braces <$> ppCode r
return (l' <+> r')
instance PrettyCode Application where
ppCode a = do
l' <- ppLeftExpression appFixity (a ^. appLeft)
r' <- ppRightExpression appFixity (a ^. appRight)
r' <- case a ^. appImplicit of
Explicit -> ppRightExpression appFixity (a ^. appRight)
Implicit -> braces <$> ppCode (a ^. appRight)
return $ l' <+> r'
instance PrettyCode TypedExpression where
@ -88,7 +92,7 @@ kwInclude :: Doc Ann
kwInclude = keyword Str.include
kwArrow :: Doc Ann
kwArrow = keyword Str.toAscii
kwArrow = keyword Str.toUnicode
kwMapsto :: Doc Ann
kwMapsto = keyword Str.mapstoUnicode
@ -148,9 +152,9 @@ instance PrettyCode BackendItem where
backend <+> kwMapsto <+> pretty _backendItemCode
instance PrettyCode TypeAbstraction where
ppCode (TypeAbstraction v r) = do
ppCode (TypeAbstraction v i r) = do
v' <- ppCode v
let l' = parens (v' <+> colon <+> kwType)
let l' = implicitDelim i (v' <+> colon <+> kwType)
r' <- ppRightExpression funFixity r
return $ l' <+> kwArrow <+> r'
@ -169,7 +173,7 @@ instance PrettyCode TypeIden where
instance PrettyCode FunctionArgType where
ppCode = \case
FunctionArgTypeType t -> ppCode t
FunctionArgTypeAbstraction v -> ppCode v
FunctionArgTypeAbstraction (_, v) -> ppCode v
instance PrettyCode Hole where
ppCode _ = return kwHole
@ -201,6 +205,11 @@ ppBlock ::
Sem r (Doc Ann)
ppBlock items = mapM ppCode items >>= bracesIndent . vsep . toList
implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann
implicitDelim = \case
Implicit -> braces
Explicit -> parens
bracesIndent :: Members '[Reader Options] r => Doc Ann -> Sem r (Doc Ann)
bracesIndent d = do
d' <- indent' d
@ -229,7 +238,8 @@ instance PrettyCode Pattern where
ppCode p = case p of
PatternVariable v -> ppCode v
PatternConstructorApp a -> ppCode a
PatternWildcard -> return kwWildcard
PatternWildcard {} -> return kwWildcard
PatternBraces b -> braces <$> ppCode b
instance PrettyCode FunctionDef where
ppCode f = do

2
src/MiniJuvix/Syntax/MicroJuvix/Pretty/Options.hs
View File

@ -11,7 +11,7 @@ defaultOptions :: Options
defaultOptions =
Options
{ _optIndent = 2,
_optShowNameIds = True
_optShowNameIds = False
}
makeLenses ''Options

108
src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
View File

@ -7,24 +7,23 @@ where
import Data.HashMap.Strict qualified as HashMap
import MiniJuvix.Prelude hiding (fromEither)
import MiniJuvix.Syntax.Concrete.Language (LiteralLoc)
import MiniJuvix.Syntax.MicroJuvix.Error
import MiniJuvix.Syntax.MicroJuvix.InfoTable
import MiniJuvix.Syntax.MicroJuvix.Language.Extra
import MiniJuvix.Syntax.MicroJuvix.LocalVars
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult
import MiniJuvix.Syntax.MicroJuvix.TypeChecker.Inference
entryMicroJuvixTyped ::
Member (Error TypeCheckerError) r =>
MicroJuvixResult ->
MicroJuvixArityResult ->
Sem r MicroJuvixTypedResult
entryMicroJuvixTyped res@MicroJuvixResult {..} = do
entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
r <- runReader table (mapM checkModule _resultModules)
return
MicroJuvixTypedResult
{ _resultMicroJuvixResult = res,
{ _resultMicroJuvixArityResult = res,
_resultModules = r
}
where
@ -98,11 +97,11 @@ checkFunctionDefType = go
TypeAny -> return ()
TypeUniverse -> return ()
goApp :: TypeApplication -> Sem r ()
goApp (TypeApplication a b) = go a >> go b
goApp (TypeApplication a b _) = go a >> go b
goFunction :: Function -> Sem r ()
goFunction (Function a b) = go a >> go b
goAbs :: TypeAbstraction -> Sem r ()
goAbs (TypeAbstraction _ b) = go b
goAbs (TypeAbstraction _ _ b) = go b
checkExpression ::
Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars, Inference] r =>
@ -133,33 +132,6 @@ inferExpression = fmap ExpressionTyped . inferExpression'
lookupVar :: Member (Reader LocalVars) r => Name -> Sem r Type
lookupVar v = HashMap.lookupDefault impossible v <$> asks (^. localTypes)
constructorType :: Member (Reader InfoTable) r => Name -> Sem r Type
constructorType c = do
info <- lookupConstructor c
let (as, bs) = constructorArgTypes info
args =
map FunctionArgTypeAbstraction as
++ map FunctionArgTypeType bs
ind = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
saturatedTy =
foldl'
( \t v ->
TypeApp
( TypeApplication
t
(TypeIden (TypeIdenVariable v))
)
)
ind
as
return (foldFunType args saturatedTy)
constructorArgTypes :: ConstructorInfo -> ([VarName], [Type])
constructorArgTypes i =
( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters),
i ^. constructorInfoArgs
)
checkFunctionClauseBody ::
Members '[Reader InfoTable, Error TypeCheckerError, Inference] r =>
LocalVars ->
@ -174,12 +146,12 @@ checkFunctionClause ::
FunctionInfo ->
FunctionClause ->
Sem r FunctionClause
checkFunctionClause info clause@FunctionClause {..} = do
checkFunctionClause info FunctionClause {..} = do
let (argTys, rty) = unfoldFunType (info ^. functionInfoDef . funDefType)
(patTys, restTys) = splitAt (length _clausePatterns) argTys
bodyTy = foldFunType restTys rty
if
| length patTys /= length _clausePatterns -> throw (tyErr patTys)
| length patTys /= length _clausePatterns -> impossible
| otherwise -> do
locals <- checkPatterns _clauseName (zipExact patTys _clausePatterns)
let bodyTy' =
@ -195,28 +167,13 @@ checkFunctionClause info clause@FunctionClause {..} = do
{ _clauseBody = _clauseBody',
..
}
where
tyErr :: [FunctionArgType] -> TypeCheckerError
tyErr patTys =
ErrTooManyPatterns
( TooManyPatterns
{ _tooManyPatternsClause = clause,
_tooManyPatternsTypes = patTys
}
)
checkPatterns ::
Members '[Reader InfoTable, Error TypeCheckerError] r =>
FunctionName ->
[(FunctionArgType, Pattern)] ->
Sem r LocalVars
checkPatterns name = execState emptyLocalVars . go
where
go ::
Members '[Error TypeCheckerError, Reader InfoTable, State LocalVars] r =>
[(FunctionArgType, Pattern)] ->
Sem r ()
go = mapM_ (uncurry (checkPattern name))
checkPatterns name = execState emptyLocalVars . mapM_ (uncurry (checkPattern name))
typeOfArg :: FunctionArgType -> Type
typeOfArg a = case a of
@ -236,12 +193,16 @@ checkPattern funName = go
go argTy p = do
tyVarMap <- fmap (TypeIden . TypeIdenVariable) . (^. localTyMap) <$> get
let ty = substitution tyVarMap (typeOfArg argTy)
case p of
PatternWildcard -> return ()
unbrace = \case
PatternBraces b -> b
x -> x
case unbrace p of
PatternWildcard {} -> return ()
PatternBraces {} -> impossible
PatternVariable v -> do
modify (addType v ty)
case argTy of
FunctionArgTypeAbstraction v' -> do
FunctionArgTypeAbstraction (_, v') -> do
modify (over localTyMap (HashMap.insert v' v))
_ -> return ()
PatternConstructorApp a -> do
@ -263,16 +224,17 @@ checkPattern funName = go
let psTys' = map (substituteIndParams ctx) psTys
expectedNum = length psTys
let w = map FunctionArgTypeType psTys'
when (expectedNum /= length ps) (throw (appErr app w))
when (expectedNum /= length ps) (throw (appErr app expectedNum))
zipWithM_ go w ps
appErr :: ConstructorApp -> [FunctionArgType] -> TypeCheckerError
appErr app tys =
ErrWrongConstructorAppArgs
( WrongConstructorAppArgs
{ _wrongCtorAppApp = app,
_wrongCtorAppTypes = tys,
_wrongCtorAppName = funName
}
appErr :: ConstructorApp -> Int -> TypeCheckerError
appErr app expected =
ErrArity
( ErrWrongConstructorAppLength
( WrongConstructorAppLength
{ _wrongConstructorAppLength = app,
_wrongConstructorAppLengthExpected = expected
}
)
)
checkSaturatedInductive :: Type -> Sem r (InductiveName, [(InductiveParameter, Type)])
checkSaturatedInductive t = do
@ -306,6 +268,7 @@ inferExpression' e = case e of
return (TypedExpression TypeUniverse (ExpressionFunction (FunctionExpression l' r')))
goLiteral :: LiteralLoc -> Sem r TypedExpression
goLiteral l = return (TypedExpression TypeAny (ExpressionLiteral l))
inferIden :: Iden -> Sem r TypedExpression
inferIden i = case i of
IdenFunction fun -> do
@ -321,17 +284,12 @@ inferExpression' e = case e of
info <- lookupAxiom v
return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i))
IdenInductive v -> do
info <- lookupInductive v
let ps = info ^. inductiveInfoDef . inductiveParameters
kind =
foldr
(\p k -> TypeAbs (TypeAbstraction (p ^. inductiveParamName) k))
TypeUniverse
ps
kind <- inductiveType v
return (TypedExpression kind (ExpressionIden i))
inferApplication :: Application -> Sem r TypedExpression
inferApplication a = do
let leftExp = a ^. appLeft
i = a ^. appImplicit
l <- inferExpression' leftExp
fun <- getFunctionType leftExp (l ^. typedType)
case fun of
@ -344,7 +302,8 @@ inferExpression' e = case e of
ExpressionApplication
Application
{ _appLeft = ExpressionTyped l,
_appRight = r
_appRight = r,
_appImplicit = i
},
_typedType = substituteType1 (ta ^. typeAbsVar, tr) (ta ^. typeAbsBody)
}
@ -356,7 +315,8 @@ inferExpression' e = case e of
ExpressionApplication
Application
{ _appLeft = ExpressionTyped l,
_appRight = r
_appRight = r,
_appImplicit = i
},
_typedType = f ^. funRight
}
@ -389,6 +349,6 @@ viewInductiveApp ty = case t of
viewTypeApp :: Type -> (Type, [Type])
viewTypeApp t = case t of
TypeApp (TypeApplication l r) ->
TypeApp (TypeApplication l r _) ->
second (`snoc` r) (viewTypeApp l)
_ -> (t, [])

10
src/MiniJuvix/Syntax/MicroJuvix/TypeChecker/Inference.hs
View File

@ -50,15 +50,15 @@ closeState = \case
goType :: Type -> Sem r' Type
goType t = case t of
TypeIden {} -> return t
TypeApp (TypeApplication a b) -> do
TypeApp (TypeApplication a b i) -> do
a' <- goType a
b' <- goType b
return (TypeApp (TypeApplication a' b'))
return (TypeApp (TypeApplication a' b' i))
TypeFunction (Function a b) -> do
a' <- goType a
b' <- goType b
return (TypeFunction (Function a' b'))
TypeAbs (TypeAbstraction v b) -> TypeAbs . TypeAbstraction v <$> goType b
TypeAbs (TypeAbstraction v i b) -> TypeAbs . TypeAbstraction v i <$> goType b
TypeUniverse -> return TypeUniverse
TypeAny -> return TypeAny
TypeHole h' ->
@ -142,11 +142,11 @@ re = reinterpret $ \case
return (a == b || mappedEq)
_ -> return False
goApp :: TypeApplication -> TypeApplication -> Sem r Bool
goApp (TypeApplication f x) (TypeApplication f' x') = andM [go f f', go x x']
goApp (TypeApplication f x _) (TypeApplication f' x' _) = andM [go f f', go x x']
goFunction :: Function -> Function -> Sem r Bool
goFunction (Function l r) (Function l' r') = andM [go l l', go r r']
goAbs :: TypeAbstraction -> TypeAbstraction -> Sem r Bool
goAbs (TypeAbstraction v1 r) (TypeAbstraction v2 r') =
goAbs (TypeAbstraction v1 _ r) (TypeAbstraction v2 _ r') =
local (HashMap.insert v1 v2) (go r r')
runInference :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem r Expression

1
src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs
View File

@ -23,7 +23,6 @@ data InfoTable = InfoTable
_infoFunctions :: HashMap Name FunctionInfo
}
-- TODO temporary function.
buildTable :: Module -> InfoTable
buildTable m = InfoTable {..}
where

16
src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs
View File

@ -6,16 +6,17 @@ where
import Data.HashMap.Strict qualified as HashMap
import MiniJuvix.Prelude
import MiniJuvix.Syntax.Abstract.AbstractResult qualified as A
import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as S
import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoper
import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as Micro
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as Micro
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
import MiniJuvix.Syntax.MonoJuvix.InfoTable
import MiniJuvix.Syntax.MonoJuvix.Language
type CompileInfoTable = HashMap S.NameId S.CompileInfo
type CompileInfoTable = HashMap Scoper.NameId Scoper.CompileInfo
data MonoJuvixResult = MonoJuvixResult
{ _resultMicroTyped :: Micro.MicroJuvixTypedResult,
@ -27,12 +28,13 @@ makeLenses ''MonoJuvixResult
compileInfoTable :: MonoJuvixResult -> CompileInfoTable
compileInfoTable r =
HashMap.mapKeys
(^. S.nameId)
(^. Scoper.nameId)
( r
^. resultMicroTyped
. Micro.resultMicroJuvixArityResult
. Micro.resultMicroJuvixResult
. Micro.resultAbstract
. A.resultScoper
. Abstract.resultScoper
. Scoper.resultScoperTable
. S.infoCompilationRules
. Scoper.infoCompilationRules
)

26
src/MiniJuvix/Syntax/Wildcard.hs Normal file
View File

@ -0,0 +1,26 @@
module MiniJuvix.Syntax.Wildcard where
import MiniJuvix.Prelude
import Prettyprinter
newtype Wildcard = Wildcard
{ _wildcardLoc :: Interval
}
deriving stock (Show)
makeLenses ''Wildcard
instance Eq Wildcard where
_ == _ = True
instance Ord Wildcard where
compare _ _ = EQ
instance Hashable Wildcard where
hashWithSalt s _ = hashWithSalt s (0 :: Int)
instance HasLoc Wildcard where
getLoc = (^. wildcardLoc)
instance Pretty Wildcard where
pretty = const "_"

2
src/MiniJuvix/Termination/Checker.hs
View File

@ -102,7 +102,7 @@ checkApplication ::
Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
Application ->
Sem r ()
checkApplication (Application l r) = do
checkApplication (Application l r _) = do
checkExpression l
checkExpression r

2
src/MiniJuvix/Termination/FunctionCall.hs
View File

@ -14,7 +14,7 @@ viewCall ::
Expression ->
Sem r (Maybe FunCall)
viewCall = \case
ExpressionApplication (Application f x) -> do
ExpressionApplication (Application f x _) -> do
c <- viewCall f
x' <- callArg
return $ over callArgs (`snoc` x') <$> c

21
src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
View File

@ -151,7 +151,14 @@ goFunction (Abstract.Function l r) = do
l' <- goFunctionParameter l
r' <- goType r
return $ case l' of
Left tyvar -> TypeAbs (TypeAbstraction tyvar r')
Left tyVar ->
TypeAbs
( TypeAbstraction
{ _typeAbsVar = tyVar,
_typeAbsImplicit = l ^. Abstract.paramImplicit,
_typeAbsBody = r'
}
)
Right ty -> TypeFunction (Function ty r')
goFunctionDef :: Abstract.FunctionDef -> Sem r FunctionDef
@ -183,7 +190,8 @@ goPattern :: Abstract.Pattern -> Sem r Pattern
goPattern p = case p of
Abstract.PatternVariable v -> return (PatternVariable (goSymbol v))
Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
Abstract.PatternWildcard -> return PatternWildcard
Abstract.PatternWildcard i -> return (PatternWildcard i)
Abstract.PatternBraces b -> PatternBraces <$> goPattern b
Abstract.PatternEmpty -> unsupported "pattern empty"
goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp
@ -218,10 +226,10 @@ goType e = case e of
Abstract.ExpressionHole h -> return (TypeHole h)
goApplication :: Abstract.Application -> Sem r Application
goApplication (Abstract.Application f x) = do
goApplication (Abstract.Application f x i) = do
f' <- goExpression f
x' <- goExpression x
return (Application f' x')
return (Application f' x' i)
goIden :: Abstract.Iden -> Iden
goIden i = case i of
@ -291,13 +299,14 @@ goInductiveDef i = case i ^. Abstract.inductiveType of
goConstructorType = fmap fst . viewConstructorType
goTypeApplication :: Abstract.Application -> Sem r TypeApplication
goTypeApplication (Abstract.Application l r) = do
goTypeApplication (Abstract.Application l r i) = do
l' <- goType l
r' <- goType r
return
TypeApplication
{ _typeAppLeft = l',
_typeAppRight = r'
_typeAppRight = r',
_typeAppImplicit = i
}
viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type)

1
src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs
View File

@ -451,6 +451,7 @@ goPattern' ty = \case
Micro.PatternVariable v -> return (PatternVariable (goName v))
Micro.PatternConstructorApp capp -> PatternConstructorApp <$> goApp capp
Micro.PatternWildcard {} -> return PatternWildcard
Micro.PatternBraces b -> goPattern' ty b
where
goApp :: Micro.ConstructorApp -> Sem r ConstructorApp
goApp capp = case ty ^. Micro.unconcreteType of

191
src/MiniJuvix/Translation/ScopedToAbstract.hs
View File

@ -8,16 +8,16 @@ import MiniJuvix.Prelude
import MiniJuvix.Syntax.Abstract.AbstractResult
import MiniJuvix.Syntax.Abstract.InfoTableBuilder
import MiniJuvix.Syntax.Abstract.Language (FunctionDef (_funDefTypeSig))
import MiniJuvix.Syntax.Abstract.Language qualified as A
import MiniJuvix.Syntax.Concrete.Language
import MiniJuvix.Syntax.Concrete.Language qualified as C
import MiniJuvix.Syntax.Abstract.Language qualified as Abstract
import MiniJuvix.Syntax.Concrete.Language qualified as Concrete
import MiniJuvix.Syntax.Concrete.Scoped.Error
import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
unsupported :: Text -> a
unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported"
entryAbstract :: Scoper.ScoperResult -> Sem r AbstractResult
entryAbstract :: Member (Error ScoperError) r => Scoper.ScoperResult -> Sem r AbstractResult
entryAbstract _resultScoper = do
(_resultTable, _resultModules) <- runInfoTableBuilder (mapM goTopModule ms)
return AbstractResult {..}
@ -25,33 +25,33 @@ entryAbstract _resultScoper = do
ms = _resultScoper ^. Scoper.resultModules
goTopModule ::
Members '[InfoTableBuilder] r =>
Members '[InfoTableBuilder, Error ScoperError] r =>
Module 'Scoped 'ModuleTop ->
Sem r A.TopModule
Sem r Abstract.TopModule
goTopModule = goModule
goLocalModule ::
Members '[InfoTableBuilder] r =>
Members '[InfoTableBuilder, Error ScoperError] r =>
Module 'Scoped 'ModuleLocal ->
Sem r A.LocalModule
Sem r Abstract.LocalModule
goLocalModule = goModule
goModule ::
(Members '[InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) =>
(Members '[InfoTableBuilder, Error ScoperError] r, ModulePathType 'Scoped t ~ S.Name' c) =>
Module 'Scoped t ->
Sem r (A.Module c)
Sem r (Abstract.Module c)
goModule (Module n par b) = case par of
[] -> A.Module n <$> goModuleBody b
[] -> Abstract.Module n <$> goModuleBody b
_ -> unsupported "Module parameters"
goModuleBody ::
forall r.
Members '[InfoTableBuilder] r =>
Members '[InfoTableBuilder, Error ScoperError] r =>
[Statement 'Scoped] ->
Sem r A.ModuleBody
Sem r Abstract.ModuleBody
goModuleBody ss' = do
otherThanFunctions <- mapMaybeM goStatement ss
functions <- map (fmap A.StatementFunction) <$> compiledFunctions
functions <- map (fmap Abstract.StatementFunction) <$> compiledFunctions
let _moduleStatements =
map
(^. indexedThing)
@ -59,12 +59,12 @@ goModuleBody ss' = do
(^. indexedIx)
(otherThanFunctions <> functions)
)
return A.ModuleBody {..}
return Abstract.ModuleBody {..}
where
ss :: [Indexed (Statement 'Scoped)]
ss = zipWith Indexed [0 ..] ss'
compiledFunctions :: Sem r [Indexed A.FunctionDef]
compiledFunctions :: Sem r [Indexed Abstract.FunctionDef]
compiledFunctions =
sequence $
[ Indexed i <$> funDef
@ -83,46 +83,47 @@ goModuleBody ss' = do
goStatement ::
forall r.
Members '[InfoTableBuilder] r =>
Members '[InfoTableBuilder, Error ScoperError] r =>
Indexed (Statement 'Scoped) ->
Sem r (Maybe (Indexed A.Statement))
Sem r (Maybe (Indexed Abstract.Statement))
goStatement (Indexed idx s) =
fmap (Indexed idx) <$> case s of
StatementAxiom d -> Just . A.StatementAxiom <$> goAxiom d
StatementImport (Import t) -> Just . A.StatementImport <$> goModule t
StatementAxiom d -> Just . Abstract.StatementAxiom <$> goAxiom d
StatementImport (Import t) -> Just . Abstract.StatementImport <$> goModule t
StatementOperator {} -> return Nothing
StatementOpenModule {} -> return Nothing
StatementEval {} -> unsupported "eval statements"
StatementPrint {} -> unsupported "print statements"
StatementInductive i -> Just . A.StatementInductive <$> goInductive i
StatementForeign f -> return (Just (A.StatementForeign f))
StatementModule f -> Just . A.StatementLocalModule <$> goLocalModule f
StatementInductive i -> Just . Abstract.StatementInductive <$> goInductive i
StatementForeign f -> return (Just (Abstract.StatementForeign f))
StatementModule f -> Just . Abstract.StatementLocalModule <$> goLocalModule f
StatementTypeSignature {} -> return Nothing
StatementFunctionClause {} -> return Nothing
StatementCompile {} -> return Nothing
goFunctionDef ::
forall r.
Members '[InfoTableBuilder] r =>
Members '[InfoTableBuilder, Error ScoperError] r =>
TypeSignature 'Scoped ->
NonEmpty (FunctionClause 'Scoped) ->
Sem r A.FunctionDef
Sem r Abstract.FunctionDef
goFunctionDef TypeSignature {..} clauses = do
let _funDefName = _sigName
_funDefTerminating = _sigTerminating
_funDefClauses <- mapM goFunctionClause clauses
_funDefTypeSig <- goExpression _sigType
registerFunction' A.FunctionDef {..}
registerFunction' Abstract.FunctionDef {..}
goFunctionClause ::
Member (Error ScoperError) r =>
FunctionClause 'Scoped ->
Sem r A.FunctionClause
Sem r Abstract.FunctionClause
goFunctionClause FunctionClause {..} = do
_clausePatterns' <- mapM goPattern _clausePatterns
_clauseBody' <- goExpression _clauseBody
goWhereBlock _clauseWhere
return
A.FunctionClause
Abstract.FunctionClause
{ _clausePatterns = _clausePatterns',
_clauseBody = _clauseBody'
}
@ -135,28 +136,30 @@ goWhereBlock w = case w of
Nothing -> return ()
goInductiveParameter ::
Member (Error ScoperError) r =>
InductiveParameter 'Scoped ->
Sem r A.FunctionParameter
Sem r Abstract.FunctionParameter
goInductiveParameter InductiveParameter {..} = do
paramType' <- goExpression _inductiveParameterType
return
A.FunctionParameter
Abstract.FunctionParameter
{ _paramType = paramType',
_paramName = Just _inductiveParameterName,
_paramImplicit = Explicit,
_paramUsage = UsageOmega
}
goInductive ::
Members '[InfoTableBuilder] r =>
Members '[InfoTableBuilder, Error ScoperError] r =>
InductiveDef 'Scoped ->
Sem r A.InductiveDef
Sem r Abstract.InductiveDef
goInductive InductiveDef {..} = do
_inductiveParameters' <- mapM goInductiveParameter _inductiveParameters
_inductiveType' <- mapM goExpression _inductiveType
_inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
inductiveInfo <-
registerInductive
A.InductiveDef
Abstract.InductiveDef
{ _inductiveParameters = _inductiveParameters',
_inductiveName = _inductiveName,
_inductiveType = _inductiveType',
@ -164,67 +167,75 @@ goInductive InductiveDef {..} = do
}
forM_ _inductiveConstructors' (registerConstructor inductiveInfo)
return (inductiveInfo ^. inductiveInfoDef)
goConstructorDef ::
Member (Error ScoperError) r =>
InductiveConstructorDef 'Scoped ->
Sem r A.InductiveConstructorDef
Sem r Abstract.InductiveConstructorDef
goConstructorDef (InductiveConstructorDef c ty) =
A.InductiveConstructorDef c <$> goExpression ty
Abstract.InductiveConstructorDef c <$> goExpression ty
goExpression ::
forall r.
Member (Error ScoperError) r =>
Expression ->
Sem r A.Expression
Sem r Abstract.Expression
goExpression = \case
ExpressionIdentifier nt -> return (goIden nt)
ExpressionParensIdentifier nt -> return (goIden nt)
ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
ExpressionInfixApplication ia -> A.ExpressionApplication <$> goInfix ia
ExpressionPostfixApplication pa -> A.ExpressionApplication <$> goPostfix pa
ExpressionLiteral l -> return (A.ExpressionLiteral l)
ExpressionApplication a -> Abstract.ExpressionApplication <$> goApplication a
ExpressionInfixApplication ia -> Abstract.ExpressionApplication <$> goInfix ia
ExpressionPostfixApplication pa -> Abstract.ExpressionApplication <$> goPostfix pa
ExpressionLiteral l -> return (Abstract.ExpressionLiteral l)
ExpressionLambda {} -> unsupported "Lambda"
ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b))
ExpressionMatch {} -> unsupported "Match"
ExpressionLetBlock {} -> unsupported "Let Block"
ExpressionUniverse uni -> return $ A.ExpressionUniverse (goUniverse uni)
ExpressionFunction func -> A.ExpressionFunction <$> goFunction func
ExpressionHole h -> return (A.ExpressionHole h)
ExpressionUniverse uni -> return (Abstract.ExpressionUniverse (goUniverse uni))
ExpressionFunction func -> Abstract.ExpressionFunction <$> goFunction func
ExpressionHole h -> return (Abstract.ExpressionHole h)
where
goIden :: C.ScopedIden -> A.Expression
goIden x = A.ExpressionIden $ case x of
ScopedAxiom a -> A.IdenAxiom (A.AxiomRef (a ^. C.axiomRefName))
ScopedInductive i -> A.IdenInductive (A.InductiveRef (i ^. C.inductiveRefName))
ScopedVar v -> A.IdenVar v
ScopedFunction fun -> A.IdenFunction (A.FunctionRef (fun ^. C.functionRefName))
ScopedConstructor c -> A.IdenConstructor (A.ConstructorRef (c ^. C.constructorRefName))
goIden :: Concrete.ScopedIden -> Abstract.Expression
goIden x = Abstract.ExpressionIden $ case x of
ScopedAxiom a -> Abstract.IdenAxiom (Abstract.AxiomRef (a ^. Concrete.axiomRefName))
ScopedInductive i -> Abstract.IdenInductive (Abstract.InductiveRef (i ^. Concrete.inductiveRefName))
ScopedVar v -> Abstract.IdenVar v
ScopedFunction fun -> Abstract.IdenFunction (Abstract.FunctionRef (fun ^. Concrete.functionRefName))
ScopedConstructor c -> Abstract.IdenConstructor (Abstract.ConstructorRef (c ^. Concrete.constructorRefName))
goApplication :: Application -> Sem r A.Application
goApplication (Application l r) = do
goApplication :: Application -> Sem r Abstract.Application
goApplication (Application l arg) = do
l' <- goExpression l
r' <- goExpression r
return (A.Application l' r')
return (Abstract.Application l' r' i)
where
(r, i) = case arg of
ExpressionBraces b -> (b ^. withLocParam, Implicit)
_ -> (arg, Explicit)
goPostfix :: PostfixApplication -> Sem r A.Application
goPostfix :: PostfixApplication -> Sem r Abstract.Application
goPostfix (PostfixApplication l op) = do
l' <- goExpression l
let op' = goIden op
return (A.Application op' l')
return (Abstract.Application op' l' Explicit)
goInfix :: InfixApplication -> Sem r A.Application
goInfix :: InfixApplication -> Sem r Abstract.Application
goInfix (InfixApplication l op r) = do
l' <- goExpression l
let op' = goIden op
l'' = Abstract.ExpressionApplication (Abstract.Application op' l' Explicit)
r' <- goExpression r
return $ A.Application (A.ExpressionApplication (A.Application op' l')) r'
return (Abstract.Application l'' r' Explicit)
goUniverse :: Universe -> Universe
goUniverse = id
goFunction :: Function 'Scoped -> Sem r A.Function
goFunction :: Member (Error ScoperError) r => Function 'Scoped -> Sem r Abstract.Function
goFunction (Function l r) = do
_funParameter <- goFunctionParameter l
_funReturn <- goExpression r
return A.Function {..}
return Abstract.Function {..}
defaultUsage :: Usage
defaultUsage = UsageOmega
@ -233,34 +244,40 @@ goUsage :: Maybe Usage -> Usage
goUsage = fromMaybe defaultUsage
goFunctionParameter ::
Member (Error ScoperError) r =>
FunctionParameter 'Scoped ->
Sem r A.FunctionParameter
goFunctionParameter (FunctionParameter _paramName u ty) = do
_paramType <- goExpression ty
let _paramUsage = goUsage u
return A.FunctionParameter {..}
Sem r Abstract.FunctionParameter
goFunctionParameter (FunctionParameter {..}) = do
_paramType' <- goExpression _paramType
return
Abstract.FunctionParameter
{ Abstract._paramUsage = goUsage _paramUsage,
Abstract._paramType = _paramType',
Abstract._paramImplicit = _paramImplicit,
Abstract._paramName = _paramName
}
goPatternApplication ::
PatternApp ->
Sem r A.ConstructorApp
goPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternApplication a)
Sem r Abstract.ConstructorApp
goPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternApplication a)
goPatternConstructor ::
ConstructorRef ->
Sem r A.ConstructorApp
goPatternConstructor a = uncurry A.ConstructorApp <$> viewApp (PatternConstructor a)
Sem r Abstract.ConstructorApp
goPatternConstructor a = uncurry Abstract.ConstructorApp <$> viewApp (PatternConstructor a)
goInfixPatternApplication ::
PatternInfixApp ->
Sem r A.ConstructorApp
goInfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternInfixApplication a)
Sem r Abstract.ConstructorApp
goInfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternInfixApplication a)
goPostfixPatternApplication ::
PatternPostfixApp ->
Sem r A.ConstructorApp
goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPostfixApplication a)
Sem r Abstract.ConstructorApp
goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a)
viewApp :: forall r. Pattern -> Sem r (A.ConstructorRef, [A.Pattern])
viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.Pattern])
viewApp = \case
PatternConstructor c -> return (goConstructorRef c, [])
PatternApplication (PatternApp l r) -> do
@ -275,25 +292,27 @@ viewApp = \case
return (goConstructorRef c, [l'])
PatternVariable {} -> err
PatternWildcard {} -> err
PatternBraces {} -> err
PatternEmpty {} -> err
where
err :: a
err = error "constructor expected on the left of a pattern application"
goConstructorRef :: ConstructorRef -> A.ConstructorRef
goConstructorRef (ConstructorRef' n) = A.ConstructorRef n
goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef
goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef n
goPattern :: Pattern -> Sem r A.Pattern
goPattern :: Pattern -> Sem r Abstract.Pattern
goPattern p = case p of
PatternVariable a -> return $ A.PatternVariable a
PatternConstructor c -> A.PatternConstructorApp <$> goPatternConstructor c
PatternApplication a -> A.PatternConstructorApp <$> goPatternApplication a
PatternInfixApplication a -> A.PatternConstructorApp <$> goInfixPatternApplication a
PatternPostfixApplication a -> A.PatternConstructorApp <$> goPostfixPatternApplication a
PatternWildcard -> return A.PatternWildcard
PatternEmpty -> return A.PatternEmpty
PatternVariable a -> return $ Abstract.PatternVariable a
PatternConstructor c -> Abstract.PatternConstructorApp <$> goPatternConstructor c
PatternApplication a -> Abstract.PatternConstructorApp <$> goPatternApplication a
PatternInfixApplication a -> Abstract.PatternConstructorApp <$> goInfixPatternApplication a
PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a
PatternWildcard i -> return (Abstract.PatternWildcard i)
PatternEmpty -> return Abstract.PatternEmpty
PatternBraces b -> Abstract.PatternBraces <$> goPattern b
goAxiom :: Members '[InfoTableBuilder] r => AxiomDef 'Scoped -> Sem r A.AxiomDef
goAxiom :: Members '[InfoTableBuilder, Error ScoperError] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
goAxiom AxiomDef {..} = do
_axiomType' <- goExpression _axiomType
registerAxiom' A.AxiomDef {_axiomType = _axiomType', ..}
registerAxiom' Abstract.AxiomDef {_axiomType = _axiomType', ..}

10
test/Arity.hs Normal file
View File

@ -0,0 +1,10 @@
module Arity
( allTests,
)
where
import Arity.Negative qualified as N
import Base
allTests :: TestTree
allTests = testGroup "Arity tests" [N.allTests]

87
test/Arity/Negative.hs Normal file
View File

@ -0,0 +1,87 @@
module Arity.Negative (allTests) where
import Base
import MiniJuvix.Pipeline
import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error
type FailMsg = String
data NegTest = NegTest
{ _name :: String,
_relDir :: FilePath,
_file :: FilePath,
_checkErr :: ArityCheckerError -> Maybe FailMsg
}
testDescr :: NegTest -> TestDescr
testDescr NegTest {..} =
let tRoot = root </> _relDir
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Single $ do
let entryPoint = defaultEntryPoint _file
result <- runIOEither (upToMicroJuvixArity entryPoint)
case mapLeft fromMiniJuvixError result of
Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
Left Nothing -> assertFailure "The arity checker did not find an error."
Right _ -> assertFailure "An error ocurred but it was not in the arity checker."
}
allTests :: TestTree
allTests =
testGroup
"Arity checker negative tests"
(map (mkTest . testDescr) tests)
root :: FilePath
root = "tests/negative"
wrongError :: Maybe FailMsg
wrongError = Just "Incorrect error"
tests :: [NegTest]
tests =
[ NegTest
"Too many arguments in expression"
"MicroJuvix"
"TooManyArguments.mjuvix"
$ \case
ErrTooManyArguments {} -> Nothing
_ -> wrongError,
NegTest
"Pattern match a function type"
"MicroJuvix"
"FunctionPattern.mjuvix"
$ \case
ErrPatternFunction {} -> Nothing
_ -> wrongError,
NegTest
"Function type (* → *) application"
"MicroJuvix"
"FunctionApplied.mjuvix"
$ \case
ErrFunctionApplied {} -> Nothing
_ -> wrongError,
NegTest
"Expected explicit pattern"
"MicroJuvix"
"ExpectedExplicitPattern.mjuvix"
$ \case
ErrExpectedExplicitPattern {} -> Nothing
_ -> wrongError,
NegTest
"Expected explicit argument"
"MicroJuvix"
"ExpectedExplicitArgument.mjuvix"
$ \case
ErrExpectedExplicitArgument {} -> Nothing
_ -> wrongError,
NegTest
"Function clause with two many patterns in the lhs"
"MicroJuvix"
"LhsTooManyPatterns.mjuvix"
$ \case
ErrLhsTooManyPatterns {} -> Nothing
_ -> wrongError
]

2
test/Main.hs
View File

@ -1,5 +1,6 @@
module Main (main) where
import Arity qualified
import BackendC qualified
import Base
import MonoJuvix qualified
@ -19,6 +20,7 @@ fastTests =
"MiniJuvix fast tests"
[ Scope.allTests,
Termination.allTests,
Arity.allTests,
TypeCheck.allTests,
MonoJuvix.allTests
]

2
test/MonoJuvix/Positive.hs
View File

@ -38,7 +38,7 @@ tests =
PosTest
"Polymorphic Simple Fungible Token"
"FullExamples"
"PolySimpleFungibleToken.mjuvix",
"SimpleFungibleTokenImplicit.mjuvix",
PosTest
"Polymorphism and higher rank functions with explicit holes"
"."

21
test/TypeCheck/Negative.hs
View File

@ -49,13 +49,6 @@ tests =
$ \case
ErrWrongConstructorType {} -> Nothing
_ -> wrongError,
NegTest
"Constructor pattern length mismatch"
"MicroJuvix"
"PatternConstructorApp.mjuvix"
$ \case
ErrWrongConstructorAppArgs {} -> Nothing
_ -> wrongError,
NegTest
"Type vs inferred type mismatch"
"MicroJuvix"
@ -70,13 +63,6 @@ tests =
$ \case
ErrExpectedFunctionType {} -> Nothing
_ -> wrongError,
NegTest
"Function definition clause with two many match patterns"
"MicroJuvix"
"TooManyPatterns.mjuvix"
$ \case
ErrTooManyPatterns {} -> Nothing
_ -> wrongError,
NegTest
"Unsolved hole"
"MicroJuvix"
@ -90,12 +76,5 @@ tests =
"MultiWrongType.mjuvix"
$ \case
ErrWrongType {} -> Nothing
_ -> wrongError,
NegTest
"Constructor pattern with arity greater than the constructor"
"MicroJuvix"
"WrongConstructorArity.mjuvix"
$ \case
ErrWrongConstructorAppArgs {} -> Nothing
_ -> wrongError
]

4
test/TypeCheck/Positive.hs
View File

@ -48,9 +48,9 @@ tests =
"MiniHaskell"
"HelloWorld.mjuvix",
PosTest
"PolySimpleFungibleToken with explicit holes"
"PolySimpleFungibleToken"
"FullExamples"
"PolySimpleFungibleTokenHoles.mjuvix",
"SimpleFungibleTokenImplicit.mjuvix",
PosTest
"GHC backend MonoSimpleFungibleToken"
"FullExamples"

8
tests/negative/MicroJuvix/ExpectedExplicitArgument.mjuvix Normal file
View File

@ -0,0 +1,8 @@
module ExpectedExplicitArgument;
inductive T (A : Type) {
c : A → T A;
};
f : {A : Type} → A → T A;
f {A} a ≔ c {A} {a};
end;

8
tests/negative/MicroJuvix/ExpectedExplicitPattern.mjuvix Normal file
View File

@ -0,0 +1,8 @@
module ExpectedExplicitPattern;
inductive T (A : Type) {
c : A → T A;
};
f : {A : Type} → T A → A;
f {_} {c a} ≔ a;
end;

8
tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix
View File

@ -1,12 +1,12 @@
module ExpectedFunctionType;
inductive A {
a : A;
inductive Pair (A : Type) {
mkPair : A → A → Pair A;
};
inductive B {
b : B;
};
f : A;
f ≔ a b;
f : Pair B → Pair B;
f (mkPair a b) ≔ a b;
end;

8
tests/negative/MicroJuvix/FunctionApplied.mjuvix Normal file
View File

@ -0,0 +1,8 @@
module FunctionApplied;
inductive T (A : Type) {
c : A → T;
};
f : {A : Type} → A → T A;
f {A} a ≔ c {(A → A) A} a;
end;

8
tests/negative/MicroJuvix/FunctionPattern.mjuvix Normal file
View File

@ -0,0 +1,8 @@
module FunctionPattern;
inductive T {
A : T;
};
f : (T → T) → T;
f A ≔ A;
end;

8
tests/negative/MicroJuvix/LhsTooManyPatterns.mjuvix Normal file
View File

@ -0,0 +1,8 @@
module LhsTooManyPatterns;
inductive T {
A : T;
};
f : T → T;
f A x ≔ A;
end;

13
tests/negative/MicroJuvix/PatternConstructorApp.mjuvix
View File

@ -1,13 +0,0 @@
module PatternConstructorApp;
inductive A {
a : A -> A;
};
inductive B {
b : B;
};
f : A → B;
f (a x _) ≔ b;
end;

8
tests/negative/MicroJuvix/TooManyArguments.mjuvix Normal file
View File

@ -0,0 +1,8 @@
module TooManyArguments;
inductive T (A : Type) {
c : A → T A;
};
f : {A : Type} → A → T A;
f {A} a ≔ c {A} a a {a} ;
end;

8
tests/negative/MicroJuvix/TooManyPatterns.mjuvix
View File

@ -1,8 +0,0 @@
module TooManyPatterns;
inductive A {
a : A;
};
f : A -> A;
f a _ ≔ a;
end;

2
tests/negative/MicroJuvix/UnsolvedMeta.mjuvix
View File

@ -5,6 +5,6 @@ inductive Proxy (A : Type) {
};
t : Proxy _;
t ≔ x _;
t ≔ x;
end;

4
tests/negative/MicroJuvix/WrongConstructorArity.mjuvix
View File

@ -1,8 +1,8 @@
module WrongConstructorArity;
inductive T {
A : T;
A : T → T;
};
f : T → T;
f (A i) ≔ i;
f (A i x) ≔ i;
end;

329
tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix
View File

@ -1,329 +0,0 @@
module PolySimpleFungibleToken;
foreign ghc {
import Anoma
};
--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------
inductive Bool {
true : Bool;
false : Bool;
};
infixr 2 ||;
|| : Bool → Bool → Bool;
|| false a ≔ a;
|| true _ ≔ true;
infixr 3 &&;
&& : Bool → Bool → Bool;
&& false _ ≔ false;
&& true a ≔ a;
if : (A : Type) → Bool → A → A → A;
if _ true a _ ≔ a;
if _ false _ b ≔ b;
--------------------------------------------------------------------------------
-- Backend Booleans
--------------------------------------------------------------------------------
axiom BackendBool : Type;
compile BackendBool {
ghc ↦ "Bool";
};
axiom backend-true : BackendBool;
compile backend-true {
ghc ↦ "True";
};
axiom backend-false : BackendBool;
compile backend-false {
ghc ↦ "False";
};
--------------------------------------------------------------------------------
-- Backend Bridge
--------------------------------------------------------------------------------
foreign ghc {
bool :: Bool -> a -> a -> a
bool True x _ = x
bool False _ y = y
};
axiom bool : BackendBool → Bool → Bool → Bool;
compile bool {
ghc ↦ "bool";
};
from-backend-bool : BackendBool → Bool;
from-backend-bool bb ≔ bool bb true false;
--------------------------------------------------------------------------------
-- Functions
--------------------------------------------------------------------------------
const : (A : Type) → (B : Type) → A → B → A;
const _ _ a _ ≔ a;
id : (A : Type) → A → A;
id _ a ≔ a;
--------------------------------------------------------------------------------
-- Integers
--------------------------------------------------------------------------------
axiom Int : Type;
compile Int {
ghc ↦ "Int";
};
infix 4 <';
axiom <' : Int → Int → BackendBool;
compile <' {
ghc ↦ "(<)";
};
infix 4 <;
< : Int → Int → Bool;
< i1 i2 ≔ from-backend-bool (i1 <' i2);
axiom eqInt : Int → Int → BackendBool;
compile eqInt {
ghc ↦ "(==)";
};
infix 4 ==Int;
==Int : Int → Int → Bool;
==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2);
infixl 6 -;
axiom - : Int -> Int -> Int;
compile - {
ghc ↦ "(-)";
};
infixl 6 +;
axiom + : Int -> Int -> Int;
compile + {
ghc ↦ "(+)";
};
--------------------------------------------------------------------------------
-- Strings
--------------------------------------------------------------------------------
axiom String : Type;
compile String {
ghc ↦ "[Char]";
};
axiom eqString : String → String → BackendBool;
compile eqString {
ghc ↦ "(==)";
};
infix 4 ==String;
==String : String → String → Bool;
==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
--------------------------------------------------------------------------------
-- Lists
--------------------------------------------------------------------------------
inductive List (A : Type) {
nil : List A;
cons : A → List A → List A;
};
elemGen : (A : Type) → (A → A → Bool) → A → List A → Bool;
elemGen _ _ _ nil ≔ false;
elemGen A eq s (cons x xs) ≔ eq s x || elemGen A eq s xs;
elem : String → List String → Bool;
elem s l ≔ elemGen String (==String) s l;
foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
foldl _ _ f z nil ≔ z;
foldl A B f z (cons h hs) ≔ foldl A B f (f z h) hs;
--------------------------------------------------------------------------------
-- Pair
--------------------------------------------------------------------------------
-- inductive PairIntBool {
-- MakePair : Int → Bool → PairIntBool;
-- };
inductive Pair (A : Type) (B : Type) {
mkPair : A → B → Pair A B;
};
if-pairIntBool : Bool → Pair Int Bool → Pair Int Bool → Pair Int Bool;
if-pairIntBool ≔ if (Pair Int Bool);
--------------------------------------------------------------------------------
-- Maybe
--------------------------------------------------------------------------------
inductive Maybe (A : Type) {
nothing : Maybe A;
just : A → Maybe A;
};
if-optionInt : Bool → Maybe Int → Maybe Int → Maybe Int;
if-optionInt ≔ if (Maybe Int);
from-int : Int → Maybe Int;
from-int i ≔ if-optionInt (i < 0) (nothing Int) (just Int i);
maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B;
maybe _ _ b _ nothing ≔ b;
maybe _ _ _ f (just x) ≔ f x;
maybe-int : Int → Maybe Int → Int;
maybe-int d ≔ maybe Int Int d (id Int);
if-optionString : Bool → Maybe String → Maybe String → Maybe String;
if-optionString ≔ if (Maybe String);
from-string : String → Maybe String;
from-string s ≔ if-optionString (s ==String "") (nothing String) (just String s);
pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool;
pair-from-optionString ≔ maybe String (Pair Int Bool) (mkPair Int Bool 0 false);
--------------------------------------------------------------------------------
-- foldl
--------------------------------------------------------------------------------
foldl' : (Pair Int Bool → String → Pair Int Bool) → Pair Int Bool → List String → Pair Int Bool;
foldl' ≔ foldl String (Pair Int Bool) ;
--------------------------------------------------------------------------------
-- Anoma
--------------------------------------------------------------------------------
axiom readPre : String → Int;
compile readPre {
ghc ↦ "readPre";
};
axiom readPost : String → Int;
compile readPost {
ghc ↦ "readPost";
};
axiom isBalanceKey : String → String → String;
compile isBalanceKey {
ghc ↦ "isBalanceKey";
};
read-pre : String → Maybe Int;
read-pre s ≔ from-int (readPre s);
read-post : String → Maybe Int;
read-post s ≔ from-int (readPost s);
is-balance-key : String → String → Maybe String;
is-balance-key token key ≔ from-string (isBalanceKey token key);
unwrap-default : Maybe Int → Int;
unwrap-default o ≔ maybe-int 0 o;
--------------------------------------------------------------------------------
-- Validity Predicate
--------------------------------------------------------------------------------
change-from-key : String → Int;
change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
check-vp : List String → String → Int → String → Pair Int Bool;
check-vp verifiers key change owner ≔
if-pairIntBool
(change-from-key key < 0)
-- make sure the spender approved the transaction
(mkPair Int Bool (change + (change-from-key key)) (elem owner verifiers))
(mkPair Int Bool (change + (change-from-key key)) true);
check-keys : String → List String → Pair Int Bool → String → Pair Int Bool;
check-keys token verifiers (mkPair change is-success) key ≔
if-pairIntBool
is-success
(pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
(mkPair Int Bool 0 false);
check-result : Pair Int Bool → Bool;
check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked;
vp : String → List String → List String → Bool;
vp token keys-changed verifiers ≔
check-result
(foldl'
(check-keys token verifiers)
(mkPair Int Bool 0 true)
keys-changed);
--------------------------------------------------------------------------------
-- IO
--------------------------------------------------------------------------------
axiom Action : Type;
compile Action {
ghc ↦ "IO ()";
};
axiom putStr : String → Action;
compile putStr {
ghc ↦ "putStr";
};
axiom putStrLn : String → Action;
compile putStrLn {
ghc ↦ "putStrLn";
};
infixl 1 >>;
axiom >> : Action → Action → Action;
compile >> {
ghc ↦ "(>>)";
};
show-result : Bool → String;
show-result true ≔ "OK";
show-result false ≔ "FAIL";
--------------------------------------------------------------------------------
-- Testing VP
--------------------------------------------------------------------------------
token : String;
token ≔ "owner-token";
owner-address : String;
owner-address ≔ "owner-address";
change1-key : String;
change1-key ≔ "change1-key";
change2-key : String;
change2-key ≔ "change2-key";
verifiers : List String;
verifiers ≔ cons String owner-address (nil String);
keys-changed : List String;
keys-changed ≔ cons String change1-key (cons String change2-key (nil String));
main : Action;
main ≔
(putStr "VP Status: ")
>> (putStrLn (show-result (vp token keys-changed verifiers)));
end;

80
tests/positive/FullExamples/PolySimpleFungibleTokenHoles.mjuvix → tests/positive/FullExamples/SimpleFungibleTokenImplicit.mjuvix
View File

@ -1,4 +1,4 @@
module PolySimpleFungibleTokenHoles;
module SimpleFungibleTokenImplicit;
foreign ghc {
import Anoma
@ -23,9 +23,9 @@ infixr 3 &&;
&& false _ ≔ false;
&& true a ≔ a;
if : (A : Type) → Bool → A → A → A;
if _ true a _ ≔ a;
if _ false _ b ≔ b;
if : {A : Type} → Bool → A → A → A;
if true a _ ≔ a;
if false _ b ≔ b;
--------------------------------------------------------------------------------
-- Backend Booleans
@ -69,11 +69,8 @@ from-backend-bool bb ≔ bool bb true false;
-- Functions
--------------------------------------------------------------------------------
const : (A : Type) → (B : Type) → A → B → A;
const _ _ a _ ≔ a;
id : (A : Type) → A → A;
id _ a ≔ a;
id : {A : Type} → A → A;
id a ≔ a;
--------------------------------------------------------------------------------
-- Integers
@ -137,25 +134,28 @@ infix 4 ==String;
-- Lists
--------------------------------------------------------------------------------
infixr 5 ∷;
inductive List (A : Type) {
nil : List A;
cons : A → List A → List A;
∷ : A → List A → List A;
};
elem : (A : Type) → (A → A → Bool) → A → List A → Bool;
elem _ _ _ nil ≔ false;
elem _ eq s (cons x xs) ≔ eq s x || elem _ eq s xs;
elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
elem _ _ nil ≔ false;
elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs;
foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
foldl _ _ f z nil ≔ z;
foldl _ _ f z (cons h hs) ≔ foldl _ _ f (f z h) hs;
foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
foldl f z nil ≔ z;
foldl f z (h ∷ hs) ≔ foldl f (f z h) hs;
--------------------------------------------------------------------------------
-- Pair
--------------------------------------------------------------------------------
inductive Pair (A : Type) (B : Type) {
mkPair : A → B → Pair A B;
infixr 4 ,;
infixr 2 ×;
inductive × (A : Type) (B : Type) {
, : A → B → A × B;
};
--------------------------------------------------------------------------------
@ -168,17 +168,17 @@ inductive Maybe (A : Type) {
};
from-int : Int → Maybe Int;
from-int i ≔ if _ (i < 0) (nothing _) (just _ i);
from-int i ≔ if (i < 0) nothing (just i);
maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B;
maybe _ _ b _ nothing ≔ b;
maybe _ _ _ f (just x) ≔ f x;
maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
maybe b _ nothing ≔ b;
maybe _ f (just x) ≔ f x;
from-string : String → Maybe String;
from-string s ≔ if _ (s ==String "") (nothing _) (just _ s);
from-string s ≔ if (s ==String "") nothing (just s);
pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool;
pair-from-optionString ≔ maybe _ _ (mkPair _ _ 0 false);
pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
pair-from-optionString ≔ maybe (0 , false);
--------------------------------------------------------------------------------
-- Anoma
@ -209,7 +209,7 @@ is-balance-key : String → String → Maybe String;
is-balance-key token key ≔ from-string (isBalanceKey token key);
unwrap-default : Maybe Int → Int;
unwrap-default o ≔ maybe _ _ 0 (id _) o;
unwrap-default ≔ maybe 0 id;
--------------------------------------------------------------------------------
-- Validity Predicate
@ -218,30 +218,30 @@ unwrap-default o ≔ maybe _ _ 0 (id _) o;
change-from-key : String → Int;
change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
check-vp : List String → String → Int → String → Pair Int Bool;
check-vp : List String → String → Int → String → Int × Bool;
check-vp verifiers key change owner ≔
if _
if
(change-from-key key < 0)
-- make sure the spender approved the transaction
(mkPair _ _ (change + (change-from-key key)) (elem _ (==String) owner verifiers))
(mkPair _ _ (change + (change-from-key key)) true);
(change + (change-from-key key), elem (==String) owner verifiers)
(change + (change-from-key key), true);
check-keys : String → List String → Pair Int Bool → String → Pair Int Bool;
check-keys token verifiers (mkPair change is-success) key ≔
if _
check-keys : String → List String → Int × Bool → String → Int × Bool;
check-keys token verifiers (change , is-success) key ≔
if
is-success
(pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
(mkPair _ _ 0 false);
(0 , false);
check-result : Pair Int Bool → Bool;
check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked;
check-result : Int × Bool → Bool;
check-result (change , all-checked) ≔ (change ==Int 0) && all-checked;
vp : String → List String → List String → Bool;
vp token keys-changed verifiers ≔
check-result
(foldl _ _
(foldl
(check-keys token verifiers)
(mkPair _ _ 0 true)
(0 , true)
keys-changed);
--------------------------------------------------------------------------------
@ -290,10 +290,10 @@ change2-key : String;
change2-key ≔ "change2-key";
verifiers : List String;
verifiers ≔ cons _ owner-address (nil _);
verifiers ≔ owner-address ∷ nil;
keys-changed : List String;
keys-changed ≔ cons _ change1-key (cons _ change2-key (nil _));
keys-changed ≔ change1-key ∷ change2-key ∷ nil;
main : Action;
main ≔

73
tests/positive/Implicit.mjuvix Normal file
View File

@ -0,0 +1,73 @@
module Implicit;
infixr 9 ∘;
∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
∘ f g x ≔ f (g x);
inductive Nat {
zero : Nat;
suc : Nat → Nat;
};
infixr 5 ∷;
inductive List (A : Type) {
nil : List A;
∷ : A → List A → List A;
};
upToTwo : _;
upToTwo ≔ zero ∷ suc zero ∷ suc (suc zero) ∷ nil;
infixr 4 ,;
inductive Pair (A : Type) (B : Type) {
, : A → B → Pair A B;
};
p1 : Nat → Nat → Pair Nat Nat;
p1 a b ≔ a , b ;
inductive Proxy (A : Type) {
proxy : Proxy A;
};
t2' : {A : Type} → Proxy A;
t2' ≔ proxy;
t2 : {A : Type} → Proxy A;
t2 ≔ proxy;
t3 : ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B;
t3 _ _ ≔ proxy;
t4 : {B : Type} → Proxy B;
t4 {_} ≔ t3 proxy proxy;
t4' : {B : Type} → Proxy B;
t4' ≔ t3 proxy proxy ;
map : {A : Type} → {B : Type} → (A → B) → List A → List B;
map f nil ≔ nil;
map f (x ∷ xs) ≔ f x ∷ map f xs;
t : {A : Type} → Proxy A;
t {_} ≔ proxy;
t' : {A : Type} → Proxy A;
t' ≔ proxy;
t5 : {A : Type} → Proxy A → Proxy A;
t5 p ≔ p;
t5' : {A : Type} → Proxy A → Proxy A;
t5' proxy ≔ proxy;
f : {A : Type} → {B : Type} → A → B → _;
f a b ≔ a;
pairEval : {A : Type} → {B : Type} → Pair (A → B) A → B;
pairEval (f , x) ≔ f x;
pairEval' : {A : Type} → {B : Type} → Pair ({C : Type} → A → B) A → B;
pairEval' {A} (f , x) ≔ f {Nat} x;
end;

4
tests/positive/MicroJuvix/HoleInSignature.mjuvix
View File

@ -9,9 +9,9 @@ inductive Bool {
};
p : Pair _ _;
p := mkPair _ _ true false;
p := mkPair true false;
p2 : (A : Type) → (B : Type) → _ → B → Pair A _;
p2 _ _ a b ≔ mkPair _ _ a b;
p2 _ _ a b ≔ mkPair a b;
end;

2
tests/positive/MiniC/MultiModules/Input.mjuvix
View File

@ -26,7 +26,7 @@ bool-to-str false ≔ "False";
fst-of-pair : Action;
fst-of-pair ≔ (put-str "fst (True, False) = ")
>> put-str-ln (bool-to-str (fst Bool Bool (mkPair Bool Bool true false)));
>> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false)));
main : Action;
main ≔ fst-of-pair;

2
tests/positive/MiniC/Polymorphism/Input.mjuvix
View File

@ -81,7 +81,7 @@ fst _ _ (mkPair a b) ≔ a;
fst-of-pair : Action;
fst-of-pair ≔ (put-str "fst (True, False) = ")
>> put-str-ln (bool-to-str (fst Bool Bool (mkPair Bool Bool true false)));
>> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false)));
main : Action;
main ≔ fst-of-pair;

6
tests/positive/MiniC/PolymorphismHoles/Input.mjuvix
View File

@ -72,8 +72,8 @@ inductive Pair (A : Type) (B : Type) {
mkPair : A → B → Pair A B;
};
fst : (A : Type) → (B : Type) → Pair A B → A;
fst _ _ (mkPair a b) ≔ a;
fst : {A : Type} → {B : Type} → Pair A B → A;
fst (mkPair a b) ≔ a;
--------------------------------------------------------------------------------
-- Main
@ -81,7 +81,7 @@ fst _ _ (mkPair a b) ≔ a;
fst-of-pair : Action;
fst-of-pair ≔ (put-str "fst (True, False) = ")
>> put-str-ln (bool-to-str (fst _ _ (mkPair _ _ true false)));
>> put-str-ln (bool-to-str (fst (mkPair true false)));
main : Action;
main ≔ fst-of-pair;

36
tests/positive/Polymorphism.mjuvix
View File

@ -32,24 +32,24 @@ add zero b ≔ b;
add (suc a) b ≔ suc (add a b);
nil' : (E : Type) → List E;
nil' A ≔ nil A;
nil' A ≔ nil;
-- currying
nil'' : (E : Type) → List E;
nil'' ≔ nil;
nil'' E ≔ nil;
fst : (A : Type) → (B : Type) → Pair A B → A;
fst _ _ (mkPair a b) ≔ a;
p : Pair Bool Bool;
p ≔ mkPair Bool Bool true false;
p ≔ mkPair true false;
swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
swap A B (mkPair a b) ≔ mkPair B A b a;
swap A B (mkPair a b) ≔ mkPair b a;
curry : (A : Type) → (B : Type) → (C : Type)
→ (Pair A B → C) → A → B → C;
curry A B C f a b ≔ f (mkPair A B a b) ;
curry A B C f a b ≔ f (mkPair a b) ;
ap : (A : Type) → (B : Type)
→ (A → B) → A → B;
@ -64,42 +64,42 @@ headDef _ d nil ≔ d;
headDef A _ (cons h _) ≔ h;
filter : (A : Type) → (A → Bool) → List A → List A;
filter A f nil ≔ nil A;
filter A f (cons x xs) ≔ ite (List A) (f x) (cons A x (filter A f xs)) (filter A f xs);
filter A f nil ≔ nil;
filter A f (cons x xs) ≔ ite (List A) (f x) (cons x (filter A f xs)) (filter A f xs);
map : (A : Type) → (B : Type) →
(A → B) → List A → List B;
map A B f nil ≔ nil B ;
map A B f (cons x xs) ≔ cons B (f x) (map A B f xs);
map A B f nil ≔ nil ;
map A B f (cons x xs) ≔ cons (f x) (map A B f xs);
zip : (A : Type) → (B : Type)
→ List A → List B → List (Pair A B);
zip A B nil _ ≔ nil (Pair A B);
zip A B _ nil ≔ nil (Pair A B);
zip A B (cons a as) (cons b bs) ≔ nil (Pair A B);
zip A B nil _ ≔ nil;
zip A B _ nil ≔ nil;
zip A B (cons a as) (cons b bs) ≔ nil;
zipWith : (A : Type) → (B : Type) → (C : Type)
→ (A → B → C)
→ List A → List B → List C;
zipWith A B C f nil _ ≔ nil C;
zipWith A B C f _ nil ≔ nil C;
zipWith A B C f (cons a as) (cons b bs) ≔ cons C (f a b) (zipWith A B C f as bs);
zipWith A B C f nil _ ≔ nil;
zipWith A B C f _ nil ≔ nil;
zipWith A B C f (cons a as) (cons b bs) ≔ cons (f a b) (zipWith A B C f as bs);
rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
rankn f b n ≔ mkPair Bool Nat (f Bool b) (f Nat n);
rankn f b n ≔ mkPair (f Bool b) (f Nat n);
-- currying
trankn : Pair Bool Nat;
trankn ≔ rankn id false zero;
l1 : List Nat;
l1 ≔ cons Nat zero (nil Nat);
l1 ≔ cons zero nil;
pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
pairEval _ _ (mkPair f x) ≔ f x;
main : Nat;
main ≔ headDef Nat (pairEval Nat Nat (mkPair (Nat → Nat) Nat (add zero) zero))
main ≔ headDef Nat (pairEval Nat Nat (mkPair (add zero) zero))
(zipWith Nat Nat Nat add l1 l1);
end;

39
tests/positive/PolymorphismHoles.mjuvix
View File

@ -31,25 +31,18 @@ add : Nat → Nat → Nat;
add zero b ≔ b;
add (suc a) b ≔ suc (add a b);
nil' : (E : Type) → List E;
nil' A ≔ nil _;
-- currying
nil'' : (E : Type) → List E;
nil'' ≔ nil;
fst : (A : Type) → (B : Type) → Pair A B → A;
fst _ _ (mkPair a b) ≔ a;
p : Pair Bool Bool;
p ≔ mkPair _ _ true false;
p ≔ mkPair true false;
swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
swap A B (mkPair a b) ≔ mkPair _ _ b a;
swap A B (mkPair a b) ≔ mkPair b a;
curry : (A : Type) → (B : Type) → (C : Type)
→ (Pair A B → C) → A → B → C;
curry A B C f a b ≔ f (mkPair _ _ a b) ;
curry A B C f a b ≔ f (mkPair a b) ;
ap : (A : Type) → (B : Type)
→ (A → B) → A → B;
@ -64,42 +57,42 @@ ite _ true tt _ ≔ tt;
ite _ false _ ff ≔ ff;
filter : (A : Type) → (A → Bool) → List A → List A;
filter _ f nil ≔ nil _;
filter _ f (cons x xs) ≔ ite _ (f x) (cons _ x (filter _ f xs)) (filter _ f xs);
filter _ f nil ≔ nil;
filter _ f (cons x xs) ≔ ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs);
map : (A : Type) → (B : Type) →
(A → B) → List _ → List _;
map _ _ f nil ≔ nil _;
map _ _ f (cons x xs) ≔ cons _ (f x) (map _ _ f xs);
map _ _ f nil ≔ nil;
map _ _ f (cons x xs) ≔ cons (f x) (map _ _ f xs);
zip : (A : Type) → (B : Type)
→ List A → List B → List (Pair A B);
zip A _ nil _ ≔ nil _;
zip _ _ _ nil ≔ nil _;
zip _ _ (cons a as) (cons b bs) ≔ nil _;
zip A _ nil _ ≔ nil;
zip _ _ _ nil ≔ nil;
zip _ _ (cons a as) (cons b bs) ≔ nil;
zipWith : (A : Type) → (B : Type) → (C : Type)
→ (A → B → C)
→ List A → List B → List C;
zipWith _ _ C f nil _ ≔ nil C;
zipWith _ _ C f _ nil ≔ nil C;
zipWith _ _ _ f (cons a as) (cons b bs) ≔ cons _ (f a b) (zipWith _ _ _ f as bs);
zipWith _ _ C f nil _ ≔ nil;
zipWith _ _ C f _ nil ≔ nil;
zipWith _ _ _ f (cons a as) (cons b bs) ≔ cons (f a b) (zipWith _ _ _ f as bs);
rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
rankn f b n ≔ mkPair _ _ (f _ b) (f _ n);
rankn f b n ≔ mkPair (f _ b) (f _ n);
-- currying
trankn : Pair Bool Nat;
trankn ≔ rankn id false zero;
l1 : List Nat;
l1 ≔ cons _ zero (nil _);
l1 ≔ cons zero nil;
pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
pairEval _ _ (mkPair f x) ≔ f x;
main : Nat;
main ≔ headDef _ (pairEval _ _ (mkPair _ _ (add zero) zero))
main ≔ headDef _ (pairEval _ _ (mkPair (add zero) zero))
(zipWith _ _ _ add l1 l1);
end;