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

Remove old function syntax (#2305)

Browse Source 
* Enables new function syntax in local let-declarations
* Closes #2251
This commit is contained in:
Łukasz Czajka 2023-08-24 11:20:09 +02:00 committed by Jan Mas Rovira
parent 56871a204c
commit 2baad15a41
229 changed files with 2233 additions and 2975 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -116,7 +116,7 @@ JUVIXFILESTOFORMAT=$(shell find \
-type d \( -name ".juvix-build" -o -name "FancyPaths" \) -prune -o \
-type f -name "*.juvix" -print)
JUVIXFORMATFLAGS?=--in-place --new-function-syntax
JUVIXFORMATFLAGS?=--in-place
JUVIXTYPECHECKFLAGS?=--only-errors
.PHONY: format-juvix-files

3
app/Commands/Format.hs
View File

@ -49,9 +49,8 @@ targetFromOptions opts = do
runCommand :: forall r. Members '[Embed IO, App, Resource, Files] r => FormatOptions -> Sem r ()
runCommand opts = do
target <- targetFromOptions opts
let newSyntax = NewSyntax (opts ^. formatNewSyntax)
runOutputSem (renderFormattedOutput target opts) $ runScopeFileApp $ do
res <- runReader newSyntax $ case target of
res <- case target of
TargetFile p -> format p
TargetProject p -> formatProject p
TargetStdin -> formatStdin

6
app/Commands/Format/Options.hs
View File

@ -5,7 +5,6 @@ import CommonOptions
data FormatOptions = FormatOptions
{ _formatInput :: Maybe (Prepath FileOrDir),
_formatCheck :: Bool,
_formatNewSyntax :: Bool,
_formatInPlace :: Bool
}
deriving stock (Data)
@ -29,11 +28,6 @@ parseFormat = do
( long "check"
<> help "Do not print reformatted sources or unformatted file paths to standard output."
)
_formatNewSyntax <-
switch
( long "new-function-syntax"
<> help "Format the file using the new function syntax."
)
_formatInPlace <-
switch
( long "in-place"

3
examples/milestone/Bank/Bank.juvix
View File

@ -83,8 +83,7 @@ calculateInterest : Nat -> Nat -> Nat -> Nat
| principal rate periods :=
let
amount : Nat := principal;
incrAmount : Nat -> Nat;
incrAmount a := div (a * rate) 10000;
incrAmount (a : Nat) : Nat := div (a * rate) 10000;
in iterate (min 100 periods) incrAmount amount;
--- Asserts some ;Bool; condition.

11
examples/milestone/Collatz/Collatz.juvix
View File

@ -3,8 +3,8 @@ module Collatz;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
collatzNext : Nat → Nat
| n := if (mod n 2 == 0) (div n 2) (3 * n + 1);
collatzNext (n : Nat) : Nat :=
if (mod n 2 == 0) (div n 2) (3 * n + 1);
collatz : Nat → Nat
| zero := zero
@ -12,10 +12,9 @@ collatz : Nat → Nat
| n := collatzNext n;
terminating
run : (Nat → Nat) → Nat → IO
| _ (suc zero) :=
printNatLn 1 >> printStringLn "Finished!"
| f n := printNatLn n >> run f (f n);
run (f : Nat → Nat) : Nat → IO
| (suc zero) := printNatLn 1 >> printStringLn "Finished!"
| n := printNatLn n >> run f (f n);
welcome : String :=
"Collatz calculator\n------------------\n\nType a number then ENTER";

3
examples/milestone/Fibonacci/Fibonacci.juvix
View File

@ -6,7 +6,6 @@ fib : Nat → Nat → Nat → Nat
| zero x1 _ := x1
| (suc n) x1 x2 := fib n x2 (x1 + x2);
fibonacci : Nat → Nat
| n := fib n 0 1;
fibonacci (n : Nat) : Nat := fib n 0 1;
main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);

29
examples/milestone/PascalsTriangle/PascalsTriangle.juvix
View File

@ -7,13 +7,12 @@ module PascalsTriangle;
import Stdlib.Prelude open;
--- Return a list of repeated applications of a given function
scanIterate : {A : Type} → Nat → (A → A) → A → List A
scanIterate {A} : Nat → (A → A) → A → List A
| zero _ _ := nil
| (suc n) f a := a :: scanIterate n f (f a);
--- Produce a singleton List
singleton : {A : Type} → A → List A
| a := a :: nil;
singleton {A} (a : A) : List A := a :: nil;
--- Concatenates a list of strings
--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
@ -21,24 +20,22 @@ singleton : {A : Type} → A → List A
:: nil;
concat : List String → String := foldl (++str) "";
intercalate : String → List String → String
| sep xs := concat (intersperse sep xs);
intercalate (sep : String) (xs : List String) : String :=
concat (intersperse sep xs);
showList : List Nat → String
| xs :=
"[" ++str intercalate "," (map natToString xs) ++str "]";
showList (xs : List Nat) : String :=
"[" ++str intercalate "," (map natToString xs) ++str "]";
--- Compute the next row of Pascal's triangle
pascalNextRow : List Nat → List Nat
| row :=
zipWith
(+)
(singleton zero ++ row)
(row ++ singleton zero);
pascalNextRow (row : List Nat) : List Nat :=
zipWith
(+)
(singleton zero ++ row)
(row ++ singleton zero);
--- Produce Pascal's triangle to a given depth
pascal : Nat → List (List Nat)
| rows := scanIterate rows pascalNextRow (singleton 1);
pascal (rows : Nat) : List (List Nat) :=
scanIterate rows pascalNextRow (singleton 1);
main : IO :=
printStringLn (unlines (map showList (pascal 10)));

17
examples/milestone/TicTacToe/CLI/TicTacToe.juvix
View File

@ -10,16 +10,15 @@ import Stdlib.Prelude open;
import Logic.Game open;
--- A ;String; that prompts the user for their input
prompt : GameState → String
| x :=
"\n"
++str showGameState x
++str "\nPlayer "
++str showSymbol (player x)
++str ": ";
prompt (x : GameState) : String :=
"\n"
++str showGameState x
++str "\nPlayer "
++str showSymbol (player x)
++str ": ";
nextMove : GameState → String → GameState
| s := flip playMove s ∘ validMove ∘ stringToNat;
nextMove (s : GameState) : String → GameState :=
flip playMove s ∘ validMove ∘ stringToNat;
--- Main loop
terminating

4
examples/milestone/TicTacToe/Logic/Board.juvix
View File

@ -35,8 +35,8 @@ columns : List (List Square) → List (List Square) :=
rows : List (List Square) → List (List Square) := id;
--- Textual representation of a ;List Square;
showRow : List Square → String
| xs := concat (surround "|" (map showSquare xs));
showRow (xs : List Square) : String :=
concat (surround "|" (map showSquare xs));
showBoard : Board → String
| (board squares) :=

8
examples/milestone/TicTacToe/Logic/Extra.juvix
View File

@ -11,9 +11,9 @@ import Stdlib.Prelude open;
concat : List String → String := foldl (++str) "";
--- It inserts the first ;String; at the beginning, in between, and at the end of the second list
surround : String → List String → List String
| x xs := (x :: intersperse x xs) ++ x :: nil;
surround (x : String) (xs : List String) : List String :=
(x :: intersperse x xs) ++ x :: nil;
--- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result
intercalate : String → List String → String
| sep xs := concat (intersperse sep xs);
intercalate (sep : String) (xs : List String) : String :=
concat (intersperse sep xs);

4
examples/milestone/TicTacToe/Logic/Game.juvix
View File

@ -43,5 +43,5 @@ playMove : Maybe Nat → GameState → GameState
noError));
--- Returns ;just; if the given ;Nat; is in range of 1..9
validMove : Nat → Maybe Nat
| n := if (n <= 9 && n >= 1) (just n) nothing;
validMove (n : Nat) : Maybe Nat :=
if (n <= 9 && n >= 1) (just n) nothing;

6
examples/milestone/TicTacToe/Logic/Square.juvix
View File

@ -23,10 +23,10 @@ showSquare : Square → String
| (empty n) := " " ++str natToString n ++str " "
| (occupied s) := " " ++str showSymbol s ++str " ";
replace : Symbol → Nat → Square → Square
| player k (empty n) :=
replace (player : Symbol) (k : Nat) : Square → Square
| (empty n) :=
if
(n Stdlib.Data.Nat.Ord.== k)
(occupied player)
(empty n)
| _ _ s := s;
| s := s;

2
juvix-stdlib

@ -1 +1 @@
Subproject commit abe514cb45def5b512e08b85f22959c33e2238ac
Subproject commit b7edcc335feee4e3db87b5aca46381e2d9644ab0

15
src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
View File

@ -397,7 +397,6 @@ goJudoc (Judoc bs) = mconcatMapM goGroup bs
goStatement :: (Members '[Reader HtmlOptions, Reader NormalizedTable] r) => Statement 'Scoped -> Sem r Html
goStatement = \case
StatementTypeSignature t -> goTypeSignature t
StatementAxiom t -> goAxiom t
StatementInductive t -> goInductive t
StatementOpenModule t -> goOpen t
@ -483,20 +482,6 @@ defHeader tmp uid sig mjudoc = do
sourceLink' <- sourceAndSelfLink tmp uid
return $ noDefHeader (sig <> sourceLink')
goTypeSignature :: forall r. (Members '[Reader HtmlOptions, Reader NormalizedTable] r) => TypeSignature 'Scoped -> Sem r Html
goTypeSignature sig = do
sig' <- typeSig
defHeader tmp uid sig' (sig ^. sigDoc)
where
tmp :: TopModulePath
tmp = sig ^. sigName . S.nameDefinedIn . S.absTopModulePath
uid :: NameId
uid = sig ^. sigName . S.nameId
typeSig :: Sem r Html
typeSig = ppCodeHtml opts (set sigDoc Nothing sig)
opts :: Options
opts = set optPrintPragmas False defaultOptions
sourceAndSelfLink :: (Members '[Reader HtmlOptions] r) => TopModulePath -> NameId -> Sem r Html
sourceAndSelfLink tmp name = do
ref' <- local (set htmlOptionsKind HtmlSrc) (nameIdAttrRef tmp (Just name))

28
src/Juvix/Compiler/Concrete/Data/InfoTable.hs
View File

@ -4,15 +4,7 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Language
import Juvix.Prelude
data OldFunctionInfo = OldFunctionInfo
{ _oldFunctionInfoType :: TypeSignature 'Scoped,
_oldFunctionInfoClauses :: [FunctionClause 'Scoped]
}
deriving stock (Eq, Show)
data FunctionInfo
= FunctionInfoOld OldFunctionInfo
| FunctionInfoNew (FunctionDef 'Scoped)
newtype FunctionInfo = FunctionInfo (FunctionDef 'Scoped)
deriving stock (Eq, Show)
data ConstructorInfo = ConstructorInfo
@ -61,25 +53,13 @@ makeLenses ''InfoTable
makeLenses ''InductiveInfo
makeLenses ''ConstructorInfo
makeLenses ''AxiomInfo
makeLenses ''OldFunctionInfo
_FunctionInfoOld :: Traversal' FunctionInfo OldFunctionInfo
_FunctionInfoOld f = \case
FunctionInfoOld x -> FunctionInfoOld <$> f x
r@FunctionInfoNew {} -> pure r
functionInfoDoc :: Lens' FunctionInfo (Maybe (Judoc 'Scoped))
functionInfoDoc f = \case
FunctionInfoOld i -> do
i' <- traverseOf (oldFunctionInfoType . sigDoc) f i
pure (FunctionInfoOld i')
FunctionInfoNew i -> do
FunctionInfo i -> do
i' <- traverseOf signDoc f i
pure (FunctionInfoNew i')
pure (FunctionInfo i')
instance HasLoc FunctionInfo where
getLoc = \case
FunctionInfoOld f ->
getLoc (f ^. oldFunctionInfoType)
<>? (getLocSpan <$> nonEmpty (f ^. oldFunctionInfoClauses))
FunctionInfoNew f -> getLoc f
FunctionInfo f -> getLoc f

20
src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
View File

@ -14,9 +14,7 @@ data InfoTableBuilder m a where
RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m ()
RegisterConstructor :: S.Symbol -> ConstructorDef 'Scoped -> InfoTableBuilder m ()
RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m ()
RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()
RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
RegisterName :: HasLoc c => S.Name' c -> InfoTableBuilder m ()
RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m ()
RegisterFixity :: FixityDef -> InfoTableBuilder m ()
@ -54,27 +52,11 @@ toState = reinterpret $ \case
registerDoc (ity ^. inductiveName . nameId) j
RegisterFunctionDef f ->
let ref = f ^. signName . S.nameId
info = FunctionInfoNew f
info = FunctionInfo f
j = f ^. signDoc
in do
modify (set (infoFunctions . at ref) (Just info))
registerDoc (f ^. signName . nameId) j
RegisterTypeSignature f ->
let ref = f ^. sigName . S.nameId
info =
FunctionInfoOld
OldFunctionInfo
{ _oldFunctionInfoType = f,
_oldFunctionInfoClauses = []
}
j = f ^. sigDoc
in do
modify (set (infoFunctions . at ref) (Just info))
registerDoc (f ^. sigName . nameId) j
RegisterFunctionClause c ->
-- assumes the signature has already been registered
let key = c ^. clauseOwnerFunction . S.nameId
in modify (over (infoFunctions . at key . _Just . _FunctionInfoOld . oldFunctionInfoClauses) (`snoc` c))
RegisterName n -> modify (over highlightNames (cons (S.AName n)))
RegisterModule m -> do
let j = m ^. moduleDoc

65
src/Juvix/Compiler/Concrete/Extra.hs
View File

@ -6,7 +6,6 @@ module Juvix.Compiler.Concrete.Extra
unfoldApplication,
groupStatements,
flattenStatement,
migrateFunctionSyntax,
recordNameSignatureByIndex,
getExpressionAtomIden,
getPatternAtomIden,
@ -18,7 +17,6 @@ import Data.IntMap.Strict qualified as IntMap
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Concrete.Data.NameSignature.Base
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Keywords
import Juvix.Compiler.Concrete.Language
import Juvix.Prelude hiding (some)
import Juvix.Prelude.Parsing
@ -108,23 +106,13 @@ groupStatements = \case
(StatementAxiom {}, _) -> False
(StatementFunctionDef {}, _) -> False
(_, StatementFunctionDef {}) -> False
(StatementTypeSignature sig, StatementFunctionClause fun) ->
case sing :: SStage s of
SParsed -> sig ^. sigName == fun ^. clauseOwnerFunction
SScoped -> sig ^. sigName == fun ^. clauseOwnerFunction
(StatementTypeSignature {}, _) -> False
(StatementFunctionClause fun1, StatementFunctionClause fun2) ->
case sing :: SStage s of
SParsed -> fun1 ^. clauseOwnerFunction == fun2 ^. clauseOwnerFunction
SScoped -> fun1 ^. clauseOwnerFunction == fun2 ^. clauseOwnerFunction
(StatementFunctionClause {}, _) -> False
(StatementProjectionDef {}, StatementProjectionDef {}) -> True
(StatementProjectionDef {}, _) -> False
definesSymbol :: Symbol -> Statement s -> Bool
definesSymbol n s = case s of
StatementTypeSignature sig -> n == symbolParsed (sig ^. sigName)
StatementInductive d -> n `elem` syms d
StatementAxiom d -> n == symbolParsed (d ^. axiomName)
StatementFunctionDef d -> n == symbolParsed (d ^. signName)
_ -> False
where
symbolParsed :: SymbolType s -> Symbol
@ -147,57 +135,6 @@ flattenStatement = \case
StatementModule m -> concatMap flattenStatement (m ^. moduleBody)
s -> [s]
migrateFunctionSyntax :: Module 'Scoped t -> Module 'Scoped t
migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m
where
goStatement :: Statement 'Scoped -> Maybe (Statement 'Scoped)
goStatement s = case s of
StatementSyntax {} -> Just s
StatementImport {} -> Just s
StatementAxiom {} -> Just s
StatementModule l -> Just (StatementModule (migrateFunctionSyntax l))
StatementInductive {} -> Just s
StatementOpenModule {} -> Just s
StatementFunctionDef {} -> Just s
StatementFunctionClause {} -> Nothing
StatementProjectionDef {} -> Just s
StatementTypeSignature sig -> Just (StatementFunctionDef (mkFunctionDef sig (getClauses (sig ^. sigName))))
ss' :: [Statement 'Scoped]
ss' = m ^. moduleBody
mkFunctionDef :: TypeSignature 'Scoped -> [FunctionClause 'Scoped] -> FunctionDef 'Scoped
mkFunctionDef sig cls =
FunctionDef
{ _signName = sig ^. sigName,
_signColonKw = sig ^. sigColonKw,
_signRetType = sig ^. sigType,
_signDoc = sig ^. sigDoc,
_signPragmas = sig ^. sigPragmas,
_signTerminating = sig ^. sigTerminating,
_signBuiltin = sig ^. sigBuiltin,
_signArgs = [],
_signBody = case sig ^. sigBody of
Just e -> SigBodyExpression e
Nothing -> case cls of
[] -> impossible
[c]
| null (c ^. clausePatterns) -> SigBodyExpression (c ^. clauseBody)
| otherwise -> SigBodyClauses (pure (mkClause c))
c : cs -> SigBodyClauses (mkClause <$> c :| cs)
}
where
mkClause :: FunctionClause 'Scoped -> NewFunctionClause 'Scoped
mkClause c =
NewFunctionClause
{ _clausenPipeKw = Irrelevant (KeywordRef kwPipe (getLoc (c ^. clauseOwnerFunction)) Ascii),
_clausenAssignKw = c ^. clauseAssignKw,
_clausenBody = c ^. clauseBody,
_clausenPatterns = nonEmpty' (c ^. clausePatterns)
}
getClauses :: S.Symbol -> [FunctionClause 'Scoped]
getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
recordNameSignatureByIndex :: RecordNameSignature -> IntMap Symbol
recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to swap)

82
src/Juvix/Compiler/Concrete/Language.hs
View File

@ -185,24 +185,20 @@ data Definition (s :: Stage)
| DefinitionFunctionDef (FunctionDef s)
| DefinitionInductive (InductiveDef s)
| DefinitionAxiom (AxiomDef s)
| DefinitionTypeSignature (TypeSignature s)
| DefinitionProjectionDef (ProjectionDef s)
data NonDefinition (s :: Stage)
= NonDefinitionImport (Import s)
| NonDefinitionModule (Module s 'ModuleLocal)
| NonDefinitionFunctionClause (FunctionClause s)
| NonDefinitionOpenModule (OpenModule s)
data Statement (s :: Stage)
= StatementSyntax (SyntaxDef s)
| StatementTypeSignature (TypeSignature s)
| StatementFunctionDef (FunctionDef s)
| StatementImport (Import s)
| StatementInductive (InductiveDef s)
| StatementModule (Module s 'ModuleLocal)
| StatementOpenModule (OpenModule s)
| StatementFunctionClause (FunctionClause s)
| StatementAxiom (AxiomDef s)
| StatementProjectionDef (ProjectionDef s)
@ -426,30 +422,6 @@ deriving stock instance Ord (FunctionDef 'Parsed)
deriving stock instance Ord (FunctionDef 'Scoped)
data TypeSignature (s :: Stage) = TypeSignature
{ _sigName :: FunctionName s,
_sigColonKw :: Irrelevant KeywordRef,
_sigType :: ExpressionType s,
_sigDoc :: Maybe (Judoc s),
_sigAssignKw :: Irrelevant (Maybe KeywordRef),
_sigPragmas :: Maybe ParsedPragmas,
_sigBuiltin :: Maybe (WithLoc BuiltinFunction),
_sigBody :: Maybe (ExpressionType s),
_sigTerminating :: Maybe KeywordRef
}
deriving stock instance Show (TypeSignature 'Parsed)
deriving stock instance Show (TypeSignature 'Scoped)
deriving stock instance Eq (TypeSignature 'Parsed)
deriving stock instance Eq (TypeSignature 'Scoped)
deriving stock instance Ord (TypeSignature 'Parsed)
deriving stock instance Ord (TypeSignature 'Scoped)
data AxiomDef (s :: Stage) = AxiomDef
{ _axiomKw :: Irrelevant KeywordRef,
_axiomDoc :: Maybe (Judoc s),
@ -861,25 +833,6 @@ deriving stock instance Ord (PatternAtoms 'Scoped)
type FunctionName s = SymbolType s
data FunctionClause (s :: Stage) = FunctionClause
{ _clauseOwnerFunction :: FunctionName s,
_clauseAssignKw :: Irrelevant KeywordRef,
_clausePatterns :: [PatternAtomType s],
_clauseBody :: ExpressionType s
}
deriving stock instance Show (FunctionClause 'Parsed)
deriving stock instance Show (FunctionClause 'Scoped)
deriving stock instance Eq (FunctionClause 'Parsed)
deriving stock instance Eq (FunctionClause 'Scoped)
deriving stock instance Ord (FunctionClause 'Parsed)
deriving stock instance Ord (FunctionClause 'Scoped)
type LocalModuleName s = SymbolType s
data Module (s :: Stage) (t :: ModuleIsTop) = Module
@ -1263,7 +1216,7 @@ instance HasFixity PostfixApplication where
data Let (s :: Stage) = Let
{ _letKw :: KeywordRef,
_letInKw :: Irrelevant KeywordRef,
_letClauses :: NonEmpty (LetClause s),
_letFunDefs :: NonEmpty (FunctionDef s),
_letExpression :: ExpressionType s
}
@ -1279,22 +1232,6 @@ deriving stock instance Ord (Let 'Parsed)
deriving stock instance Ord (Let 'Scoped)
data LetClause (s :: Stage)
= LetTypeSig (TypeSignature s)
| LetFunClause (FunctionClause s)
deriving stock instance Show (LetClause 'Parsed)
deriving stock instance Show (LetClause 'Scoped)
deriving stock instance Eq (LetClause 'Parsed)
deriving stock instance Eq (LetClause 'Scoped)
deriving stock instance Ord (LetClause 'Parsed)
deriving stock instance Ord (LetClause 'Scoped)
data CaseBranch (s :: Stage) = CaseBranch
{ _caseBranchPipe :: Irrelevant KeywordRef,
_caseBranchAssignKw :: Irrelevant KeywordRef,
@ -1721,13 +1658,11 @@ makeLenses ''OperatorSyntaxDef
makeLenses ''IteratorSyntaxDef
makeLenses ''ConstructorDef
makeLenses ''Module
makeLenses ''TypeSignature
makeLenses ''SigArg
makeLenses ''SigArgRhs
makeLenses ''FunctionDef
makeLenses ''AxiomDef
makeLenses ''ExportInfo
makeLenses ''FunctionClause
makeLenses ''InductiveParameters
makeLenses ''InductiveParametersRhs
makeLenses ''ModuleRef'
@ -1825,9 +1760,6 @@ instance SingI s => HasLoc (InductiveParameters s) where
instance HasLoc (InductiveDef s) where
getLoc i = (getLoc <$> i ^. inductivePositive) ?<> getLoc (i ^. inductiveKw)
instance SingI s => HasLoc (FunctionClause s) where
getLoc c = getLocSymbolType (c ^. clauseOwnerFunction) <> getLocExpressionType (c ^. clauseBody)
instance HasLoc ModuleRef where
getLoc (ModuleRef' (_ :&: r)) = getLoc r
@ -1847,13 +1779,11 @@ instance HasLoc (Statement 'Scoped) where
getLoc :: Statement 'Scoped -> Interval
getLoc = \case
StatementSyntax t -> getLoc t
StatementTypeSignature t -> getLoc t
StatementFunctionDef t -> getLoc t
StatementImport t -> getLoc t
StatementInductive t -> getLoc t
StatementModule t -> getLoc t
StatementOpenModule t -> getLoc t
StatementFunctionClause t -> getLoc t
StatementAxiom t -> getLoc t
StatementProjectionDef t -> getLoc t
@ -1995,16 +1925,6 @@ instance SingI s => HasLoc (FunctionDef s) where
?<> getLocSymbolType _signName
<> getLoc _signBody
instance SingI s => HasLoc (TypeSignature s) where
getLoc TypeSignature {..} =
(getLoc <$> _sigDoc)
?<> (getLoc <$> _sigPragmas)
?<> (getLoc <$> _sigBuiltin)
?<> (getLoc <$> _sigTerminating)
?<> getLocSymbolType _sigName
<> (getLocExpressionType <$> _sigBody)
?<> getLocExpressionType _sigType
instance HasLoc (Example s) where
getLoc e = e ^. exampleLoc

56
src/Juvix/Compiler/Concrete/Print/Base.hs
View File

@ -234,11 +234,7 @@ instance PrettyPrint S.AName where
instance PrettyPrint FunctionInfo where
ppCode = \case
FunctionInfoOld f -> do
let ty = StatementTypeSignature (f ^. oldFunctionInfoType)
cs = map StatementFunctionClause (f ^. oldFunctionInfoClauses)
ppStatements (ty : cs)
FunctionInfoNew f -> ppCode f
FunctionInfo f -> ppCode f
instance SingI s => PrettyPrint (List s) where
ppCode List {..} = do
@ -448,9 +444,9 @@ instance SingI s => PrettyPrint (LambdaClause s) where
instance SingI s => PrettyPrint (Let s) where
ppCode Let {..} = do
let letClauses' = blockIndent (ppBlock _letClauses)
let letFunDefs' = blockIndent (ppBlock _letFunDefs)
letExpression' = ppExpressionType _letExpression
ppCode _letKw <> letClauses' <> ppCode _letInKw <+> letExpression'
ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'
instance SingI s => PrettyPrint (Case s) where
ppCode Case {..} = do
@ -555,11 +551,6 @@ instance SingI s => PrettyPrint (CaseBranch s) where
e' = ppExpressionType _caseBranchExpression
ppCode _caseBranchPipe <+> pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e'
instance SingI s => PrettyPrint (LetClause s) where
ppCode c = case c of
LetTypeSig sig -> ppCode sig
LetFunClause cl -> ppCode cl
ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
ppBlock items = vsep (sepEndSemicolon (fmap ppCode items))
@ -795,30 +786,6 @@ instance SingI s => PrettyPrint (FunctionDef s) where
<> body'
)
instance SingI s => PrettyPrint (TypeSignature s) where
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => TypeSignature s -> Sem r ()
ppCode TypeSignature {..} = do
let termin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _sigTerminating
doc' :: Maybe (Sem r ()) = ppCode <$> _sigDoc
pragmas' :: Maybe (Sem r ()) = ppCode <$> _sigPragmas
builtin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _sigBuiltin
type' = ppExpressionType _sigType
name' = annDef _sigName (ppSymbolType _sigName)
body' = case _sigBody of
Nothing -> Nothing
Just body -> Just (ppCode (fromJust <$> _sigAssignKw) <> oneLineOrNext (ppExpressionType body))
doc'
?<> pragmas'
?<> builtin'
?<> termin'
?<> ( name'
<+> ppCode _sigColonKw
<> oneLineOrNext
( type'
<+?> body'
)
)
instance PrettyPrint Wildcard where
ppCode w = morpheme (getLoc w) C.kwWildcard
@ -940,21 +907,6 @@ instance SingI s => PrettyPrint (OpenModule s) where
<+?> usingHiding'
<+?> public'
instance SingI s => PrettyPrint (FunctionClause s) where
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => FunctionClause s -> Sem r ()
ppCode FunctionClause {..} = do
let clauseFun' = ppSymbolType _clauseOwnerFunction
clausePatterns' = case nonEmpty _clausePatterns of
Nothing -> Nothing
Just ne -> Just (hsep (ppPatternAtom <$> ne))
clauseBody' = ppExpressionType _clauseBody
nest
( clauseFun'
<+?> clausePatterns'
)
<+> ppCode _clauseAssignKw
<> oneLineOrNext clauseBody'
ppCodeAtom :: (HasAtomicity c, PrettyPrint c) => PrettyPrinting c
ppCodeAtom c = do
let p' = ppCode c
@ -1090,13 +1042,11 @@ instance SingI s => PrettyPrint (ProjectionDef s) where
instance SingI s => PrettyPrint (Statement s) where
ppCode = \case
StatementSyntax s -> ppCode s
StatementTypeSignature s -> ppCode s
StatementFunctionDef f -> ppCode f
StatementImport i -> ppCode i
StatementInductive i -> ppCode i
StatementModule m -> ppCode m
StatementOpenModule o -> ppCode o
StatementFunctionClause c -> ppCode c
StatementAxiom a -> ppCode a
StatementProjectionDef a -> ppCode a

91
src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
View File

@ -778,24 +778,6 @@ checkFunctionDef FunctionDef {..} = do
_clausenAssignKw
}
checkTypeSignature ::
Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax, Reader BindingStrategy] r =>
TypeSignature 'Parsed ->
Sem r (TypeSignature 'Scoped)
checkTypeSignature TypeSignature {..} = do
sigType' <- checkParseExpressionAtoms _sigType
sigName' <- bindFunctionSymbol _sigName
sigDoc' <- mapM checkJudoc _sigDoc
sigBody' <- mapM checkParseExpressionAtoms _sigBody
registerTypeSignature
@$> TypeSignature
{ _sigName = sigName',
_sigType = sigType',
_sigDoc = sigDoc',
_sigBody = sigBody',
..
}
checkInductiveParameters ::
forall r.
Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
@ -1051,7 +1033,6 @@ checkModuleBody body = do
toStatement = \case
NonDefinitionImport d -> StatementImport d
NonDefinitionModule d -> StatementModule d
NonDefinitionFunctionClause d -> StatementFunctionClause d
NonDefinitionOpenModule d -> StatementOpenModule d
goDefinitions :: forall t. Members '[Output (Statement s)] t => DefinitionsSection s -> Sem t ()
@ -1065,7 +1046,6 @@ checkModuleBody body = do
DefinitionAxiom d -> StatementAxiom d
DefinitionFunctionDef d -> StatementFunctionDef d
DefinitionInductive d -> StatementInductive d
DefinitionTypeSignature d -> StatementTypeSignature d
DefinitionProjectionDef d -> StatementProjectionDef d
checkSections ::
@ -1115,7 +1095,6 @@ checkSections sec = do
goNonDefinition = \case
NonDefinitionModule m -> NonDefinitionModule <$> checkLocalModule m
NonDefinitionImport i -> NonDefinitionImport <$> checkImport i
NonDefinitionFunctionClause i -> NonDefinitionFunctionClause <$> checkFunctionClause i
NonDefinitionOpenModule i -> NonDefinitionOpenModule <$> checkOpenModule i
goDefinitions :: DefinitionsSection 'Parsed -> Sem r' (DefinitionsSection 'Scoped)
@ -1133,7 +1112,6 @@ checkSections sec = do
reserveDefinition = \case
DefinitionSyntax s -> resolveSyntaxDef s
DefinitionFunctionDef d -> void (reserveFunctionSymbol d)
DefinitionTypeSignature d -> void (reserveSymbolOf SKNameFunction Nothing (d ^. sigName))
DefinitionAxiom d -> void (reserveAxiomSymbol d)
DefinitionProjectionDef d -> void (reserveProjectionSymbol d)
DefinitionInductive d -> reserveInductive d
@ -1176,7 +1154,6 @@ checkSections sec = do
goDefinition = \case
DefinitionSyntax s -> DefinitionSyntax <$> checkSyntaxDef s
DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d
DefinitionTypeSignature d -> DefinitionTypeSignature <$> checkTypeSignature d
DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d
DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d
DefinitionProjectionDef d -> DefinitionProjectionDef <$> checkProjectionDef d
@ -1225,13 +1202,8 @@ checkSections sec = do
_ -> fail
_ -> fail
mkLetSections :: [LetClause 'Parsed] -> StatementSections 'Parsed
mkLetSections = mkSections . map fromLetClause
where
fromLetClause :: LetClause 'Parsed -> Statement 'Parsed
fromLetClause = \case
LetTypeSig t -> StatementTypeSignature t
LetFunClause c -> StatementFunctionClause c
mkLetSections :: [FunctionDef 'Parsed] -> StatementSections 'Parsed
mkLetSections = mkSections . map StatementFunctionDef
mkSections :: [Statement 'Parsed] -> StatementSections 'Parsed
mkSections = \case
@ -1271,7 +1243,6 @@ mkSections = \case
fromStatement :: Statement 'Parsed -> Either (Definition 'Parsed) (NonDefinition 'Parsed)
fromStatement = \case
StatementAxiom a -> Left (DefinitionAxiom a)
StatementTypeSignature t -> Left (DefinitionTypeSignature t)
StatementFunctionDef n -> Left (DefinitionFunctionDef n)
StatementInductive i -> Left (DefinitionInductive i)
StatementSyntax s -> Left (DefinitionSyntax s)
@ -1279,7 +1250,6 @@ mkSections = \case
StatementImport i -> Right (NonDefinitionImport i)
StatementModule m -> Right (NonDefinitionModule m)
StatementOpenModule o -> Right (NonDefinitionOpenModule o)
StatementFunctionClause c -> Right (NonDefinitionFunctionClause c)
reserveLocalModuleSymbol ::
Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r =>
@ -1585,37 +1555,6 @@ checkOpenModule op
| isJust (op ^. openModuleImportKw) = checkOpenImportModule op
| otherwise = checkOpenModuleNoImport Nothing op
checkFunctionClause ::
forall r.
Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r =>
FunctionClause 'Parsed ->
Sem r (FunctionClause 'Scoped)
checkFunctionClause clause@FunctionClause {..} = do
clauseOwnerFunction' <- checkTypeSigInScope
registerName (S.unqualifiedSymbol clauseOwnerFunction')
(clausePatterns', clauseBody') <- withLocalScope $ do
clp <- mapM checkParsePatternAtom _clausePatterns
clb <- checkParseExpressionAtoms _clauseBody
return (clp, clb)
registerFunctionClause
@$> FunctionClause
{ _clauseOwnerFunction = clauseOwnerFunction',
_clausePatterns = clausePatterns',
_clauseBody = clauseBody',
_clauseAssignKw
}
where
fun = _clauseOwnerFunction
checkTypeSigInScope :: Sem r S.Symbol
checkTypeSigInScope = do
ms <- HashMap.lookup fun <$> gets (^. scopeLocalSymbols)
sym <- maybe err return ms
unless (S.isFunctionKind sym) err
return (set S.nameConcrete _clauseOwnerFunction sym)
where
err :: Sem r a
err = throw (ErrLacksTypeSig (LacksTypeSig clause))
checkAxiomDef ::
Members '[Reader ScopeParameters, InfoTableBuilder, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperSyntax, Reader BindingStrategy] r =>
AxiomDef 'Parsed ->
@ -1649,11 +1588,11 @@ checkFunction f = do
return Function {..}
-- | for now functions defined in let clauses cannot be infix operators
checkLetClauses ::
checkLetFunDefs ::
Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
NonEmpty (LetClause 'Parsed) ->
Sem r (NonEmpty (LetClause 'Scoped))
checkLetClauses =
NonEmpty (FunctionDef 'Parsed) ->
Sem r (NonEmpty (FunctionDef 'Scoped))
checkLetFunDefs =
localBindings
. ignoreSyntax
. fmap fromSections
@ -1661,31 +1600,29 @@ checkLetClauses =
. mkLetSections
. toList
where
fromSections :: StatementSections s -> NonEmpty (LetClause s)
fromSections :: StatementSections s -> NonEmpty (FunctionDef s)
fromSections = \case
SectionsEmpty -> impossible
SectionsDefinitions d -> fromDefs d
SectionsNonDefinitions d -> fromNonDefs d
where
fromDefs :: DefinitionsSection s -> NonEmpty (LetClause s)
fromDefs :: DefinitionsSection s -> NonEmpty (FunctionDef s)
fromDefs DefinitionsSection {..} =
(fromDef <$> _definitionsSection) <>? (fromNonDefs <$> _definitionsNext)
where
fromDef :: Definition s -> LetClause s
fromDef :: Definition s -> FunctionDef s
fromDef = \case
DefinitionTypeSignature d -> LetTypeSig d
DefinitionFunctionDef {} -> impossible
DefinitionFunctionDef d -> d
DefinitionInductive {} -> impossible
DefinitionProjectionDef {} -> impossible
DefinitionAxiom {} -> impossible
DefinitionSyntax {} -> impossible
fromNonDefs :: NonDefinitionsSection s -> NonEmpty (LetClause s)
fromNonDefs :: NonDefinitionsSection s -> NonEmpty (FunctionDef s)
fromNonDefs NonDefinitionsSection {..} =
(fromNonDef <$> _nonDefinitionsSection) <>? (fromDefs <$> _nonDefinitionsNext)
where
fromNonDef :: NonDefinition s -> LetClause s
fromNonDef :: NonDefinition s -> FunctionDef s
fromNonDef = \case
NonDefinitionFunctionClause f -> LetFunClause f
NonDefinitionImport {} -> impossible
NonDefinitionModule {} -> impossible
NonDefinitionOpenModule {} -> impossible
@ -1779,11 +1716,11 @@ checkLet ::
Sem r (Let 'Scoped)
checkLet Let {..} =
withLocalScope $ do
letClauses' <- checkLetClauses _letClauses
letFunDefs' <- checkLetFunDefs _letFunDefs
letExpression' <- checkParseExpressionAtoms _letExpression
return
Let
{ _letClauses = letClauses',
{ _letFunDefs = letFunDefs',
_letExpression = letExpression',
_letKw,
_letInKw

4
src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
View File

@ -16,8 +16,6 @@ data ScoperError
| ErrAppLeftImplicit AppLeftImplicit
| ErrInfixPattern InfixErrorP
| ErrMultipleDeclarations MultipleDeclarations
| ErrLacksTypeSig LacksTypeSig
| ErrLacksFunctionClause LacksFunctionClause
| ErrImportCycle ImportCycle
| ErrSymNotInScope NotInScope
| ErrQualSymNotInScope QualSymNotInScope
@ -56,7 +54,6 @@ instance ToGenericError ScoperError where
ErrAppLeftImplicit e -> genericError e
ErrInfixPattern e -> genericError e
ErrMultipleDeclarations e -> genericError e
ErrLacksTypeSig e -> genericError e
ErrImportCycle e -> genericError e
ErrSymNotInScope e -> genericError e
ErrQualSymNotInScope e -> genericError e
@ -68,7 +65,6 @@ instance ToGenericError ScoperError where
ErrAmbiguousModuleSym e -> genericError e
ErrUnusedOperatorDef e -> genericError e
ErrUnusedIteratorDef e -> genericError e
ErrLacksFunctionClause e -> genericError e
ErrDoubleBracesPattern e -> genericError e
ErrDoubleBinderPattern e -> genericError e
ErrAliasBinderPattern e -> genericError e

77
src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
View File

@ -8,7 +8,6 @@ where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Data.List.NonEmpty.Extra qualified as NonEmpty
import Data.Text qualified as Text
import Juvix.Compiler.Concrete.Data.Scope
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Language
@ -96,82 +95,6 @@ instance ToGenericError InfixErrorP where
<> line
<> "Perhaps you forgot parentheses around a pattern?"
-- | function clause without a type signature.
newtype LacksTypeSig = LacksTypeSig
{ _lacksTypeSigClause :: FunctionClause 'Parsed
}
deriving stock (Show)
instance ToGenericError LacksTypeSig where
genericError LacksTypeSig {..} = ask >>= generr
where
generr opts =
return
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
opts' = fromGenericOptions opts
i = _lacksTypeSigClause ^. clauseOwnerFunction . symbolLoc
msg =
"The declaration is missing a type signature:"
<> line
<> indent' (ppCode opts' _lacksTypeSigClause)
<> checkColon _lacksTypeSigClause
checkColon :: FunctionClause 'Parsed -> Doc Ann
checkColon fc@FunctionClause {..} =
case Text.splitOn ":" (_clauseOwnerFunction ^. withLocParam) of
[x, ""] -> makeMessage x [":"]
[x, y] -> makeMessage x [":", y]
_ -> mempty
where
makeMessage :: Text -> [Text] -> Doc Ann
makeMessage x xs =
line
<> "Perhaps you meant:"
<> line
<> indent'
( ppCode
opts'
(adjustPatterns x xs)
)
adjustPatterns :: Text -> [Text] -> FunctionClause 'Parsed
adjustPatterns x xs =
( over clauseOwnerFunction (set withLocParam x) $
over clausePatterns (map mkpat xs ++) fc
)
mkpat :: Text -> PatternAtom 'Parsed
mkpat txt = PatternAtomIden (NameUnqualified (set withLocParam txt _clauseOwnerFunction))
-- | type signature without a function clause
newtype LacksFunctionClause = LacksFunctionClause
{ _lacksFunctionClause :: TypeSignature 'Scoped
}
deriving stock (Show)
instance ToGenericError LacksFunctionClause where
genericError LacksFunctionClause {..} = ask >>= generr
where
generr opts =
return
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
opts' = fromGenericOptions opts
i = getLoc (_lacksFunctionClause ^. sigName)
msg =
"Type signature with no function clause:"
<> line
<> indent' (ppCode opts' _lacksFunctionClause)
newtype ImportCycle = ImportCycle
{ -- | If we have [a, b, c] it means that a import b imports c imports a.
_importCycleImports :: NonEmpty (Import 'Parsed)

110
src/Juvix/Compiler/Concrete/Translation/FromSource.hs
View File

@ -205,9 +205,7 @@ replInput :: forall r. Members '[Files, PathResolver, InfoTableBuilder, JudocSta
replInput =
P.label "<repl input>" $
ReplExpression <$> parseExpressionAtoms
<|> P.try (ReplOpenImport <$> newOpenSyntax)
<|> ReplImport <$> import_
<|> ReplOpenImport <$> openModule
<|> either ReplImport ReplOpenImport <$> importOpenSyntax
--------------------------------------------------------------------------------
-- Symbols and names
@ -296,22 +294,14 @@ statement = P.label "<top level statement>" $ do
optional_ stashPragmas
ms <-
optional
( StatementOpenModule
<$> newOpenSyntax
-- TODO remove <?|> after removing old syntax
<?|> StatementFunctionDef
<$> newTypeSignature Nothing
-- TODO remove <?|> after removing old syntax
<?|> StatementOpenModule
<$> openModule
( either StatementImport StatementOpenModule <$> importOpenSyntax
<|> StatementOpenModule <$> openModule
<|> StatementSyntax <$> syntaxDef
<|> StatementImport <$> import_
<|> StatementInductive <$> inductiveDef Nothing
<|> StatementModule <$> moduleDef
<|> StatementAxiom <$> axiomDef Nothing
<|> builtinStatement
<|> either StatementTypeSignature StatementFunctionClause
<$> auxTypeSigFunClause
<|> StatementFunctionDef <$> functionDefinition Nothing
)
case ms of
Just s -> return s
@ -490,27 +480,17 @@ builtinAxiomDef ::
ParsecS r (AxiomDef 'Parsed)
builtinAxiomDef = axiomDef . Just
builtinTypeSig ::
Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
WithLoc BuiltinFunction ->
ParsecS r (TypeSignature 'Parsed)
builtinTypeSig b = do
terminating <- optional (kw kwTerminating)
fun <- symbol
typeSignature terminating fun (Just b)
builtinNewTypeSig ::
builtinFunctionDef ::
Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
WithLoc BuiltinFunction ->
ParsecS r (FunctionDef 'Parsed)
builtinNewTypeSig = newTypeSignature . Just
builtinFunctionDef = functionDefinition . Just
builtinStatement :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed)
builtinStatement = do
void (kw kwBuiltin)
(builtinInductive >>= fmap StatementInductive . builtinInductiveDef)
<|> (builtinFunction >>= fmap StatementFunctionDef . builtinNewTypeSig)
<?|> (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig)
<|> (builtinFunction >>= fmap StatementFunctionDef . builtinFunctionDef)
<|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef)
--------------------------------------------------------------------------------
@ -838,15 +818,18 @@ literal = do
<|> literalString
P.lift (registerLiteral l)
letClause :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (LetClause 'Parsed)
letClause = do
letFunDef ::
forall r.
Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
ParsecS r (FunctionDef 'Parsed)
letFunDef = do
optional_ stashPragmas
either LetTypeSig LetFunClause <$> auxTypeSigFunClause
functionDefinition Nothing
letBlock :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Let 'Parsed)
letBlock = do
_letKw <- kw kwLet
_letClauses <- P.sepEndBy1 letClause semicolon
_letFunDefs <- P.sepEndBy1 letFunDef semicolon
_letInKw <- Irrelevant <$> kw kwIn
_letExpression <- parseExpressionAtoms
return Let {..}
@ -897,52 +880,12 @@ getPragmas = P.lift $ do
put (Nothing @ParsedPragmas)
return j
typeSignature ::
Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
Maybe KeywordRef ->
Symbol ->
Maybe (WithLoc BuiltinFunction) ->
ParsecS r (TypeSignature 'Parsed)
typeSignature _sigTerminating _sigName _sigBuiltin = P.label "<type signature>" $ do
_sigColonKw <- Irrelevant <$> kw kwColon
_sigType <- parseExpressionAtoms
_sigDoc <- getJudoc
_sigPragmas <- getPragmas
body <- optional $ do
k <- Irrelevant <$> kw kwAssign
(k,) <$> parseExpressionAtoms
let _sigBody = snd <$> body
_sigAssignKw = mapM fst body
return TypeSignature {..}
-- | Used to minimize the amount of required @P.try@s.
auxTypeSigFunClause ::
forall r.
(Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
ParsecS r (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed))
auxTypeSigFunClause = do
terminating <- optional (kw kwTerminating)
sym <- symbol
if
| isJust terminating ->
Left <$> typeSignature terminating sym Nothing
| otherwise ->
checkEq
<|> Left <$> typeSignature terminating sym Nothing
<|> Right <$> functionClause sym
where
checkEq :: ParsecS r a
checkEq = do
off <- P.getOffset
kw kwEq
parseFailure off "expected \":=\" instead of \"=\""
newTypeSignature ::
functionDefinition ::
forall r.
Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
Maybe (WithLoc BuiltinFunction) ->
ParsecS r (FunctionDef 'Parsed)
newTypeSignature _signBuiltin = P.label "<function definition>" $ do
functionDefinition _signBuiltin = P.label "<function definition>" $ do
_signTerminating <- optional (kw kwTerminating)
_signName <- symbol
_signArgs <- many parseArg
@ -1250,17 +1193,6 @@ parsePatternAtomsNested = do
(_patternAtoms, _patternAtomsLoc) <- second Irrelevant <$> interval (P.some patternAtomNested)
return PatternAtoms {..}
--------------------------------------------------------------------------------
-- Function binding declaration
--------------------------------------------------------------------------------
functionClause :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Symbol -> ParsecS r (FunctionClause 'Parsed)
functionClause _clauseOwnerFunction = do
_clausePatterns <- P.many patternAtom
_clauseAssignKw <- Irrelevant <$> kw kwAssign
_clauseBody <- parseExpressionAtoms
return FunctionClause {..}
--------------------------------------------------------------------------------
-- Module declaration
--------------------------------------------------------------------------------
@ -1320,9 +1252,8 @@ usingOrHiding =
Using <$> pusingList
<|> Hiding <$> phidingList
newOpenSyntax :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (OpenModule 'Parsed)
newOpenSyntax = do
im <- import_
openSyntax :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Import 'Parsed -> ParsecS r (OpenModule 'Parsed)
openSyntax im = do
_openModuleKw <- kw kwOpen
_openUsingHiding <- optional usingOrHiding
_openPublicKw <- Irrelevant <$> optional (kw kwPublic)
@ -1331,3 +1262,8 @@ newOpenSyntax = do
_openImportAsName = im ^. importAsName
_openPublic = maybe NoPublic (const Public) (_openPublicKw ^. unIrrelevant)
return OpenModule {..}
importOpenSyntax :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Either (Import 'Parsed) (OpenModule 'Parsed))
importOpenSyntax = do
im <- import_
(Right <$> openSyntax im) <|> return (Left im)

110
src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
View File

@ -286,9 +286,8 @@ goModuleBody stmts = do
_moduleImports <- mapM goImport (scanImports stmts)
otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goAxiomInductive) ss
functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions
newFunctions <- map (fmap Internal.PreFunctionDef) <$> newCompiledFunctions
projections <- map (fmap Internal.PreFunctionDef) <$> mkProjections
let unsorted = otherThanFunctions <> functions <> newFunctions <> projections
let unsorted = otherThanFunctions <> functions <> projections
_moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx) unsorted)
return Internal.ModuleBody {..}
where
@ -306,27 +305,13 @@ goModuleBody stmts = do
let funDef = goProjectionDef f
]
newCompiledFunctions :: Sem r [Indexed Internal.FunctionDef]
newCompiledFunctions =
sequence
[ Indexed i <$> funDef
| Indexed i (StatementFunctionDef f) <- ss,
let funDef = goTopNewFunctionDef f
]
compiledFunctions :: Sem r [Indexed Internal.FunctionDef]
compiledFunctions =
sequence
[ Indexed i <$> funDef
| Indexed i sig <- sigs,
let name = sig ^. sigName,
let funDef = goTopFunctionDef sig (getClauses name)
| Indexed i (StatementFunctionDef f) <- ss,
let funDef = goTopFunctionDef f
]
where
getClauses :: S.Symbol -> [FunctionClause 'Scoped]
getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
sigs :: [Indexed (TypeSignature 'Scoped)]
sigs = [Indexed i t | Indexed i (StatementTypeSignature t) <- ss]
scanImports :: [Statement 'Scoped] -> [Import 'Scoped]
scanImports stmts = mconcatMap go stmts
@ -337,8 +322,6 @@ scanImports stmts = mconcatMap go stmts
StatementModule m -> concatMap go (m ^. moduleBody)
StatementOpenModule o -> maybeToList (openImport o)
StatementInductive {} -> []
StatementFunctionClause {} -> []
StatementTypeSignature {} -> []
StatementAxiom {} -> []
StatementSyntax {} -> []
StatementFunctionDef {} -> []
@ -390,8 +373,6 @@ goAxiomInductive = \case
StatementFunctionDef {} -> return []
StatementSyntax {} -> return []
StatementOpenModule {} -> return []
StatementTypeSignature {} -> return []
StatementFunctionClause {} -> return []
StatementProjectionDef {} -> return []
goOpenModule' ::
@ -423,39 +404,9 @@ goOpenModule o = goOpenModule' o
goLetFunctionDef ::
Members '[Builtins, NameIdGen, Reader Pragmas, Error ScoperError] r =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
FunctionDef 'Scoped ->
Sem r Internal.FunctionDef
goLetFunctionDef = goFunctionDefHelper
goFunctionDefHelper ::
forall r.
Members '[Builtins, NameIdGen, Reader Pragmas, Error ScoperError] r =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Internal.FunctionDef
goFunctionDefHelper sig@TypeSignature {..} clauses = do
let _funDefName = goSymbol _sigName
_funDefTerminating = isJust _sigTerminating
_funDefBuiltin = (^. withLocParam) <$> _sigBuiltin
_funDefType <- goExpression _sigType
_funDefExamples <- goExamples _sigDoc
_funDefPragmas <- goPragmas _sigPragmas
_funDefClauses <- case (_sigBody, nonEmpty clauses) of
(Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig))
(Just {}, Just {}) -> error "duplicate function clause. TODO remove this when old function syntax is removed"
(Just body, Nothing) -> do
body' <- goExpression body
return
( pure
Internal.FunctionClause
{ _clauseName = _funDefName,
_clausePatterns = [],
_clauseBody = body'
}
)
(Nothing, Just clauses') -> mapM goFunctionClause clauses'
return Internal.FunctionDef {..}
goLetFunctionDef = goTopFunctionDef
goProjectionDef ::
forall r.
@ -467,12 +418,12 @@ goProjectionDef ProjectionDef {..} = do
info <- gets @ConstructorInfos (^?! at c . _Just)
Internal.genFieldProjection (goSymbol _projectionField) info _projectionFieldIx
goTopNewFunctionDef ::
goTopFunctionDef ::
forall r.
Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r =>
FunctionDef 'Scoped ->
Sem r Internal.FunctionDef
goTopNewFunctionDef FunctionDef {..} = do
goTopFunctionDef FunctionDef {..} = do
let _funDefName = goSymbol _signName
_funDefTerminating = isJust _signTerminating
_funDefBuiltin = (^. withLocParam) <$> _signBuiltin
@ -480,7 +431,9 @@ goTopNewFunctionDef FunctionDef {..} = do
_funDefExamples <- goExamples _signDoc
_funDefPragmas <- goPragmas _signPragmas
_funDefClauses <- goBody
return Internal.FunctionDef {..}
let fun = Internal.FunctionDef {..}
whenJust _signBuiltin (registerBuiltinFunction fun . (^. withLocParam))
return fun
where
goBody :: Sem r (NonEmpty Internal.FunctionClause)
goBody = do
@ -536,17 +489,6 @@ goTopNewFunctionDef FunctionDef {..} = do
return Internal.PatternArg {..}
mapM mk _sigArgNames
goTopFunctionDef ::
forall r.
(Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Internal.FunctionDef
goTopFunctionDef sig clauses = do
fun <- goFunctionDefHelper sig clauses
whenJust (sig ^. sigBuiltin) (registerBuiltinFunction fun . (^. withLocParam))
return fun
goExamples ::
forall r.
Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r =>
@ -563,20 +505,6 @@ goExamples = mapM goExample . maybe [] judocExamples
_exampleId = ex ^. exampleId
}
goFunctionClause ::
Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r =>
FunctionClause 'Scoped ->
Sem r Internal.FunctionClause
goFunctionClause FunctionClause {..} = do
_clausePatterns' <- mapM goPatternArg _clausePatterns
_clauseBody' <- goExpression _clauseBody
return
Internal.FunctionClause
{ _clauseName = goSymbol _clauseOwnerFunction,
_clausePatterns = _clausePatterns',
_clauseBody = _clauseBody'
}
goInductiveParameters ::
forall r.
Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r =>
@ -918,24 +846,16 @@ goExpression = \case
goLet :: Let 'Scoped -> Sem r Internal.Let
goLet l = do
_letExpression <- goExpression (l ^. letExpression)
_letClauses <- goLetClauses (l ^. letClauses)
_letClauses <- goLetFunDefs (l ^. letFunDefs)
return Internal.Let {..}
where
goLetClauses :: NonEmpty (LetClause 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
goLetClauses cl = fmap goSCC <$> preLetStatements cl
goLetFunDefs :: NonEmpty (FunctionDef 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
goLetFunDefs cl = fmap goSCC <$> preLetStatements cl
preLetStatements :: NonEmpty (LetClause 'Scoped) -> Sem r (NonEmpty (SCC Internal.PreLetStatement))
preLetStatements :: NonEmpty (FunctionDef 'Scoped) -> Sem r (NonEmpty (SCC Internal.PreLetStatement))
preLetStatements cl = do
pre <- nonEmpty' <$> sequence [Internal.PreLetFunctionDef <$> goSig sig | LetTypeSig sig <- toList cl]
pre <- mapM (fmap Internal.PreLetFunctionDef . goLetFunctionDef) cl
return (buildLetMutualBlocks pre)
where
goSig :: TypeSignature 'Scoped -> Sem r Internal.FunctionDef
goSig sig = goLetFunctionDef sig clauses
where
clauses :: [FunctionClause 'Scoped]
clauses =
[ c | LetFunClause c <- toList cl, sig ^. sigName == c ^. clauseOwnerFunction
]
goSCC :: SCC Internal.PreLetStatement -> Internal.LetClause
goSCC = \case

21
src/Juvix/Formatter.hs
View File

@ -2,7 +2,6 @@ module Juvix.Formatter where
import Data.List.NonEmpty qualified as NonEmpty
import Data.Text qualified as T
import Juvix.Compiler.Concrete.Extra (migrateFunctionSyntax)
import Juvix.Compiler.Concrete.Language
import Juvix.Compiler.Concrete.Print (ppOutDefault)
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
@ -18,8 +17,6 @@ data FormattedFileInfo = FormattedFileInfo
_formattedFileInfoContentsModified :: Bool
}
newtype NewSyntax = NewSyntax Bool
data ScopeEff m a where
ScopeFile :: Path Abs File -> ScopeEff m Scoper.ScoperResult
ScopeStdin :: ScopeEff m Scoper.ScoperResult
@ -65,7 +62,7 @@ formattedFileInfoContentsText = to infoToPlainText
-- contents of the file.
format ::
forall r.
Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r =>
Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
Path Abs File ->
Sem r FormatResult
format p = do
@ -91,7 +88,7 @@ format p = do
-- subdirectories that contain a juvix.yaml file.
formatProject ::
forall r.
Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r =>
Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
Path Abs Dir ->
Sem r FormatResult
formatProject p = do
@ -108,14 +105,14 @@ formatProject p = do
subRes <- combineResults <$> mapM format juvixFiles
return (res <> subRes, RecurseFilter (\hasJuvixYaml d -> not hasJuvixYaml && not (isHiddenDirectory d)))
formatPath :: Members '[Reader NewSyntax, Reader Text, ScopeEff] r => Path Abs File -> Sem r (NonEmpty AnsiText)
formatPath :: Members '[Reader Text, ScopeEff] r => Path Abs File -> Sem r (NonEmpty AnsiText)
formatPath p = do
res <- scopeFile p
formatScoperResult res
formatStdin ::
forall r.
Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r =>
Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
Sem r FormatResult
formatStdin = do
res <- scopeStdin
@ -147,7 +144,7 @@ formatResultFromContents formattedContents filepath = do
)
return res
formatScoperResult :: Members '[Reader NewSyntax, Reader Text] r => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText)
formatScoperResult :: Members '[Reader Text] r => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText)
formatScoperResult res = do
let cs = res ^. Scoper.comments
formattedModules <-
@ -165,11 +162,7 @@ formatScoperResult res = do
Nothing ->
return formattedModules
where
formatTopModule :: Members '[Reader NewSyntax, Reader Comments] r => Module 'Scoped 'ModuleTop -> Sem r AnsiText
formatTopModule :: Members '[Reader Comments] r => Module 'Scoped 'ModuleTop -> Sem r AnsiText
formatTopModule m = do
NewSyntax newSyntax <- ask
cs <- ask
let m'
| newSyntax = migrateFunctionSyntax m
| otherwise = m
return (ppOutDefault cs m')
return (ppOutDefault cs m)

1
test/Formatter/Positive.hs
View File

@ -28,7 +28,6 @@ makeFormatTest' Scope.PosTest {..} =
. runOutputList @FormattedFileInfo
. runScopeEffIO
. runFilesIO
. runReader (NewSyntax False)
$ format file'
case d of
Right (_, FormatResultOK) -> return ()

28
test/Scope/Negative.hs
View File

@ -134,20 +134,6 @@ scoperErrorTests =
$ \case
ErrAmbiguousSym {} -> Nothing
_ -> wrongError,
NegTest
"Lacks function clause"
$(mkRelDir ".")
$(mkRelFile "LacksFunctionClause.juvix")
$ \case
ErrLacksFunctionClause {} -> Nothing
_ -> wrongError,
NegTest
"Lacks function clause inside let"
$(mkRelDir ".")
$(mkRelFile "LetMissingClause.juvix")
$ \case
ErrLacksFunctionClause {} -> Nothing
_ -> wrongError,
NegTest
"Ambiguous export"
$(mkRelDir ".")
@ -225,20 +211,6 @@ scoperErrorTests =
$ \case
ErrNameSignature (ErrDuplicateName DuplicateName {}) -> Nothing
_ -> wrongError,
NegTest
"A function lacks a type signature"
$(mkRelDir ".")
$(mkRelFile "LacksTypeSig.juvix")
$ \case
ErrLacksTypeSig {} -> Nothing
_ -> wrongError,
NegTest
"A function inside a let lacks a type signature that is at the top level"
$(mkRelDir ".")
$(mkRelFile "LacksTypeSig2.juvix")
$ \case
ErrLacksTypeSig {} -> Nothing
_ -> wrongError,
NegTest
"Using symbol that is not exported"
$(mkRelDir "UsingHiding")

14
tests/Compilation/negative/test001.juvix
View File

@ -1,14 +1,12 @@
-- pattern matching coverage
module test001;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
f : List Nat -> List Nat -> Nat;
f (x :: xs) (y :: ys) := x + y;
f _ (_ :: (z :: zs)) := z;
f _ nil := 0;
f : List Nat -> List Nat -> Nat
| (x :: xs) (y :: ys) := x + y
| _ (_ :: z :: zs) := z
| _ nil := 0;
main : Nat;
main := f (1 :: nil) (2 :: nil);
main : Nat := f (1 :: nil) (2 :: nil);
end;

13
tests/Compilation/negative/test002.juvix
View File

@ -1,12 +1,11 @@
-- pattern matching coverage in cases
module test002;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
f : List Nat -> Nat;
f x := case x
| nil := 0
| x :: y :: _ := x + y;
f (x : List Nat) : Nat :=
case x
| nil := 0
| x :: y :: _ := x + y;
main : Nat;
main := f (1 :: 2 :: nil);
main : Nat := f (1 :: 2 :: nil);

5
tests/Compilation/negative/test003.juvix
View File

@ -1,7 +1,6 @@
-- pattern matching coverage in lambdas
module test003;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : Nat;
main := λ{ zero := 1 | (suc (suc _)) := 2 } 1;
main : Nat := λ{ zero := 1 | (suc (suc _)) := 2 } 1;

5
tests/Compilation/negative/test004.juvix
View File

@ -1,6 +1,5 @@
module test004;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : Nat -> Nat;
main x := x;
main (x : Nat) : Nat := x;

3
tests/Compilation/negative/test005.juvix
View File

@ -5,5 +5,4 @@ type Unit := unit : Unit;
axiom Boom : Unit;
x : Unit;
x := Boom;
x : Unit := Boom;

7
tests/Compilation/positive/test001.juvix
View File

@ -1,8 +1,5 @@
module test001;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main := printNatLn (5 + 2 * 3);
end;
main : IO := printNatLn (5 + 2 * 3);

7
tests/Compilation/positive/test002.juvix
View File

@ -1,8 +1,5 @@
module test002;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main := printNatLn ((\{ x y z := z + x * y }) 2 3 5);
end;
main : IO := printNatLn (\ {x y z := z + x * y} 2 3 5);

17
tests/Compilation/positive/test003.juvix
View File

@ -9,14 +9,11 @@ Multiline comment
-}
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main :=
printNatLn (mod 3 2) >>
printNatLn (div 18 4) >>
printNatLn (mod 18 4) >>
printNatLn (div 16 4) >>
printNatLn (mod 16 4);
end;
main : IO :=
printNatLn (mod 3 2)
>> printNatLn (div 18 4)
>> printNatLn (mod 18 4)
>> printNatLn (div 16 4)
>> printNatLn (mod 16 4);

19
tests/Compilation/positive/test004.juvix
View File

@ -1,15 +1,12 @@
-- Test IO builtins
module test004;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main :=
printNat 1 >>
printNat 2 >>
printNat 3 >>
printNat 4 >>
printNat 5 >>
printString "\n";
end;
main : IO :=
printNat 1
>> printNat 2
>> printNat 3
>> printNat 4
>> printNat 5
>> printString "\n";

24
tests/Compilation/positive/test005.juvix
View File

@ -1,18 +1,20 @@
-- Higher-order functions
module test005;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
S : {A B C : Type} → (A → B → C) → (A → B) → A → C;
S x y z := x z (y z);
S {A B C} (x : A → B → C) (y : A → B) (z : A) : C :=
x z (y z);
K : {A B : Type} → A → B → A;
K x y := x;
K {A B} (x : A) (_ : B) : A := x;
I : {A : Type} → A → A;
I := S K (K {_} {Bool});
I {A} : A → A := S K (K {_} {Bool});
main : IO;
main := printNatLn (I 1 + I I 1 + I (I 1) + I I I 1 + I (I I) I (I I I) 1 + I I I (I I I (I I)) I (I I) I I I 1);
end;
main : IO :=
printNatLn
(I 1
+ I I 1
+ I (I 1)
+ I I I 1
+ I (I I) I (I I I) 1
+ I I I (I I I (I I)) I (I I) I I I 1);

18
tests/Compilation/positive/test006.juvix
View File

@ -1,16 +1,14 @@
-- if-then-else and lazy boolean operators
module test006;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
terminating
loop : Nat;
loop := loop;
loop : Nat := loop;
main : IO;
main := printNatLn ((if (3 > 0) 1 loop) + (if (2 < 1) loop (if (7 >= 8) loop 1))) >>
printBoolLn (2 > 0 || loop == 0) >>
printBoolLn (2 < 0 && loop == 0);
end;
main : IO :=
printNatLn
(if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1))
>> printBoolLn (2 > 0 || loop == 0)
>> printBoolLn (2 < 0 && loop == 0);

48
tests/Compilation/positive/test007.juvix
View File

@ -1,34 +1,34 @@
-- pattern matching and lambda-case
module test007;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
map' : {A : Type} → {B : Type} → (A → B) → List A → List B;
map' f := \{ nil := nil | (h :: t) := f h :: map' f t};
map' {A B} (f : A → B) : List A → List B :=
\ {
| nil := nil
| (h :: t) := f h :: map' f t
};
terminating
map'' : {A : Type} → {B : Type} → (A → B) → List A → List B;
map'' f x := if (null x) nil (f (head x) :: map'' f (tail x));
map'' {A B} (f : A → B) (x : List A) : List B :=
if (null x) nil (f (head x) :: map'' f (tail x));
lst : List Nat;
lst := 0 :: 1 :: nil;
lst : List Nat := 0 :: 1 :: nil;
printNatList : List Nat → IO;
printNatList nil := printString "nil";
printNatList (h :: t) := printNat h >> printString " :: " >> printNatList t;
printNatList : List Nat → IO
| nil := printString "nil"
| (h :: t) :=
printNat h >> printString " :: " >> printNatList t;
printNatListLn : List Nat → IO;
printNatListLn lst := printNatList lst >> printString "\n";
printNatListLn (lst : List Nat) : IO :=
printNatList lst >> printString "\n";
main : IO;
main :=
printBoolLn (null lst) >>
printBoolLn (null (nil {Nat})) >>
printNatLn (head lst) >>
printNatListLn (tail lst) >>
printNatLn (head (tail lst)) >>
printNatListLn (map ((+) 1) lst) >>
printNatListLn (map' ((+) 1) lst) >>
printNatListLn (map'' ((+) 1) lst);
end;
main : IO :=
printBoolLn (null lst)
>> printBoolLn (null (nil {Nat}))
>> printNatLn (head lst)
>> printNatListLn (tail lst)
>> printNatLn (head (tail lst))
>> printNatListLn (map ((+) 1) lst)
>> printNatListLn (map' ((+) 1) lst)
>> printNatListLn (map'' ((+) 1) lst);

13
tests/Compilation/positive/test008.juvix
View File

@ -1,13 +1,10 @@
-- recursion
module test008;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
sum : Nat → Nat;
sum zero := 0;
sum (suc x) := suc x + sum x;
sum : Nat → Nat
| zero := 0
| (suc x) := suc x + sum x;
main : IO;
main := printNatLn (sum 10000);
end;
main : IO := printNatLn (sum 10000);

33
tests/Compilation/positive/test009.juvix
View File

@ -1,27 +1,22 @@
-- tail recursion
module test009;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
sum' : Nat → Nat → Nat;
sum' acc zero := acc;
sum' acc (suc x) := sum' (suc x + acc) x;
sum' (acc : Nat) : Nat → Nat
| zero := acc
| (suc x) := sum' (suc x + acc) x;
sum : Nat → Nat;
sum := sum' 0;
sum : Nat → Nat := sum' 0;
fact' : Nat → Nat → Nat;
fact' acc zero := acc;
fact' acc (suc x) := fact' (acc * suc x) x;
fact' (acc : Nat) : Nat → Nat
| zero := acc
| (suc x) := fact' (acc * suc x) x;
fact : Nat → Nat;
fact := fact' 1;
fact : Nat → Nat := fact' 1;
main : IO;
main :=
printNatLn (sum 10000) >>
printNatLn (fact 5) >>
printNatLn (fact 10) >>
printNatLn (fact 12);
end;
main : IO :=
printNatLn (sum 10000)
>> printNatLn (fact 5)
>> printNatLn (fact 10)
>> printNatLn (fact 12);

29
tests/Compilation/positive/test010.juvix
View File

@ -1,15 +1,22 @@
-- let
module test010;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main :=
let x : Nat; x := 1 in
let x1 : Nat; x1 := x + let x2 : Nat; x2 := 2 in x2 in
let x3 : Nat; x3 := x1 * x1 in
let y : Nat; y := x3 + 2 in
let z : Nat; z := x3 + y in
printNatLn (x + y + z);
end;
main : IO :=
let
x : Nat := 1;
in let
x1 :
Nat :=
x
+ let
x2 : Nat := 2;
in x2;
in let
x3 : Nat := x1 * x1;
in let
y : Nat := x3 + 2;
in let
z : Nat := x3 + y;
in printNatLn (x + y + z);

19
tests/Compilation/positive/test011.juvix
View File

@ -1,16 +1,15 @@
-- tail recursion: compute the n-th Fibonacci number in O(n)
module test011;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
fib' : Nat → Nat → Nat → Nat;
fib' x y zero := x;
fib' x y (suc n) := fib' y (x + y) n;
fib' : Nat → Nat → Nat → Nat
| x y zero := x
| x y (suc n) := fib' y (x + y) n;
fib : Nat → Nat;
fib := fib' 0 1;
fib : Nat → Nat := fib' 0 1;
main : IO;
main := printNatLn (fib 10) >> printNatLn (fib 100) >> printNatLn (fib 1000);
end;
main : IO :=
printNatLn (fib 10)
>> printNatLn (fib 100)
>> printNatLn (fib 1000);

60
tests/Compilation/positive/test012.juvix
View File

@ -1,36 +1,42 @@
-- trees
module test012;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
type Tree :=
leaf : Tree
| node1 : Tree → Tree
| node2 : Tree → Tree → Tree
| node3 : Tree → Tree → Tree → Tree;
| leaf : Tree
| node1 : Tree → Tree
| node2 : Tree → Tree → Tree
| node3 : Tree → Tree → Tree → Tree;
terminating
gen : Nat → Tree;
gen zero := leaf;
gen n := if (mod n 3 == 0)
(node1 (gen (sub n 1)))
(if (mod n 3 == 1)
(node2 (gen (sub n 1)) (gen (sub n 1)))
(node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1))));
gen : Nat → Tree
| zero := leaf
| n :=
if
(mod n 3 == 0)
(node1 (gen (sub n 1)))
(if
(mod n 3 == 1)
(node2 (gen (sub n 1)) (gen (sub n 1)))
(node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1))));
preorder : Tree → IO;
preorder leaf := printNat 0;
preorder (node1 c) := printNat 1 >> preorder c;
preorder (node2 l r) := printNat 2 >> preorder l >> preorder r;
preorder (node3 l m r) := printNat 3 >> preorder l >> preorder m >> preorder r;
preorder : Tree → IO
| leaf := printNat 0
| (node1 c) := printNat 1 >> preorder c
| (node2 l r) := printNat 2 >> preorder l >> preorder r
| (node3 l m r) :=
printNat 3 >> preorder l >> preorder m >> preorder r;
main : IO;
main :=
preorder (gen 3) >> printString "\n" >>
preorder (gen 4) >> printString "\n" >>
preorder (gen 5) >> printString "\n" >>
preorder (gen 6) >> printString "\n" >>
preorder (gen 7) >> printString "\n";
end;
main : IO :=
preorder (gen 3)
>> printString "\n"
>> preorder (gen 4)
>> printString "\n"
>> preorder (gen 5)
>> printString "\n"
>> preorder (gen 6)
>> printString "\n"
>> preorder (gen 7)
>> printString "\n";

34
tests/Compilation/positive/test013.juvix
View File

@ -1,23 +1,21 @@
-- functions returning functions with variable capture
module test013;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
f : Nat → Nat → Nat;
f x := if (x == 6)
λ{_ := 0}
(if (x == 5)
λ{_ := 1}
(if (x == 10)
λ{_ := λ{x := x} 2}
λ{x := x}));
f : Nat → Nat → Nat
| x :=
if
(x == 6)
λ {_ := 0}
(if
(x == 5)
λ {_ := 1}
(if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
main : IO;
main :=
printNatLn (f 5 6) >>
printNatLn (f 6 5) >>
printNatLn (f 10 5) >>
printNatLn (f 11 5);
end;
main : IO :=
printNatLn (f 5 6)
>> printNatLn (f 6 5)
>> printNatLn (f 10 5)
>> printNatLn (f 11 5);

50
tests/Compilation/positive/test014.juvix
View File

@ -1,40 +1,36 @@
-- arithmetic
module test014;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
f : Nat → Nat → IO;
f x y := printNatLn (x + y);
f (x y : Nat) : IO := printNatLn (x + y);
g : Nat → Nat → Nat;
g x y := sub (x + 21) (y * 7);
g (x y : Nat) : Nat := sub (x + 21) (y * 7);
h : (Nat → Nat → Nat) → Nat → Nat → Nat;
h f y z := f y y * z;
h (f : Nat → Nat → Nat) (y z : Nat) : Nat := f y y * z;
x : Nat;
x := 5;
x : Nat := 5;
y : Nat;
y := 17;
y : Nat := 17;
func : Nat → Nat;
func x := x + 4;
func (x : Nat) : Nat := x + 4;
z : Nat;
z := 0;
z : Nat := 0;
vx : Nat;
vx := 30;
vx : Nat := 30;
vy : Nat;
vy := 7;
vy : Nat := 7;
main : IO;
main :=
printNatLn (func (div y x)) >> -- 17 div 5 + 4 = 7
printNatLn (y + x * z) >> -- 17
printNatLn (vx + vy * (z + 1)) >> -- 37
f (h g 2 3) 4 -- (g 2 2) * 3 + 4 = (2+21-2*7)*3 + 4 = 9*3 + 4 = 27+4 = 31
end;
main : IO :=
printNatLn (func (div y x))
>> -- 17 div 5 + 4 = 7
printNatLn
(y + x * z)
>> -- 17
printNatLn
(vx + vy * (z + 1))
>> -- 37
f
(h g 2 3)
4;
-- (g 2 2) * 3 + 4 = (2+21-2*7)*3 + 4 = 9*3 + 4 = 27+4 = 31

24
tests/Compilation/positive/test015.juvix
View File

@ -1,34 +1,30 @@
-- local functions with free variables
module test015;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
terminating
f : Nat → Nat → Nat;
f x :=
let g : Nat → Nat; g y := x + y in
f : Nat → Nat → Nat
| x :=
let g (y : Nat) : Nat := x + y in
if (x == 0)
(f 10)
(if (x < 10)
λ{y := g (f (sub x 1) y)}
g);
g : Nat → (Nat → Nat) → Nat;
g x h := x + h x;
g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
terminating
h : Nat → Nat;
h zero := 0;
h (suc x) := g x h;
h : Nat → Nat
| zero := 0
| (suc x) := g x h;
main : IO;
main :=
main : IO :=
printNatLn (f 100 500) >> -- 600
printNatLn (f 5 0) >> -- 25
printNatLn (f 5 5) >> -- 30
printNatLn (h 10) >> -- 45
printNatLn (g 10 h) >> -- 55
printNatLn (g 3 (f 10));
end;

17
tests/Compilation/positive/test016.juvix
View File

@ -1,17 +1,14 @@
-- recursion through higher-order functions
module test016;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
g : (Nat → Nat) → Nat → Nat;
g f zero := 0;
g f (suc x) := f x;
g (f : Nat → Nat) : Nat → Nat
| zero := 0
| (suc x) := f x;
terminating
f : Nat → Nat;
f x := x + g f x;
f (x : Nat) : Nat := x + g f x;
main : IO;
main := printNatLn (f 10); -- 55
end;
main : IO := printNatLn (f 10);
-- 55

19
tests/Compilation/positive/test017.juvix
View File

@ -1,20 +1,15 @@
-- tail recursion through higher-order functions
module test017;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
sumb : Nat → (Nat → Nat → Nat) → Nat → Nat;
sumb acc f zero := acc;
sumb acc f (suc x) := f acc x;
sumb (acc : Nat) (f : Nat → Nat → Nat) : Nat → Nat
| zero := acc
| (suc x) := f acc x;
terminating
sum' : Nat → Nat → Nat;
sum' acc x := sumb (x + acc) sum' x;
sum' (acc x : Nat) : Nat := sumb (x + acc) sum' x;
sum : Nat → Nat;
sum := sum' 0;
sum : Nat → Nat := sum' 0;
main : IO;
main := printNatLn (sum 10000);
end;
main : IO := printNatLn (sum 10000);

18
tests/Compilation/positive/test018.juvix
View File

@ -1,18 +1,16 @@
-- higher-order functions & recursion
module test018;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
f : (Nat → Nat) → Nat;
f g := g 5;
f : (Nat → Nat) → Nat
| g := g 5;
h : Nat → Nat → Nat;
h x z := x + z;
h : Nat → Nat → Nat
| x z := x + z;
u : Nat → Nat;
u x := f (h 4) + x;
u : Nat → Nat
| x := f (h 4) + x;
main : IO;
main := printNatLn (u 2);
main : IO := printNatLn (u 2);
end;

10
tests/Compilation/positive/test019.juvix
View File

@ -1,13 +1,11 @@
-- self-application
module test019;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
-- change this to a lambda once we have type annotations for lambdas
app : ({A : Type} → A → A) → {A : Type} → A → A;
app x := x x;
app : ({A : Type} → A → A) → {A : Type} → A → A
| x := x x;
main : IO;
main := printNatLn (app id (3 + 4));
main : IO := printNatLn (app id (3 + 4));
end;

36
tests/Compilation/positive/test020.juvix
View File

@ -1,30 +1,26 @@
-- recursive functions
module test020;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
-- McCarthy's 91 function
terminating
f91 : Nat → Nat;
f91 n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
f91 : Nat → Nat
| n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
-- subtraction by increments
terminating
subp : Nat → Nat → Nat;
subp i j := if (i == j) 0 (subp i (j + 1) + 1);
subp : Nat → Nat → Nat
| i j := if (i == j) 0 (subp i (j + 1) + 1);
main : IO;
main :=
printNatLn (f91 101) >>
printNatLn (f91 95) >>
printNatLn (f91 16) >>
printNatLn (f91 5) >>
printNatLn (subp 101 1) >>
printNatLn (subp 11 5) >>
printNatLn (subp 10 4) >>
printNatLn (subp 1000 600) >>
printNatLn (subp 10000 6000);
end;
main : IO :=
printNatLn (f91 101)
>> printNatLn (f91 95)
>> printNatLn (f91 16)
>> printNatLn (f91 5)
>> printNatLn (subp 101 1)
>> printNatLn (subp 11 5)
>> printNatLn (subp 10 4)
>> printNatLn (subp 1000 600)
>> printNatLn (subp 10000 6000);

33
tests/Compilation/positive/test021.juvix
View File

@ -1,25 +1,24 @@
-- fast exponentiation
module test021;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
terminating
power' : Nat → Nat → Nat → Nat;
power' acc a b :=
if (b == 0)
acc
(if (mod b 2 == 0)
(power' acc (a * a) (div b 2))
(power' (acc * a) (a * a) (div b 2)));
power' : Nat → Nat → Nat → Nat
| acc a b :=
if
(b == 0)
acc
(if
(mod b 2 == 0)
(power' acc (a * a) (div b 2))
(power' (acc * a) (a * a) (div b 2)));
power : Nat → Nat → Nat;
power := power' 1;
power : Nat → Nat → Nat := power' 1;
main : IO;
main :=
printNatLn (power 2 3) >>
printNatLn (power 3 7) >>
printNatLn (power 5 11)
main : IO :=
printNatLn (power 2 3)
>> printNatLn (power 3 7)
>> printNatLn (power 5 11);
end;

41
tests/Compilation/positive/test022.juvix
View File

@ -1,30 +1,29 @@
-- lists
module test022;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
gen : Nat → List Nat;
gen zero := nil;
gen n@(suc m) := n :: gen m;
gen : Nat → List Nat
| zero := nil
| n@(suc m) := n :: gen m;
sum : Nat → Nat;
sum n := foldl (+) 0 (gen n);
sum : Nat → Nat
| n := foldl (+) 0 (gen n);
sum' : Nat → Nat;
sum' n := foldr (+) 0 (gen n);
sum' : Nat → Nat
| n := foldr (+) 0 (gen n);
printListNatLn : List Nat → IO;
printListNatLn nil := printStringLn "nil";
printListNatLn (h :: t) := printNat h >> printString " :: " >> printListNatLn t;
printListNatLn : List Nat → IO
| nil := printStringLn "nil"
| (h :: t) :=
printNat h >> printString " :: " >> printListNatLn t;
main : IO;
main :=
printListNatLn (gen 10) >>
printListNatLn (reverse (gen 10)) >>
printListNatLn (filter ((<) 5) (gen 10)) >>
printListNatLn (reverse (map (flip sub 1) (gen 10))) >>
printNatLn (sum 10000) >>
printNatLn (sum' 10000);
main : IO :=
printListNatLn (gen 10)
>> printListNatLn (reverse (gen 10))
>> printListNatLn (filter ((<) 5) (gen 10))
>> printListNatLn (reverse (map (flip sub 1) (gen 10)))
>> printNatLn (sum 10000)
>> printNatLn (sum' 10000);
end;

30
tests/Compilation/positive/test023.juvix
View File

@ -1,24 +1,24 @@
-- mutual recursion
module test023;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
terminating
f : Nat → Nat;
f : Nat → Nat
| x := if (x < 1) 1 (2 * x + g (sub x 1));
terminating
g : Nat → Nat;
g : Nat → Nat
| x := if (x < 1) 1 (x + h (sub x 1));
terminating
h : Nat → Nat;
h : Nat → Nat
| x := if (x < 1) 1 (x * f (sub x 1));
f x := if (x < 1) 1 (2 * x + g (sub x 1));
g x := if (x < 1) 1 (x + h (sub x 1));
h x := if (x < 1) 1 (x * f (sub x 1));
main : IO :=
printNatLn (f 5)
>> printNatLn (f 10)
>> printNatLn (f 20);
main : IO;
main :=
printNatLn (f 5) >>
printNatLn (f 10) >>
printNatLn (f 20);
end;

67
tests/Compilation/positive/test024.juvix
View File

@ -1,43 +1,46 @@
-- nested binders with variable capture
module test024;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type Tree := leaf : Tree | node : Tree → Tree → Tree;
type Tree :=
| leaf : Tree
| node : Tree → Tree → Tree;
gen : Nat → Tree;
gen zero := leaf;
gen (suc zero) := node leaf leaf;
gen (suc (suc n')) := node (gen n') (gen (suc n'));
gen : Nat → Tree
| zero := leaf
| (suc zero) := node leaf leaf
| (suc (suc n')) := node (gen n') (gen (suc n'));
g : Tree → Tree;
g : Tree → Tree
| leaf := leaf
| (node l r) := if (isNode l) r (node r l);
terminating
f : Tree → Nat;
f leaf := 1;
f (node l' r') :=
let
l : Tree := g l';
r : Tree := g r';
terminating a : Nat :=
case l
| leaf := 1
| node l r := f l + f r;
terminating b : Nat :=
case r
| node l r := f l + f r
| _ := 2;
in
a * b;
f : Tree → Nat
| leaf := 1
| (node l' r') :=
let
l : Tree := g l';
r : Tree := g r';
terminating
a :
Nat :=
case l
| leaf := 1
| node l r := f l + f r;
terminating
b :
Nat :=
case r
| node l r := f l + f r
| _ := 2;
in a * b;
isNode : Tree → Bool;
isNode (node _ _) := true;
isNode leaf := false;
isNode : Tree → Bool
| (node _ _) := true
| leaf := false;
g leaf := leaf;
g (node l r) := if (isNode l) r (node r l);
main : IO := printNatLn (f (gen 10));
main : IO;
main := printNatLn (f (gen 10));
end;

27
tests/Compilation/positive/test025.juvix
View File

@ -1,23 +1,18 @@
-- Euclid's algorithm
module test025;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
terminating
gcd : Nat → Nat → Nat;
gcd a b := if (a > b)
(gcd b a)
(if (a == 0)
b
(gcd (mod b a) a));
gcd : Nat → Nat → Nat
| a b :=
if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
main : IO;
main :=
printNatLn (gcd (3 * 7 * 2) (7 * 2 * 11)) >>
printNatLn (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5)) >>
printNatLn (gcd 3 7) >>
printNatLn (gcd 7 3) >>
printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13));
main : IO :=
printNatLn (gcd (3 * 7 * 2) (7 * 2 * 11))
>> printNatLn (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5))
>> printNatLn (gcd 3 7)
>> printNatLn (gcd 7 3)
>> printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13));
end;

77
tests/Compilation/positive/test026.juvix
View File

@ -1,52 +1,59 @@
-- functional queues
module test026;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type Queue (A : Type) := queue : List A → List A → Queue A;
type Queue (A : Type) :=
| queue : List A → List A → Queue A;
qfst : {A : Type} → Queue A → List A;
qfst (queue x _) := x;
qfst : {A : Type} → Queue A → List A
| (queue x _) := x;
qsnd : {A : Type} → Queue A → List A;
qsnd (queue _ x) := x;
qsnd : {A : Type} → Queue A → List A
| (queue _ x) := x;
front : {A : Type} → Queue A → A;
front q := head (qfst q);
front : {A : Type} → Queue A → A
| q := head (qfst q);
pop_front : {A : Type} → Queue A → Queue A;
pop_front {A} q :=
let q' : Queue A := queue (tail (qfst q)) (qsnd q) in
case qfst q'
| nil := queue (reverse (qsnd q')) nil
| _ := q';
pop_front : {A : Type} → Queue A → Queue A
| {A} q :=
let
q' : Queue A := queue (tail (qfst q)) (qsnd q);
in case qfst q'
| nil := queue (reverse (qsnd q')) nil
| _ := q';
push_back : {A : Type} → Queue A → A → Queue A;
push_back q x := case qfst q
| nil := queue (x :: nil) (qsnd q)
| q' := queue q' (x :: qsnd q);
push_back : {A : Type} → Queue A → A → Queue A
| q x :=
case qfst q
| nil := queue (x :: nil) (qsnd q)
| q' := queue q' (x :: qsnd q);
is_empty : {A : Type} → Queue A → Bool;
is_empty q := case qfst q
| nil := (case qsnd q | nil := true | _ := false)
| _ := false;
is_empty : {A : Type} → Queue A → Bool
| q :=
case qfst q
| nil :=
(case qsnd q
| nil := true
| _ := false)
| _ := false;
empty : {A : Type} → Queue A;
empty := queue nil nil;
empty : {A : Type} → Queue A := queue nil nil;
terminating
g : List Nat → Queue Nat → List Nat;
g acc q := if (is_empty q) acc (g (front q :: acc) (pop_front q));
g : List Nat → Queue Nat → List Nat
| acc q :=
if (is_empty q) acc (g (front q :: acc) (pop_front q));
f : Nat → Queue Nat → List Nat;
f zero q := g nil q;
f n@(suc n') q := f n' (push_back q n);
f : Nat → Queue Nat → List Nat
| zero q := g nil q
| n@(suc n') q := f n' (push_back q n);
printListNatLn : List Nat → IO;
printListNatLn nil := printStringLn "nil";
printListNatLn (h :: t) := printNat h >> printString " :: " >> printListNatLn t;
printListNatLn : List Nat → IO
| nil := printStringLn "nil"
| (h :: t) :=
printNat h >> printString " :: " >> printListNatLn t;
main : IO;
main := printListNatLn (f 100 empty); -- list of numbers from 1 to 100
main : IO := printListNatLn (f 100 empty);
-- list of numbers from 1 to 100
end;

45
tests/Compilation/positive/test027.juvix
View File

@ -1,37 +1,34 @@
-- Church numerals
module test027;
open import Stdlib.Prelude hiding {toNat};
import Stdlib.Prelude open hiding {toNat};
Num : Type;
Num := {A : Type} → (A → A) → A → A;
Num : Type := {A : Type} → (A → A) → A → A;
czero : Num;
czero {_} f x := x;
czero : Num
| {_} f x := x;
csuc : Num → Num;
csuc n {_} f := f ∘ n {_} f;
csuc : Num → Num
| n {_} f := f ∘ n {_} f;
num : Nat → Num;
num zero := czero;
num (suc n) := csuc (num n);
num : Nat → Num
| zero := czero
| (suc n) := csuc (num n);
add : Num → Num → Num;
add n m {_} f := n {_} f ∘ m {_} f;
add : Num → Num → Num
| n m {_} f := n {_} f ∘ m {_} f;
mul : Num → Num → Num;
mul n m {_} := n {_} ∘ m {_};
mul : Num → Num → Num
| n m {_} := n {_} ∘ m {_};
isZero : Num → Bool;
isZero n := n {_} (const false) true;
isZero : Num → Bool
| n := n {_} (const false) true;
toNat : Num → Nat;
toNat n := n {_} ((+) 1) 0;
toNat : Num → Nat
| n := n {_} ((+) 1) 0;
main : IO;
main :=
printNatLn (toNat (num 7)) >>
printNatLn (toNat (add (num 7) (num 3))) >>
printNatLn (toNat (mul (num 7) (num 3)));
main : IO :=
printNatLn (toNat (num 7))
>> printNatLn (toNat (add (num 7) (num 3)))
>> printNatLn (toNat (mul (num 7) (num 3)));
end;

64
tests/Compilation/positive/test028.juvix
View File

@ -1,49 +1,51 @@
-- streams without memoization
module test028;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
type Stream := cons : Nat → (Unit → Stream) → Stream;
type Stream :=
| cons : Nat → (Unit → Stream) → Stream;
force : (Unit → Stream) → Stream;
force f := f unit;
force : (Unit → Stream) → Stream
| f := f unit;
terminating
sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream;
sfilter p s unit := case force s
| cons h t := if (p h) (cons h (sfilter p t)) (force (sfilter p t));
sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
| p s unit :=
case force s
| cons h t :=
if (p h) (cons h (sfilter p t)) (force (sfilter p t));
shead : Stream → Nat;
shead (cons h _) := h;
shead : Stream → Nat
| (cons h _) := h;
stail : Stream → Unit → Stream;
stail (cons _ t) := t;
stail : Stream → Unit → Stream
| (cons _ t) := t;
snth : Nat → (Unit → Stream) → Nat;
snth zero s := shead (force s);
snth (suc n) s := snth n (stail (force s));
snth : Nat → (Unit → Stream) → Nat
| zero s := shead (force s)
| (suc n) s := snth n (stail (force s));
terminating
numbers : Nat → Unit → Stream;
numbers n unit := cons n (numbers (suc n));
numbers : Nat → Unit → Stream
| n unit := cons n (numbers (suc n));
indivisible : Nat → Nat → Bool;
indivisible n x := not (mod x n == 0);
indivisible : Nat → Nat → Bool
| n x := not (mod x n == 0);
terminating
eratostenes : (Unit → Stream) → Unit → Stream;
eratostenes s unit := case force s
| cons n t := cons n (eratostenes (sfilter (indivisible n) t));
eratostenes : (Unit → Stream) → Unit → Stream
| s unit :=
case force s
| cons n t :=
cons n (eratostenes (sfilter (indivisible n) t));
primes : Unit → Stream;
primes := eratostenes (numbers 2);
primes : Unit → Stream := eratostenes (numbers 2);
main : IO;
main :=
printNatLn (snth 10 primes) >>
printNatLn (snth 50 primes) >>
printNatLn (snth 100 primes) >>
printNatLn (snth 200 primes);
main : IO :=
printNatLn (snth 10 primes)
>> printNatLn (snth 50 primes)
>> printNatLn (snth 100 primes)
>> printNatLn (snth 200 primes);
end;

26
tests/Compilation/positive/test029.juvix
View File

@ -1,20 +1,18 @@
-- Ackermann function
module test029;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
ack : Nat → Nat → Nat;
ack zero n := n + 1;
ack (suc m) zero := ack m 1;
ack (suc m) (suc n) := ack m (ack (suc m) n);
ack : Nat → Nat → Nat
| zero n := n + 1
| (suc m) zero := ack m 1
| (suc m) (suc n) := ack m (ack (suc m) n);
main : IO;
main :=
printNatLn (ack 0 7) >>
printNatLn (ack 1 7) >>
printNatLn (ack 1 13) >>
printNatLn (ack 2 7) >>
printNatLn (ack 2 13) >>
printNatLn (ack 3 7);
main : IO :=
printNatLn (ack 0 7)
>> printNatLn (ack 1 7)
>> printNatLn (ack 1 13)
>> printNatLn (ack 2 7)
>> printNatLn (ack 2 13)
>> printNatLn (ack 3 7);
end;

39
tests/Compilation/positive/test030.juvix
View File

@ -1,31 +1,28 @@
-- Ackermann function (higher-order definition)
module test030;
open import Stdlib.Prelude hiding {iterate};
import Stdlib.Prelude open hiding {iterate};
iterate : {A : Type} → (A → A) → Nat → A → A;
-- clauses with differing number of patterns not yet supported
-- iterate f zero x := x;
iterate f zero := id;
iterate f (suc n) := f ∘ (iterate f n);
iterate : {A : Type} → (A → A) → Nat → A → A
-- clauses with differing number of patterns not yet supported
-- iterate f zero x := x;
| f zero := id
| f (suc n) := f ∘ iterate f n;
plus : Nat → Nat → Nat;
plus := iterate suc;
plus : Nat → Nat → Nat := iterate suc;
mult : Nat → Nat → Nat;
mult m n := iterate (plus n) m 0;
mult : Nat → Nat → Nat
| m n := iterate (plus n) m 0;
exp : Nat → Nat → Nat;
exp m n := iterate (mult m) n 1;
exp : Nat → Nat → Nat
| m n := iterate (mult m) n 1;
ackermann : Nat → Nat → Nat;
ackermann m := iterate (λ{f n := iterate f (suc n) 1}) m suc;
ackermann : Nat → Nat → Nat
| m := iterate λ {f n := iterate f (suc n) 1} m suc;
main : IO;
main :=
printNatLn (plus 3 7) >>
printNatLn (mult 3 7) >>
printNatLn (exp 3 7) >>
printNatLn (ackermann 3 7);
main : IO :=
printNatLn (plus 3 7)
>> printNatLn (mult 3 7)
>> printNatLn (exp 3 7)
>> printNatLn (ackermann 3 7);
end;

27
tests/Compilation/positive/test031.juvix
View File

@ -1,22 +1,19 @@
-- nested lists
module test031;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
mklst : Nat → List Nat;
mklst zero := nil;
mklst (suc n) := suc n :: mklst n;
mklst : Nat → List Nat
| zero := nil
| (suc n) := suc n :: mklst n;
mklst2 : Nat → List (List Nat);
mklst2 zero := nil;
mklst2 (suc n) := mklst (suc n) :: mklst2 n;
mklst2 : Nat → List (List Nat)
| zero := nil
| (suc n) := mklst (suc n) :: mklst2 n;
printListNatLn : List Nat → IO;
printListNatLn nil := printStringLn "nil";
printListNatLn (x :: xs) := printNat x >> printString " :: " >> printListNatLn xs;
printListNatLn : List Nat → IO
| nil := printStringLn "nil"
| (x :: xs) :=
printNat x >> printString " :: " >> printListNatLn xs;
main : IO;
main :=
printListNatLn (flatten (mklst2 4));
end;
main : IO := printListNatLn (flatten (mklst2 4));

83
tests/Compilation/positive/test032.juvix
View File

@ -1,53 +1,60 @@
-- merge sort
module test032;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
split : {A : Type} → Nat → List A → List A × List A;
split zero xs := (nil, xs);
split (suc n) nil := (nil, nil);
split (suc n) (x :: xs) := case split n xs
| l1, l2 := (x :: l1, l2);
split : {A : Type} → Nat → List A → List A × List A
| zero xs := nil, xs
| (suc n) nil := nil, nil
| (suc n) (x :: xs) :=
case split n xs
| l1, l2 := x :: l1, l2;
terminating
merge' : List Nat → List Nat → List Nat;
merge' nil ys := ys;
merge' xs nil := xs;
merge' xs@(x :: xs') ys@(y :: ys') := if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
merge' : List Nat → List Nat → List Nat
| nil ys := ys
| xs nil := xs
| xs@(x :: xs') ys@(y :: ys') :=
if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
terminating
sort : List Nat → List Nat;
sort xs :=
let n : Nat; n := length xs in
if (n <= 1)
xs
(case split (div n 2) xs
| l1, l2 := merge' (sort l1) (sort l2)
);
sort : List Nat → List Nat
| xs :=
let
n : Nat := length xs;
in if
(n <= 1)
xs
(case split (div n 2) xs
| l1, l2 := merge' (sort l1) (sort l2));
terminating
uniq : List Nat → List Nat;
uniq nil := nil;
uniq (x :: nil) := x :: nil;
uniq (x :: xs@(x' :: _)) := if (x == x') (uniq xs) (x :: uniq xs);
uniq : List Nat → List Nat
| nil := nil
| (x :: nil) := x :: nil
| (x :: xs@(x' :: _)) :=
if (x == x') (uniq xs) (x :: uniq xs);
gen : List Nat → Nat → (Nat → Nat) → List Nat;
gen acc zero f := acc;
gen acc (suc n) f := gen (f (suc n) :: acc) n f;
gen : List Nat → Nat → (Nat → Nat) → List Nat
| acc zero f := acc
| acc (suc n) f := gen (f (suc n) :: acc) n f;
gen2 : List (List Nat) → Nat → Nat → List (List Nat);
gen2 acc m zero := acc;
gen2 acc m (suc n) := gen2 (gen nil m ((+) (suc n)) :: acc) m n;
gen2 : List (List Nat) → Nat → Nat → List (List Nat)
| acc m zero := acc
| acc m (suc n) :=
gen2 (gen nil m ((+) (suc n)) :: acc) m n;
printListNatLn : List Nat → IO;
printListNatLn nil := printStringLn "nil";
printListNatLn (x :: xs) := printNat x >> printString " :: " >> printListNatLn xs;
printListNatLn : List Nat → IO
| nil := printStringLn "nil"
| (x :: xs) :=
printNat x >> printString " :: " >> printListNatLn xs;
main : IO;
main :=
printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 40))))) >>
printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 9 80))))) >>
printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 80)))));
main : IO :=
printListNatLn
(take 10 (uniq (sort (flatten (gen2 nil 6 40)))))
>> printListNatLn
(take 10 (uniq (sort (flatten (gen2 nil 9 80)))))
>> printListNatLn
(take 10 (uniq (sort (flatten (gen2 nil 6 80)))));
end;

53
tests/Compilation/positive/test033.juvix
View File

@ -1,38 +1,41 @@
-- eta-expansion of builtins and constructors
module test033;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
f : (Nat → Nat) → Nat;
f g := g 2;
f : (Nat → Nat) → Nat
| g := g 2;
f' : Nat → Nat;
f' x := f ((+) x);
f' : Nat → Nat
| x := f ((+) x);
g : (Nat → Nat × Nat) → Nat × Nat;
g f := f 2;
g : (Nat → Nat × Nat) → Nat × Nat
| f := f 2;
g' : Nat → Nat × Nat;
g' x := g ((,) x);
g' : Nat → Nat × Nat
| x := g ((,) x);
f1' : Nat → Nat → Nat;
f1' x y := f ((+) (div x y));
f1' : Nat → Nat → Nat
| x y := f ((+) (div x y));
g1' : Nat → Nat → Nat × Nat;
g1' x y := g ((,) (div x y));
g1' : Nat → Nat → Nat × Nat
| x y := g ((,) (div x y));
h : (Nat → Nat → Nat × Nat) → Nat × Nat;
h f := f 1 2;
h : (Nat → Nat → Nat × Nat) → Nat × Nat
| f := f 1 2;
printPairNatLn : Nat × Nat → IO;
printPairNatLn (x, y) := printString "(" >> printNat x >> printString ", " >> printNat y >> printStringLn ")";
printPairNatLn : Nat × Nat → IO
| (x, y) :=
printString "("
>> printNat x
>> printString ", "
>> printNat y
>> printStringLn ")";
main : IO;
main :=
printNatLn (f' 7) >>
printPairNatLn (g' 7) >>
printNatLn (f1' 7 2) >>
printPairNatLn (g1' 7 2) >>
printPairNatLn (h (,));
main : IO :=
printNatLn (f' 7)
>> printPairNatLn (g' 7)
>> printNatLn (f1' 7 2)
>> printPairNatLn (g1' 7 2)
>> printPairNatLn (h (,));
end;

46
tests/Compilation/positive/test034.juvix
View File

@ -1,33 +1,29 @@
-- recursive let
module test034;
open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;
sum : Nat → Nat;
sum := let
sum' : Nat → Nat;
sum' := λ {
zero := zero
| (suc n) := suc n + sum' n
};
in sum';
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
mutrec : IO;
mutrec := let
terminating
f : Nat → Nat;
terminating
g : Nat → Nat;
terminating
h : Nat → Nat;
f x := if (x < 1) 1 (g (sub x 1) + 2 * x);
g x := if (x < 1) 1 (x + h (sub x 1));
h x := if (x < 1) 1 (x * f (sub x 1));
in printNatLn (f 5)
sum : Nat → Nat :=
let
sum' : Nat → Nat :=
λ {
zero := zero
| (suc n) := suc n + sum' n
};
in sum';
mutrec : IO :=
let
terminating
f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
terminating
g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
terminating
h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
in printNatLn (f 5)
>> printNatLn (f 10)
>> printNatLn (g 5)
>> printNatLn (h 5);
main : IO;
main := printNatLn (sum 10000) >> mutrec;
end;
main : IO := printNatLn (sum 10000) >> mutrec;

87
tests/Compilation/positive/test035.juvix
View File

@ -1,59 +1,58 @@
-- pattern matching
module test035;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
lgen : Nat → List Nat;
lgen zero := nil;
lgen (suc n) := suc n :: lgen n;
lgen : Nat → List Nat
| zero := nil
| (suc n) := suc n :: lgen n;
sum2 : List Nat → List Nat;
sum2 (x :: (y :: xs)) := x + y :: sum2 (y :: xs);
sum2 xs := xs;
sum2 : List Nat → List Nat
| (x :: y :: xs) := x + y :: sum2 (y :: xs)
| xs := xs;
type Tree :=
leaf : Tree
| node : Tree -> Tree -> Tree;
| leaf : Tree
| node : Tree -> Tree -> Tree;
gen : Nat → Tree;
gen zero := leaf;
gen (suc zero) := node leaf leaf;
gen (suc (suc n)) := node (gen n) (gen (suc n));
g : Tree → Tree;
gen : Nat → Tree
| zero := leaf
| (suc zero) := node leaf leaf
| (suc (suc n)) := node (gen n) (gen (suc n));
terminating
f : Tree → Nat;
f leaf := 1;
f (node l r) :=
case g l, g r
| (leaf, leaf) := 3
| (node l r, leaf) := mod ((f l + f r) * 2) 20000
| (node l1 r1, node l2 r2) := mod ((f l1 + f r1) * (f l2 + f r2)) 20000
| (_, node l r) := mod (f l + f r) 20000;
f : Tree → Nat
| leaf := 1
| (node l r) :=
case g l, g r
| leaf, leaf := 3
| node l r, leaf := mod ((f l + f r) * 2) 20000
| node l1 r1, node l2 r2 :=
mod ((f l1 + f r1) * (f l2 + f r2)) 20000
| _, node l r := mod (f l + f r) 20000;
g leaf := leaf;
g (node (node _ _) r) := r;
g (node l r) := node r l;
g : Tree → Tree
| leaf := leaf
| (node (node _ _) r) := r
| (node l r) := node r l;
h : Nat -> Nat;
h (suc (suc (suc (suc n)))) := n;
h _ := 0;
h : Nat -> Nat
| (suc (suc (suc (suc n)))) := n
| _ := 0;
printListNatLn : List Nat → IO;
printListNatLn nil := printStringLn "nil";
printListNatLn (x :: xs) := printNat x >> printString " :: " >> printListNatLn xs;
printListNatLn : List Nat → IO
| nil := printStringLn "nil"
| (x :: xs) :=
printNat x >> printString " :: " >> printListNatLn xs;
main : IO;
main :=
printListNatLn (sum2 (lgen 5)) >>
printNatLn (f (gen 10)) >>
printNatLn (f (gen 15)) >>
printNatLn (f (gen 16)) >>
printNatLn (f (gen 17)) >>
printNatLn (f (gen 18)) >>
printNatLn (f (gen 20)) >>
printNatLn (h 5) >>
printNatLn (h 3);
main : IO :=
printListNatLn (sum2 (lgen 5))
>> printNatLn (f (gen 10))
>> printNatLn (f (gen 15))
>> printNatLn (f (gen 16))
>> printNatLn (f (gen 17))
>> printNatLn (f (gen 18))
>> printNatLn (f (gen 20))
>> printNatLn (h 5)
>> printNatLn (h 3);
end;

30
tests/Compilation/positive/test036.juvix
View File

@ -1,30 +1,24 @@
-- eta-expansion
module test036;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
expand : {A : Type} → A → Nat → A;
expand f x := f;
expand : {A : Type} → A → Nat → A
| f x := f;
f : Nat → Nat;
f := suc;
f : Nat → Nat := suc;
g : Nat → Nat → Nat;
g z := f ∘ (flip sub z);
g : Nat → Nat → Nat
| z := f ∘ flip sub z;
g' : Nat → Nat → Nat;
g' z := f ∘ (λ{x := sub x z});
g' : Nat → Nat → Nat
| z := f ∘ λ {x := sub x z};
h : Nat → Nat;
h := f ∘ g 3;
h : Nat → Nat := f ∘ g 3;
j : Nat → Nat → Nat;
j := g';
j : Nat → Nat → Nat := g';
k : Nat → Nat → Nat → Nat;
k := expand j;
k : Nat → Nat → Nat → Nat := expand j;
main : IO;
main := printNatLn (h 13 + j 2 3 + k 9 4 7);
main : IO := printNatLn (h 13 + j 2 3 + k 9 4 7);
end;

28
tests/Compilation/positive/test037.juvix
View File

@ -1,21 +1,21 @@
-- Applications with lets and cases in function position
module test037;
open import Stdlib.Prelude;
f : List ((Nat → Nat) → Nat → Nat) → Nat;
f l := (case l
| x :: _ := x
| nil := id)
import Stdlib.Prelude open;
f (l : List ((Nat → Nat) → Nat → Nat)) : Nat :=
(case l
| x :: _ := x
| nil := id)
(let
y : Nat → Nat;
y := id;
in (let
z : (Nat → Nat) → Nat → Nat;
z := id;
in (case l | _ :: _ := id | _ := id) z)
y : Nat → Nat := id;
in (let
z : (Nat → Nat) → Nat → Nat := id;
in (case l
| _ :: _ := id
| _ := id)
z)
y)
7;
main : IO;
main := printNatLn (f (λ {| x y := x y + 2 } :: nil));
end;
main : IO := printNatLn (f (λ {| x y := x y + 2} :: nil));

11
tests/Compilation/positive/test038.juvix
View File

@ -1,9 +1,12 @@
-- Simple case expression
module test038;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main := printNatLn (case 1, 2 | suc _, zero := 0 | suc _, suc x := x | _ := 19);
main : IO :=
printNatLn
(case 1, 2
| suc _, zero := 0
| suc _, suc x := x
| _ := 19);
end;

26
tests/Compilation/positive/test039.juvix
View File

@ -1,22 +1,18 @@
-- Mutually recursive let expressions
module test039;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main :=
main : IO :=
let
Ty : Type;
Ty := Nat;
odd : _;
even : _;
unused : _;
odd zero := false;
odd (suc n) := not (even n);
unused := 123;
even zero := true;
even (suc n) := not (odd n);
plusOne : Ty → Ty;
plusOne n := n + 1;
Ty : Type := Nat;
odd : _
| zero := false
| (suc n) := not (even n);
unused : _ := 123;
even : _
| zero := true
| (suc n) := not (odd n);
plusOne (n : Ty) : Ty := n + 1;
in printBoolLn (odd (plusOne 13))
>> printBoolLn (even (plusOne 12));

11
tests/Compilation/positive/test040.juvix
View File

@ -1,8 +1,8 @@
-- pattern matching nullary constructor
module test040;
open import Stdlib.System.IO;
open import Stdlib.Data.Bool;
import Stdlib.System.IO open;
import Stdlib.Data.Bool open;
type Unit :=
| unit : Unit;
@ -10,8 +10,7 @@ type Unit :=
type Foo (A : Type) :=
| foo : Unit -> A -> Foo A;
f : {A : Type} -> Foo A -> A;
f (foo unit a) := a;
f : {A : Type} -> Foo A -> A
| (foo unit a) := a;
main : IO;
main := printBoolLn (f (foo unit true));
main : IO := printBoolLn (f (foo unit true));

9
tests/Compilation/positive/test041.juvix
View File

@ -1,13 +1,12 @@
-- Use a builtin inductive in an inductive constructor
module test041;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type BoxedString :=
| boxed : String -> BoxedString;
printBoxedString : BoxedString -> IO;
printBoxedString (boxed s) := printStringLn s;
printBoxedString : BoxedString -> IO
| (boxed s) := printStringLn s;
main : IO;
main := printBoxedString (boxed "abc");
main : IO := printBoxedString (boxed "abc");

15
tests/Compilation/positive/test042.juvix
View File

@ -1,17 +1,20 @@
-- builtin string-to-nat
module test042;
builtin bool type Bool :=
builtin bool
type Bool :=
| true : Bool
| false : Bool;
builtin string axiom String : Type;
builtin string
axiom String : Type;
builtin nat type Nat :=
builtin nat
type Nat :=
| zero : Nat
| suc : Nat → Nat;
builtin string-to-nat axiom stringToNat : String -> Nat;
builtin string-to-nat
axiom stringToNat : String -> Nat;
main : Nat;
main := stringToNat "1";
main : Nat := stringToNat "1";

19
tests/Compilation/positive/test043.juvix
View File

@ -1,20 +1,21 @@
-- builtin trace
module test043;
builtin nat type Nat :=
builtin nat
type Nat :=
| zero : Nat
| suc : Nat → Nat;
builtin string axiom String : Type;
builtin string
axiom String : Type;
builtin trace axiom trace : {A : Type} → A → A;
builtin trace
axiom trace : {A : Type} → A → A;
builtin seq
seq : {A B : Type} → A → B → B;
seq x y := y;
seq : {A B : Type} → A → B → B
| x y := y;
f : Nat;
f := seq (trace "a") 1;
f : Nat := seq (trace "a") 1;
main : Nat;
main := f;
main : Nat := f;

18
tests/Compilation/positive/test044.juvix
View File

@ -1,10 +1,16 @@
-- Builtin readline
module test044;
builtin string axiom String : Type;
builtin IO axiom IO : Type;
builtin IO-readline axiom readLn : (String → IO) → IO;
builtin string-print axiom printString : String → IO;
builtin string
axiom String : Type;
main : IO;
main := readLn printString;
builtin IO
axiom IO : Type;
builtin IO-readline
axiom readLn : (String → IO) → IO;
builtin string-print
axiom printString : String → IO;
main : IO := readLn printString;

23
tests/Compilation/positive/test045.juvix
View File

@ -2,17 +2,18 @@
-- Builtin nat requires builtin bool when translated to integers, because
-- matching is translated to comparison operators and cases on booleans.
module test045;
builtin nat type Nat :=
| zero : Nat
| suc : Nat → Nat;
syntax fixity additive {arity: binary, assoc: left};
builtin nat
type Nat :=
| zero : Nat
| suc : Nat → Nat;
syntax operator + additive;
+ : Nat → Nat → Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
syntax fixity additive {arity: binary, assoc: left};
main : Nat;
main := 1 + 3;
end;
syntax operator + additive;
+ : Nat → Nat → Nat
| zero b := b
| (suc a) b := suc (a + b);
main : Nat := 1 + 3;

16
tests/Compilation/positive/test046.juvix
View File

@ -1,18 +1,14 @@
-- polymorphic type arguments
module test046;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
Ty : Type;
Ty := {B : Type} -> B -> B;
Ty : Type := {B : Type} -> B -> B;
id' : Ty;
id' {_} x := x;
id' : Ty
| {_} x := x;
fun : {A : Type} → A → Ty;
fun := id (λ{_ := id'});
fun : {A : Type} → A → Ty := id λ {_ := id'};
main : Nat;
main := fun 5 {Nat} 7;
main : Nat := fun 5 {Nat} 7;
end;

26
tests/Compilation/positive/test047.juvix
View File

@ -1,30 +1,25 @@
-- local modules
module test047;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
module Local;
t : Nat;
t := 2;
t : Nat := 2;
module Nested;
t : Nat;
t := 3;
t : Nat := 3;
-- module shadowing
module Nested;
t : Nat;
t := 5;
t : Nat := 5;
end;
module Nested2;
t : Nat;
t := 7;
t : Nat := 7;
-- module shadowing
module Nested;
t : Nat;
t := 11;
t : Nat := 11;
end;
end;
end;
@ -36,16 +31,13 @@ module Public;
open Nested public;
end;
tt : Nat;
tt := t;
tt : Nat := t;
x : Nat;
x :=
x : Nat :=
t
* Local.t
* Local.Nested.t
* Nested.Nested2.Nested.t
* Public.Nested.t;
main : IO;
main := printNatLn x;
main : IO := printNatLn x;

5
tests/Compilation/positive/test048.juvix
View File

@ -1,7 +1,6 @@
-- String quoting
module test048;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : String;
main := "hello!\n\b\t\r";
main : String := "hello!\n\b\t\r";

82
tests/Compilation/positive/test049.juvix
View File

@ -1,43 +1,49 @@
-- Builtin Int
module test049;
open import Stdlib.Prelude hiding {+;*;div;mod};
open import Stdlib.Data.Int.Ord;
open import Stdlib.Data.Int;
import Stdlib.Prelude open hiding {+; *; div; mod};
import Stdlib.Data.Int.Ord open;
import Stdlib.Data.Int open;
f : Int -> Nat;
f (negSuc n) := n;
f (ofNat n) := n;
f : Int -> Nat
| (negSuc n) := n
| (ofNat n) := n;
main : IO;
main := printStringLn (intToString 1)
>> printStringLn (intToString -1)
>> printIntLn (ofNat 1)
>> printIntLn (negSuc 0)
>> printIntLn (ofNat (suc zero))
>> printIntLn (negSuc zero)
>> printStringLn (natToString (f 1))
>> printNatLn (f (-1))
>> printNatLn (f (ofNat (suc zero)))
>> printNatLn (f (negSuc (suc zero)))
>> printBoolLn (-1 == -2)
>> printBoolLn (-1 == -1)
>> printBoolLn (1 == 1)
>> printBoolLn (-1 == 1)
>> printIntLn (-1 + 1)
>> printIntLn (negNat (suc zero))
>> printIntLn (let g : Nat -> Int := negNat in g (suc zero))
>> printIntLn (neg -1)
>> printIntLn (let g : Int -> Int := neg in g -1)
>> printIntLn (-2 * 2)
>> printIntLn (div 4 -2)
>> printIntLn (2 - 2)
>> printBoolLn (nonNeg 0)
>> printBoolLn (nonNeg -1)
>> printIntLn (mod -5 -2)
>> printBoolLn (0 < 0)
>> printBoolLn (0 <= 0)
>> printBoolLn (0 < 1)
>> printBoolLn (1 <= 0)
>> printIntLn (mod 5 -3)
>> printIntLn (div 5 -3);
main : IO :=
printStringLn (intToString 1)
>> printStringLn (intToString -1)
>> printIntLn (ofNat 1)
>> printIntLn (negSuc 0)
>> printIntLn (ofNat (suc zero))
>> printIntLn (negSuc zero)
>> printStringLn (natToString (f 1))
>> printNatLn (f -1)
>> printNatLn (f (ofNat (suc zero)))
>> printNatLn (f (negSuc (suc zero)))
>> printBoolLn (-1 == -2)
>> printBoolLn (-1 == -1)
>> printBoolLn (1 == 1)
>> printBoolLn (-1 == 1)
>> printIntLn (-1 + 1)
>> printIntLn (negNat (suc zero))
>> printIntLn
(let
g : Nat -> Int := negNat;
in g (suc zero))
>> printIntLn (neg -1)
>> printIntLn
(let
g : Int -> Int := neg;
in g -1)
>> printIntLn (-2 * 2)
>> printIntLn (div 4 -2)
>> printIntLn (2 - 2)
>> printBoolLn (nonNeg 0)
>> printBoolLn (nonNeg -1)
>> printIntLn (mod -5 -2)
>> printBoolLn (0 < 0)
>> printBoolLn (0 <= 0)
>> printBoolLn (0 < 1)
>> printBoolLn (1 <= 0)
>> printIntLn (mod 5 -3)
>> printIntLn (div 5 -3);

17
tests/Compilation/positive/test050.juvix
View File

@ -1,14 +1,13 @@
-- Pattern matching with integers
module test050;
open import Stdlib.Prelude hiding {+;*;div;mod};
open import Stdlib.Data.Int.Ord;
open import Stdlib.Data.Int;
import Stdlib.Prelude open hiding {+; *; div; mod};
import Stdlib.Data.Int.Ord open;
import Stdlib.Data.Int open;
f : Int -> Int;
f (negSuc zero) := ofNat 0;
f (negSuc m@(suc n)) := ofNat n + ofNat m;
f (ofNat n) := neg (ofNat n - 7);
f : Int -> Int
| (negSuc zero) := ofNat 0
| (negSuc m@(suc n)) := ofNat n + ofNat m
| (ofNat n) := neg (ofNat n - 7);
main : Int;
main := f -10 - f 1 + f -1;
main : Int := f -10 - f 1 + f -1;

11
tests/Compilation/positive/test051.juvix
View File

@ -1,12 +1,11 @@
-- local recursive function using IO >>
module test051;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : IO;
main :=
main : IO :=
let
f : Nat -> IO;
f zero := printStringLn "";
f (suc n) := printString "*" >> f n;
f : Nat -> IO
| zero := printStringLn ""
| (suc n) := printString "*" >> f n;
in f 3;

209
tests/Compilation/positive/test052.juvix
View File

@ -1,18 +1,18 @@
--- Simple lambda calculus
module test052;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
import Stdlib.Trait.Show as Show;
fromShow : {a : Type} -> Show a -> a -> String;
fromShow (mkShow s) a := s a;
fromShow : {a : Type} -> Show a -> a -> String
| (mkShow s) a := s a;
LambdaTy : Type -> Type;
LambdaTy : Type -> Type := Lambda';
AppTy : Type -> Type;
AppTy : Type -> Type := App';
syntax operator :+: additive;
--- An ;Expr'; is an expression in our language.
type Expr' (v : Type) :=
| ! : v -> Expr' v
@ -29,20 +29,13 @@ type Lambda' (v : Type) :=
type App' (v : Type) :=
| mkApp : Expr' v -> Expr' v -> App' v;
LambdaTy := Lambda';
Expr : Type := Expr' Nat;
AppTy := App';
Lambda : Type := Lambda' Nat;
Expr : Type;
Expr := Expr' Nat;
App : Type := App' Nat;
Lambda : Type;
Lambda := Lambda' Nat;
App : Type;
App := App' Nat;
ValTy : Type -> Type;
ValTy : Type -> Type := Val';
--- A ;Closure'; is a context (;List; of ;ValTy;) and an ;Expr'; in that context.
type Closure' (v : Type) :=
@ -53,13 +46,9 @@ type Val' (v : Type) :=
| vnum : Nat -> Val' v
| closure : Closure' v -> Val' v;
ValTy := Val';
Val : Type := Val' Nat;
Val : Type;
Val := Val' Nat;
Closure : Type;
Closure := Closure' Nat;
Closure : Type := Closure' Nat;
--- Sum type.
type Either (a : Type) (b : Type) :=
@ -67,54 +56,50 @@ type Either (a : Type) (b : Type) :=
| right : b -> Either a b;
module ExprTraits;
toString : Expr -> String;
toString (! v) := "[" ++str natToString v ++str "]";
toString (lam (mkLambda b)) :=
"\955 {" ++str toString b ++str "}";
toString (app (mkApp l r)) :=
"("
++str toString l
++str " # "
++str toString r
++str ")";
toString (l :+: r) :=
"("
++str toString l
++str " + "
++str toString r
++str ")";
toString (num n) := natToString n;
toString : Expr -> String
| (! v) := "[" ++str natToString v ++str "]"
| (lam (mkLambda b)) := "λ {" ++str toString b ++str "}"
| (app (mkApp l r)) :=
"("
++str toString l
++str " # "
++str toString r
++str ")"
| (l :+: r) :=
"("
++str toString l
++str " + "
++str toString r
++str ")"
| (num n) := natToString n;
--- ;Show; instance for ;Expr;.
Show : Show.Show Expr;
Show := mkShow toString;
Show : Show.Show Expr := mkShow toString;
end;
module ValTraits;
terminating
valToString : Val -> String;
valToString : Val -> String
| (vnum n) := natToString n
| (closure (mkClosure ctx n)) :=
fromShow (ListTraits.Show Show) ctx
++str " ⊢ "
++str ExprTraits.toString n;
--- ;Show; instance for ;Val;.
terminating
Show : Show.Show Val;
Show := mkShow valToString;
valToString (vnum n) := natToString n;
valToString (closure (mkClosure ctx n)) :=
fromShow (ListTraits.Show Show) ctx
++str " \8866 "
++str ExprTraits.toString n;
Show : Show.Show Val := mkShow valToString;
end;
syntax operator >>= seq;
--- Monadic binding for ;Either;.
>>= :
{e a b : Type}
>>=
: {e a b : Type}
-> Either e a
-> (a -> Either e b)
-> Either e b;
>>= (left e) _ := left e;
>>= (right a) f := f a;
-> Either e b
| (left e) _ := left e
| (right a) f := f a;
--- An evaluation error.
type Error :=
@ -126,96 +111,82 @@ type Error :=
ExpectedLambda : Error;
--- Returns the first item of a ;List;, if it exists.
headMay : {a : Type} -> List a -> Maybe a;
headMay nil := nothing;
headMay (x :: _) := just x;
headMay : {a : Type} -> List a -> Maybe a
| nil := nothing
| (x :: _) := just x;
--- ;List; indexing.
index : {a : Type} -> List a -> Nat -> Maybe a;
index l n := headMay (drop n l);
index : {a : Type} -> List a -> Nat -> Maybe a
| l n := headMay (drop n l);
--- Get a ;Nat; from a ;Val; or return an ;Error;.
getNat : Val -> Either Error Nat;
getNat (vnum n) := right n;
getNat e := left (ExpectedNat e);
getNat : Val -> Either Error Nat
| (vnum n) := right n
| e := left (ExpectedNat e);
--- Evaluates an ;Expr; and returns a ;Val;.
--- If an error occurs during evaluation, returns ;Error;.
eval : Expr -> Either Error Val;
eval topExpr :=
let
getClosure : Val -> Either Error Closure;
getClosure (closure l) := right l;
getClosure _ := left ExpectedLambda;
terminating
go : List Val -> Expr -> Either Error Val;
go ctx (! v) :=
maybe (left (ScopeError v ctx)) right (index ctx v);
go ctx (app (mkApp fun x)) :=
let
terminating
applyClosure : Closure -> Either Error Val;
applyClosure (mkClosure closCtx body) :=
go ctx x
>>= λ {
| x' := go (x' :: closCtx) body
};
in go ctx fun >>= getClosure >>= applyClosure;
go ctx (lam (mkLambda body)) :=
right (closure (mkClosure ctx body));
go _ (num n) := right (vnum n);
go ctx (l :+: r) :=
go ctx l
>>= getNat
>>= λ {
| l' :=
go ctx r
>>= getNat
>>= λ {
| r' := right (vnum (l' + r'))
}
};
in go nil topExpr;
eval : Expr -> Either Error Val
| topExpr :=
let
getClosure : Val -> Either Error Closure
| (closure l) := right l
| _ := left ExpectedLambda;
terminating
go : List Val -> Expr -> Either Error Val
| ctx (! v) :=
maybe (left (ScopeError v ctx)) right (index ctx v)
| ctx (app (mkApp fun x)) :=
let
terminating
applyClosure : Closure -> Either Error Val
| (mkClosure closCtx body) :=
go ctx x >>= λ {| x' := go (x' :: closCtx) body};
in go ctx fun >>= getClosure >>= applyClosure
| ctx (lam (mkLambda body)) :=
right (closure (mkClosure ctx body))
| _ (num n) := right (vnum n)
| ctx (l :+: r) :=
go ctx l
>>= getNat
>>= λ {| l' :=
go ctx r
>>= getNat
>>= λ {| r' := right (vnum (l' + r'))}};
in go nil topExpr;
--- Evaluate an ;Expr; and try to extract a ;Nat;.
terminating
evalNat : Expr -> Either Error Nat;
evalNat topExpr := eval topExpr >>= getNat;
evalNat : Expr -> Either Error Nat
| topExpr := eval topExpr >>= getNat;
--- Syntactical helper for creating a ;lam;.
Λ : Expr -> Expr;
Λ body := lam (mkLambda body);
Λ : Expr -> Expr
| body := lam (mkLambda body);
syntax fixity app {arity: binary, assoc: left, above: [composition]};
syntax operator # app;
--- Syntactical helper for creating an ;app;.
# : Expr -> Expr -> Expr;
# f x := app (mkApp f x);
# : Expr -> Expr -> Expr
| f x := app (mkApp f x);
--- ;Expr; that doubles a number.
double : Expr;
double := Λ (! 0 :+: ! 0);
double : Expr := Λ (! 0 :+: ! 0);
--- ;Expr; that adds 1 to a number.
+1 : Expr;
+1 := Λ (! 0 :+: num 1);
+1 : Expr := Λ (! 0 :+: num 1);
apps : Expr -> List Expr -> Expr;
apps := foldl (#);
apps : Expr -> List Expr -> Expr := foldl (#);
--- ;Expr; for function composition.
compose : Expr;
compose := Λ (Λ (Λ (! 2 # (! 1 # ! 0))));
compose : Expr := Λ (Λ (Λ (! 2 # (! 1 # ! 0))));
double+1 : Expr;
double+1 := Λ (compose # +1 # double # ! 0);
double+1 : Expr := Λ (compose # +1 # double # ! 0);
res : Either Error Val;
res := eval (double+1 # num 7);
res : Either Error Val := eval (double+1 # num 7);
main : IO;
main :=
main : IO :=
case res
| left (ScopeError n ctx) :=
printStringLn

37
tests/Compilation/positive/test053.juvix
View File

@ -4,33 +4,30 @@ module test053;
import Stdlib.Prelude open;
{-# inline: 2 #-}
mycompose :
{A B C : Type} -> (B -> C) -> (A -> B) -> A -> C;
mycompose f g x := f (g x);
mycompose : {A B C : Type} -> (B -> C) -> (A -> B) -> A -> C
| f g x := f (g x);
{-# inline: true #-}
myconst : {A B : Type} -> A -> B -> A;
myconst x _ := x;
myconst : {A B : Type} -> A -> B -> A
| x _ := x;
{-# inline: 1 #-}
myflip : {A B C : Type} -> (A -> B -> C) -> B -> A -> C;
myflip f b a := f a b;
myflip : {A B C : Type} -> (A -> B -> C) -> B -> A -> C
| f b a := f a b;
rumpa : {A : Type} -> (A -> A) -> A -> A;
rumpa {A} f a :=
let
{-# inline: 1 #-}
go : Nat -> A -> A;
go zero a := a;
go (suc _) a := f a;
rumpa : {A : Type} -> (A -> A) -> A -> A
| {A} f a :=
let
{-# inline: 1 #-}
go : Nat -> A -> A
| zero a := a
| (suc _) a := f a;
{-# inline: false #-}
h : (A -> A) -> A;
h g := g a;
in h (go 10);
{-# inline: false #-}
h (g : A -> A) : A := g a;
in h (go 10);
main : Nat;
main :=
main : Nat :=
let
f : Nat -> Nat := mycompose λ {x := x + 1} λ {x := x * 2};
g : Nat -> Nat -> Nat := myflip myconst;

50
tests/Compilation/positive/test054.juvix
View File

@ -4,51 +4,49 @@ module test054;
import Stdlib.Prelude open;
syntax iterator myfor;
myfor : {A B : Type} → (A → B → A) → A → List B → A;
myfor := foldl {_} {_};
myfor : {A B : Type} → (A → B → A) → A → List B → A :=
foldl {_} {_};
syntax iterator mymap {init: 0};
mymap : {A B : Type} → (A → B) → List A → List B;
mymap f nil := nil;
mymap f (x :: xs) := f x :: mymap f xs;
mymap : {A B : Type} → (A → B) → List A → List B
| f nil := nil
| f (x :: xs) := f x :: mymap f xs;
sum : List Nat → Nat;
sum xs := myfor (acc := 0) (x in xs) {acc + x};
sum : List Nat → Nat
| xs := myfor (acc := 0) (x in xs) {acc + x};
sum' : List Nat → Nat;
sum' xs := myfor λ {acc x := acc + x} 0 xs;
sum' : List Nat → Nat
| xs := myfor λ {acc x := acc + x} 0 xs;
lst : List Nat;
lst := 1 :: 2 :: 3 :: 4 :: 5 :: nil;
lst : List Nat := 1 :: 2 :: 3 :: 4 :: 5 :: nil;
syntax iterator myfor2 {init: 1, range: 2};
myfor2 :
{A B C : Type}
myfor2
: {A B C : Type}
→ (A → B → C → A)
→ A
→ List B
→ List C
→ A;
myfor2 f acc xs ys :=
myfor (acc' := acc) (x in xs)
myfor (acc'' := acc') (y in ys)
f acc'' x y;
→ A
| f acc xs ys :=
myfor (acc' := acc) (x in xs)
myfor (acc'' := acc') (y in ys)
f acc'' x y;
syntax iterator myzip2 {init: 2, range: 2};
myzip2 :
{A A' B C : Type}
myzip2
: {A A' B C : Type}
→ (A → A' → B → C → A × A')
→ A
→ A'
→ List B
→ List C
→ A × A';
myzip2 f a b xs ys :=
myfor (acc, acc' := a, b) (x, y in zip xs ys)
f acc acc' x y;
→ A × A'
| f a b xs ys :=
myfor (acc, acc' := a, b) (x, y in zip xs ys)
f acc acc' x y;
main : Nat;
main :=
main : Nat :=
sum lst
+ sum' lst
+ fst (myfor (a, b := 0, 0) (x in lst) b + x, a)

8
tests/Compilation/positive/test055.juvix
View File

@ -3,7 +3,9 @@ module test055;
import Stdlib.Prelude open;
type Pair := pair : Nat -> Nat -> Pair;
type Pair :=
| pair : Nat -> Nat -> Pair;
main : List (Pair × Nat) × List Pair;
main := (pair 1 2, 3) :: (pair 2 3, 4) :: nil, pair 1 2 :: pair 2 3 :: nil;
main : List (Pair × Nat) × List Pair :=
(pair 1 2, 3) :: (pair 2 3, 4) :: nil
, pair 1 2 :: pair 2 3 :: nil;

63
tests/Compilation/positive/test056.juvix
View File

@ -4,35 +4,46 @@ module test056;
import Stdlib.Prelude open;
{-# specialize: [1] #-}
mymap : {A B : Type} -> (A -> B) -> List A -> List B;
mymap f nil := nil;
mymap f (x :: xs) := f x :: mymap f xs;
mymap : {A B : Type} -> (A -> B) -> List A -> List B
| f nil := nil
| f (x :: xs) := f x :: mymap f xs;
{-# specialize: [2, 5] #-}
myf : {A B : Type} -> A -> (A -> A -> B) -> A -> B -> Bool -> B;
myf a0 f a b true := f a0 a;
myf a0 f a b false := b;
myf
: {A B : Type}
-> A
-> (A -> A -> B)
-> A
-> B
-> Bool
-> B
| a0 f a b true := f a0 a
| a0 f a b false := b;
myf' : {A B : Type} -> A -> (A -> A -> A -> B) -> A -> B -> B;
myf' a0 f a b := myf a0 (f a0) a b true;
myf'
: {A B : Type} -> A -> (A -> A -> A -> B) -> A -> B -> B
| a0 f a b := myf a0 (f a0) a b true;
sum : List Nat -> Nat;
sum xs := for (acc := 0) (x in xs) {x + acc};
sum : List Nat -> Nat
| xs := for (acc := 0) (x in xs) {x + acc};
funa : {A : Type} -> (A -> A) -> A -> A;
funa {A} f a :=
let
{-# specialize-by: [f] #-}
go : Nat -> A;
go zero := a;
go (suc n) := f (go n);
in go 10;
funa : {A : Type} -> (A -> A) -> A -> A
| {A} f a :=
let
{-# specialize-by: [f] #-}
go : Nat -> A
| zero := a
| (suc n) := f (go n);
in go 10;
main : Nat;
main :=
sum (mymap λ{x := x + 3} (1 :: 2 :: 3 :: 4 :: nil)) +
sum (flatten (mymap (mymap λ{x := x + 2}) ((1 :: nil) :: (2 :: 3 :: nil) :: nil))) +
myf 3 (*) 2 5 true +
myf 1 (+) 2 0 false +
myf' 7 (const (+)) 2 0 +
funa ((+) 1) 5;
main : Nat :=
sum (mymap λ {x := x + 3} (1 :: 2 :: 3 :: 4 :: nil))
+ sum
(flatten
(mymap
(mymap λ {x := x + 2})
((1 :: nil) :: (2 :: 3 :: nil) :: nil)))
+ myf 3 (*) 2 5 true
+ myf 1 (+) 2 0 false
+ myf' 7 (const (+)) 2 0
+ funa ((+) 1) 5;

14
tests/Compilation/positive/test057.juvix
View File

@ -3,11 +3,11 @@ module test057;
import Stdlib.Prelude open;
myfun : {A : Type} -> (A -> A -> A) -> A -> List A -> A;
myfun f x xs := case x :: xs
| nil := x
| y :: nil := y
| y :: z :: _ := f y z;
myfun : {A : Type} -> (A -> A -> A) -> A -> List A -> A
| f x xs :=
case x :: xs
| nil := x
| y :: nil := y
| y :: z :: _ := f y z;
main : Nat;
main := myfun (+) 1 (7 :: 3 :: nil);
main : Nat := myfun (+) 1 (7 :: 3 :: nil);

11
tests/Compilation/positive/test058.juvix
View File

@ -4,11 +4,10 @@ module test058;
import Stdlib.Prelude open hiding {for};
import Stdlib.Data.Nat.Range open;
sum : Nat → Nat;
sum x := for (acc := 0) (n in 1 to x) {acc + n};
sum : Nat → Nat
| x := for (acc := 0) (n in 1 to x) {acc + n};
sum' : Nat → Nat;
sum' x := for (acc := 0) (n in 1 to x step 2) {acc + n};
sum' : Nat → Nat
| x := for (acc := 0) (n in 1 to x step 2) {acc + n};
main : Nat;
main := sum 100 + sum' 100;
main : Nat := sum 100 + sum' 100;

17
tests/Compilation/positive/test059.juvix
View File

@ -3,16 +3,13 @@ module test059;
import Stdlib.Prelude open hiding {head};
mylist : List Nat;
mylist := [1; 2; 3 + 1];
mylist : List Nat := [1; 2; 3 + 1];
mylist2 : List (List Nat);
mylist2 := [[10]; [2]; 3 + 1 :: nil];
mylist2 : List (List Nat) := [[10]; [2]; 3 + 1 :: nil];
head : {a : Type} -> a -> List a -> a;
head a [] := a;
head a [x; _] := x;
head _ (h :: _) := h;
head : {a : Type} -> a -> List a -> a
| a [] := a
| a [x; _] := x
| _ (h :: _) := h;
main : Nat;
main := head 50 mylist + head 50 (head [] mylist2);
main : Nat := head 50 mylist + head 50 (head [] mylist2);

4
tests/Compilation/positive/test060.juvix
View File

@ -32,7 +32,7 @@ main : Triple Nat Nat Nat :=
f :
Triple Nat Nat Nat -> Triple Nat Nat Nat :=
(@Triple{fst := fst * 10});
in
if (mf (mkPair (fst := mkPair true nil; snd := 0 :: nil)))
in if
(mf (mkPair (fst := mkPair true nil; snd := 0 :: nil)))
(f p')
(mkTriple (fst := 0; thd := 0; snd := 0));

5
tests/Geb/positive/Compilation/test001.juvix
View File

@ -1,7 +1,6 @@
-- not function
module test001;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : Bool;
main := λ{x := if x false true} true;
main : Bool := λ {x := if x false true} true;

15
tests/Geb/positive/Compilation/test002.juvix
View File

@ -1,11 +1,16 @@
-- pattern matching
module test002;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type optbool :=
| Just : Bool -> optbool
| Nothing : optbool;
| Just : Bool -> optbool
| Nothing : optbool;
main : Bool;
main := λ{ x (Just b) := if x true b | _ Nothing := false } false (Just true);
main : Bool :=
λ {
x (Just b) := if x true b
| _ Nothing := false
}
false
(Just true);

21
tests/Geb/positive/Compilation/test003.juvix
View File

@ -1,16 +1,17 @@
-- inductive types
module test003;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type enum :=
| opt0 : enum
| opt1 : Bool -> enum
| opt2 : Bool -> Bool -> enum;
| opt0 : enum
| opt1 : Bool -> enum
| opt2 : Bool -> Bool -> enum;
main : Bool;
main := λ{
| opt0 := false
| (opt1 b) := b
| (opt2 b c) := if b b c
} (opt2 false true);
main : Bool :=
λ {
| opt0 := false
| (opt1 b) := b
| (opt2 b c) := if b b c
}
(opt2 false true);

5
tests/Geb/positive/Compilation/test004.juvix
View File

@ -1,7 +1,6 @@
-- definitions
module test004;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : Bool;
main := and (not false) (not (not true));
main : Bool := and (not false) (not (not true));

5
tests/Geb/positive/Compilation/test005.juvix
View File

@ -1,7 +1,6 @@
-- basic arithmetic
module test005;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
main : Nat;
main := 5 + 2 * 3;
main : Nat := 5 + 2 * 3;

40
tests/Geb/positive/Compilation/test006.juvix
View File

@ -1,31 +1,43 @@
-- arithmetic
module test006;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
f : Nat -> Nat -> Nat;
f x y := x + y;
f : Nat -> Nat -> Nat
| x y := x + y;
g : Nat -> Nat -> Nat;
g x y := sub (3 * x) y;
g : Nat -> Nat -> Nat
| x y := sub (3 * x) y;
h : (Nat -> Nat -> Nat) -> Nat -> Nat -> Nat;
h f y z := f y y * z;
h : (Nat -> Nat -> Nat) -> Nat -> Nat -> Nat
| f y z := f y y * z;
x : Nat := 5;
y : Nat := 17;
func : Nat -> Nat := λ{x := x + 4};
func : Nat -> Nat := λ {x := x + 4};
z : Nat := 0;
vx : Nat := 30;
vy : Nat := 7;
main : Nat;
main :=
main : Nat :=
sub
(func (div y x) + -- 17 div 5 + 4 = 7
(z * x + y) + -- 17
(vx + vy * (z + 1)) + -- 37
f (h g 2 3) 4) -- 16
(func (div y x)
+ -- 17 div 5 + 4 = 7
(z
* x
+ y)
+ -- 17
(vx
+ vy * (z + 1))
+ -- 37
f
(h g 2 3)
4)
-- 16
45;
-- result: 32

12
tests/Geb/positive/Compilation/test007.juvix
View File

@ -1,15 +1,15 @@
-- single-constructor inductive types
module test007;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type Box2 :=
box2 : Nat -> Nat -> Box2;
| box2 : Nat -> Nat -> Box2;
type Box :=
box : Box2 -> Box;
| box : Box2 -> Box;
main : Nat;
main := case box (box2 3 5)
| box (box2 x y) := x + y;
main : Nat :=
case box (box2 3 5)
| box (box2 x y) := x + y;
-- result: 8

22
tests/Geb/positive/Compilation/test008.juvix
View File

@ -1,17 +1,17 @@
-- higher-order inductive types
module test008;
open import Stdlib.Prelude;
import Stdlib.Prelude open;
type enum :=
| opt0 : enum
| opt1 : Bool -> enum
| opt2 : Bool -> (Bool -> Bool) -> enum
| opt3 : Bool -> (Bool -> Bool -> Bool) -> Bool -> enum;
| opt0 : enum
| opt1 : Bool -> enum
| opt2 : Bool -> (Bool -> Bool) -> enum
| opt3 : Bool -> (Bool -> Bool -> Bool) -> Bool -> enum;
main : Bool;
main := case (opt3 true (λ{ x y := if y false x }) false)
| opt0 := false
| opt1 b := b
| opt2 b f := f b
| opt3 b1 f b2 := f b1 b2;
main : Bool :=
case opt3 true λ {x y := if y false x} false
| opt0 := false
| opt1 b := b
| opt2 b f := f b
| opt3 b1 f b2 := f b1 b2;

Some files were not shown because too many files have changed in this diff Show More