diff --git a/Makefile b/Makefile index a7461cc1fc..c80ba82944 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/app/Commands/Format.hs b/app/Commands/Format.hs index 5575bf9dee..2972cc9e1c 100644 --- a/app/Commands/Format.hs +++ b/app/Commands/Format.hs @@ -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 diff --git a/app/Commands/Format/Options.hs b/app/Commands/Format/Options.hs index 60b3f48ec9..dc179ed186 100644 --- a/app/Commands/Format/Options.hs +++ b/app/Commands/Format/Options.hs @@ -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" diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix index 416f2c932d..7a425db27d 100644 --- a/examples/milestone/Bank/Bank.juvix +++ b/examples/milestone/Bank/Bank.juvix @@ -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. diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix index bfaf3f7547..7977b9c715 100644 --- a/examples/milestone/Collatz/Collatz.juvix +++ b/examples/milestone/Collatz/Collatz.juvix @@ -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"; diff --git a/examples/milestone/Fibonacci/Fibonacci.juvix b/examples/milestone/Fibonacci/Fibonacci.juvix index 8c47a86586..56f23c2518 100644 --- a/examples/milestone/Fibonacci/Fibonacci.juvix +++ b/examples/milestone/Fibonacci/Fibonacci.juvix @@ -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); diff --git a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix index 17789bdb6e..c6f7c9daa9 100644 --- a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix +++ b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix @@ -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))); diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix index 1cf349838e..45bb264044 100644 --- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix +++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix @@ -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 diff --git a/examples/milestone/TicTacToe/Logic/Board.juvix b/examples/milestone/TicTacToe/Logic/Board.juvix index c89a44df6c..cc83832bb2 100644 --- a/examples/milestone/TicTacToe/Logic/Board.juvix +++ b/examples/milestone/TicTacToe/Logic/Board.juvix @@ -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) := diff --git a/examples/milestone/TicTacToe/Logic/Extra.juvix b/examples/milestone/TicTacToe/Logic/Extra.juvix index ea6e2ac7ae..98a7a06540 100644 --- a/examples/milestone/TicTacToe/Logic/Extra.juvix +++ b/examples/milestone/TicTacToe/Logic/Extra.juvix @@ -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); diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix index fa01c68363..01f8edd2a5 100644 --- a/examples/milestone/TicTacToe/Logic/Game.juvix +++ b/examples/milestone/TicTacToe/Logic/Game.juvix @@ -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; diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix index 77ac80d089..710e8c4922 100644 --- a/examples/milestone/TicTacToe/Logic/Square.juvix +++ b/examples/milestone/TicTacToe/Logic/Square.juvix @@ -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; diff --git a/juvix-stdlib b/juvix-stdlib index abe514cb45..b7edcc335f 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit abe514cb45def5b512e08b85f22959c33e2238ac +Subproject commit b7edcc335feee4e3db87b5aca46381e2d9644ab0 diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs index b38ef3e86a..750bb4f5e0 100644 --- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs @@ -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)) diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs index ef6036ef7b..cd9b7ca8e8 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index 13ba0d0081..92f743cffe 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 80e745e3ef..229718b7cb 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -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) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index a169596b7f..8ce805532f 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index a435202ff9..0fc5fd60ad 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index d1e597ad9d..455bdbe704 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 4a6dfd068e..9131bec2e6 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index d2057311c5..3d8f8baee2 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -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) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 9540d611de..03f9d537a0 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -205,9 +205,7 @@ replInput :: forall r. Members '[Files, PathResolver, InfoTableBuilder, JudocSta replInput = P.label "" $ ReplExpression <$> parseExpressionAtoms - <|> P.try (ReplOpenImport <$> newOpenSyntax) - <|> ReplImport <$> import_ - <|> ReplOpenImport <$> openModule + <|> either ReplImport ReplOpenImport <$> importOpenSyntax -------------------------------------------------------------------------------- -- Symbols and names @@ -296,22 +294,14 @@ statement = P.label "" $ 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 "" $ 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 "" $ do +functionDefinition _signBuiltin = P.label "" $ 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) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index cd8dcb2fad..015012ec84 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -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] -> - Sem r Internal.FunctionDef -goLetFunctionDef = goFunctionDefHelper - -goFunctionDefHelper :: - forall r. - Members '[Builtins, NameIdGen, Reader Pragmas, Error ScoperError] r => - TypeSignature 'Scoped -> - [FunctionClause 'Scoped] -> + FunctionDef '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 diff --git a/src/Juvix/Formatter.hs b/src/Juvix/Formatter.hs index d153992e41..d4e565b8ee 100644 --- a/src/Juvix/Formatter.hs +++ b/src/Juvix/Formatter.hs @@ -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) diff --git a/test/Formatter/Positive.hs b/test/Formatter/Positive.hs index d36a5898a5..618f7c0a8e 100644 --- a/test/Formatter/Positive.hs +++ b/test/Formatter/Positive.hs @@ -28,7 +28,6 @@ makeFormatTest' Scope.PosTest {..} = . runOutputList @FormattedFileInfo . runScopeEffIO . runFilesIO - . runReader (NewSyntax False) $ format file' case d of Right (_, FormatResultOK) -> return () diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index cb5062f84f..44ab638c2f 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -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") diff --git a/tests/Compilation/negative/test001.juvix b/tests/Compilation/negative/test001.juvix index 1bd8968a0c..2c32aaebca 100644 --- a/tests/Compilation/negative/test001.juvix +++ b/tests/Compilation/negative/test001.juvix @@ -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; diff --git a/tests/Compilation/negative/test002.juvix b/tests/Compilation/negative/test002.juvix index c1cce6424d..37641b35e9 100644 --- a/tests/Compilation/negative/test002.juvix +++ b/tests/Compilation/negative/test002.juvix @@ -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); diff --git a/tests/Compilation/negative/test003.juvix b/tests/Compilation/negative/test003.juvix index 6c32d197a8..0487108773 100644 --- a/tests/Compilation/negative/test003.juvix +++ b/tests/Compilation/negative/test003.juvix @@ -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; diff --git a/tests/Compilation/negative/test004.juvix b/tests/Compilation/negative/test004.juvix index 04a732e901..6cb0fb3ce2 100644 --- a/tests/Compilation/negative/test004.juvix +++ b/tests/Compilation/negative/test004.juvix @@ -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; diff --git a/tests/Compilation/negative/test005.juvix b/tests/Compilation/negative/test005.juvix index c84a248b12..76aff564e4 100644 --- a/tests/Compilation/negative/test005.juvix +++ b/tests/Compilation/negative/test005.juvix @@ -5,5 +5,4 @@ type Unit := unit : Unit; axiom Boom : Unit; -x : Unit; -x := Boom; +x : Unit := Boom; diff --git a/tests/Compilation/positive/test001.juvix b/tests/Compilation/positive/test001.juvix index a4a9fb1b09..aac894efe4 100644 --- a/tests/Compilation/positive/test001.juvix +++ b/tests/Compilation/positive/test001.juvix @@ -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); diff --git a/tests/Compilation/positive/test002.juvix b/tests/Compilation/positive/test002.juvix index 0da855a4f2..e42b65fbea 100644 --- a/tests/Compilation/positive/test002.juvix +++ b/tests/Compilation/positive/test002.juvix @@ -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); diff --git a/tests/Compilation/positive/test003.juvix b/tests/Compilation/positive/test003.juvix index 346faebc68..fbf6be4cc8 100644 --- a/tests/Compilation/positive/test003.juvix +++ b/tests/Compilation/positive/test003.juvix @@ -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); diff --git a/tests/Compilation/positive/test004.juvix b/tests/Compilation/positive/test004.juvix index 9a80f8fc84..a95f83e6df 100644 --- a/tests/Compilation/positive/test004.juvix +++ b/tests/Compilation/positive/test004.juvix @@ -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"; diff --git a/tests/Compilation/positive/test005.juvix b/tests/Compilation/positive/test005.juvix index 02556ff5fa..5ba20ea4ad 100644 --- a/tests/Compilation/positive/test005.juvix +++ b/tests/Compilation/positive/test005.juvix @@ -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); diff --git a/tests/Compilation/positive/test006.juvix b/tests/Compilation/positive/test006.juvix index a5ded90bda..4a9b1c8ecb 100644 --- a/tests/Compilation/positive/test006.juvix +++ b/tests/Compilation/positive/test006.juvix @@ -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); diff --git a/tests/Compilation/positive/test007.juvix b/tests/Compilation/positive/test007.juvix index 4fc5bc9a47..9b9d31d0b3 100644 --- a/tests/Compilation/positive/test007.juvix +++ b/tests/Compilation/positive/test007.juvix @@ -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)); - -lst : List Nat; -lst := 0 :: 1 :: nil; - -printNatList : List Nat → IO; -printNatList nil := printString "nil"; -printNatList (h :: t) := printNat h >> printString " :: " >> printNatList t; - -printNatListLn : List Nat → IO; -printNatListLn lst := 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; +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 := 0 :: 1 :: nil; + +printNatList : List Nat → IO + | nil := printString "nil" + | (h :: t) := + printNat h >> printString " :: " >> printNatList t; + +printNatListLn (lst : List Nat) : IO := + printNatList lst >> printString "\n"; + +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); diff --git a/tests/Compilation/positive/test008.juvix b/tests/Compilation/positive/test008.juvix index f8ac0271c9..a01efbf309 100644 --- a/tests/Compilation/positive/test008.juvix +++ b/tests/Compilation/positive/test008.juvix @@ -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); diff --git a/tests/Compilation/positive/test009.juvix b/tests/Compilation/positive/test009.juvix index 7932a6d6b2..139ebd00a7 100644 --- a/tests/Compilation/positive/test009.juvix +++ b/tests/Compilation/positive/test009.juvix @@ -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); diff --git a/tests/Compilation/positive/test010.juvix b/tests/Compilation/positive/test010.juvix index 22d0f1ebaf..d09b01f2c8 100644 --- a/tests/Compilation/positive/test010.juvix +++ b/tests/Compilation/positive/test010.juvix @@ -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); diff --git a/tests/Compilation/positive/test011.juvix b/tests/Compilation/positive/test011.juvix index 48dac2f24b..e1d098605f 100644 --- a/tests/Compilation/positive/test011.juvix +++ b/tests/Compilation/positive/test011.juvix @@ -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); diff --git a/tests/Compilation/positive/test012.juvix b/tests/Compilation/positive/test012.juvix index 0914e149c9..43e068d45f 100644 --- a/tests/Compilation/positive/test012.juvix +++ b/tests/Compilation/positive/test012.juvix @@ -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"; diff --git a/tests/Compilation/positive/test013.juvix b/tests/Compilation/positive/test013.juvix index ee4f6218b7..e9d84dc4d4 100644 --- a/tests/Compilation/positive/test013.juvix +++ b/tests/Compilation/positive/test013.juvix @@ -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); diff --git a/tests/Compilation/positive/test014.juvix b/tests/Compilation/positive/test014.juvix index 832125d3ee..e20d99f22e 100644 --- a/tests/Compilation/positive/test014.juvix +++ b/tests/Compilation/positive/test014.juvix @@ -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 diff --git a/tests/Compilation/positive/test015.juvix b/tests/Compilation/positive/test015.juvix index d54c207e5a..85ac0d1035 100644 --- a/tests/Compilation/positive/test015.juvix +++ b/tests/Compilation/positive/test015.juvix @@ -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; diff --git a/tests/Compilation/positive/test016.juvix b/tests/Compilation/positive/test016.juvix index 2c7fa129dc..c2123affdf 100644 --- a/tests/Compilation/positive/test016.juvix +++ b/tests/Compilation/positive/test016.juvix @@ -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 diff --git a/tests/Compilation/positive/test017.juvix b/tests/Compilation/positive/test017.juvix index 327f1e9140..749fbfbd27 100644 --- a/tests/Compilation/positive/test017.juvix +++ b/tests/Compilation/positive/test017.juvix @@ -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); diff --git a/tests/Compilation/positive/test018.juvix b/tests/Compilation/positive/test018.juvix index eba2e0d5a4..1fc723b20e 100644 --- a/tests/Compilation/positive/test018.juvix +++ b/tests/Compilation/positive/test018.juvix @@ -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; diff --git a/tests/Compilation/positive/test019.juvix b/tests/Compilation/positive/test019.juvix index d1f09a6d6a..f87c6c752a 100644 --- a/tests/Compilation/positive/test019.juvix +++ b/tests/Compilation/positive/test019.juvix @@ -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; diff --git a/tests/Compilation/positive/test020.juvix b/tests/Compilation/positive/test020.juvix index a59889d307..9a387d19ba 100644 --- a/tests/Compilation/positive/test020.juvix +++ b/tests/Compilation/positive/test020.juvix @@ -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); diff --git a/tests/Compilation/positive/test021.juvix b/tests/Compilation/positive/test021.juvix index 62053a7292..ac7ce1afcc 100644 --- a/tests/Compilation/positive/test021.juvix +++ b/tests/Compilation/positive/test021.juvix @@ -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; diff --git a/tests/Compilation/positive/test022.juvix b/tests/Compilation/positive/test022.juvix index b17435bd42..8a30c42d33 100644 --- a/tests/Compilation/positive/test022.juvix +++ b/tests/Compilation/positive/test022.juvix @@ -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; diff --git a/tests/Compilation/positive/test023.juvix b/tests/Compilation/positive/test023.juvix index 70fd4f2bda..fdfb1af8e7 100644 --- a/tests/Compilation/positive/test023.juvix +++ b/tests/Compilation/positive/test023.juvix @@ -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; -terminating -g : Nat → Nat; +f : Nat → Nat + + | x := if (x < 1) 1 (2 * x + g (sub x 1)); + terminating -h : Nat → Nat; +g : Nat → Nat + | x := if (x < 1) 1 (x + h (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)); +terminating +h : Nat → Nat + | x := if (x < 1) 1 (x * f (sub x 1)); -main : IO; -main := - printNatLn (f 5) >> - printNatLn (f 10) >> - printNatLn (f 20); +main : IO := + printNatLn (f 5) + >> printNatLn (f 10) + >> printNatLn (f 20); -end; diff --git a/tests/Compilation/positive/test024.juvix b/tests/Compilation/positive/test024.juvix index 518ff9b0f5..620aecba38 100644 --- a/tests/Compilation/positive/test024.juvix +++ b/tests/Compilation/positive/test024.juvix @@ -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; - -isNode : Tree → Bool; -isNode (node _ _) := true; -isNode leaf := false; - -g leaf := leaf; -g (node l r) := if (isNode l) r (node r l); - -main : IO; -main := printNatLn (f (gen 10)); - -end; +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 + | (node _ _) := true + | leaf := false; + +main : IO := printNatLn (f (gen 10)); + diff --git a/tests/Compilation/positive/test025.juvix b/tests/Compilation/positive/test025.juvix index 4e45c69361..a40bddc0a8 100644 --- a/tests/Compilation/positive/test025.juvix +++ b/tests/Compilation/positive/test025.juvix @@ -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; diff --git a/tests/Compilation/positive/test026.juvix b/tests/Compilation/positive/test026.juvix index 5050813050..5c83dc1443 100644 --- a/tests/Compilation/positive/test026.juvix +++ b/tests/Compilation/positive/test026.juvix @@ -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; diff --git a/tests/Compilation/positive/test027.juvix b/tests/Compilation/positive/test027.juvix index 8b91844260..189a20de16 100644 --- a/tests/Compilation/positive/test027.juvix +++ b/tests/Compilation/positive/test027.juvix @@ -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; diff --git a/tests/Compilation/positive/test028.juvix b/tests/Compilation/positive/test028.juvix index d8624b23b6..2d8002728f 100644 --- a/tests/Compilation/positive/test028.juvix +++ b/tests/Compilation/positive/test028.juvix @@ -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; diff --git a/tests/Compilation/positive/test029.juvix b/tests/Compilation/positive/test029.juvix index 7ff82b73cd..efa465ee51 100644 --- a/tests/Compilation/positive/test029.juvix +++ b/tests/Compilation/positive/test029.juvix @@ -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; diff --git a/tests/Compilation/positive/test030.juvix b/tests/Compilation/positive/test030.juvix index ef061255f7..8db307a639 100644 --- a/tests/Compilation/positive/test030.juvix +++ b/tests/Compilation/positive/test030.juvix @@ -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; diff --git a/tests/Compilation/positive/test031.juvix b/tests/Compilation/positive/test031.juvix index 9c0341210f..8718f7ef7d 100644 --- a/tests/Compilation/positive/test031.juvix +++ b/tests/Compilation/positive/test031.juvix @@ -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)); diff --git a/tests/Compilation/positive/test032.juvix b/tests/Compilation/positive/test032.juvix index f022c6a802..bdf8495c00 100644 --- a/tests/Compilation/positive/test032.juvix +++ b/tests/Compilation/positive/test032.juvix @@ -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); - -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; - -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; - -printListNatLn : List Nat → IO; -printListNatLn nil := printStringLn "nil"; -printListNatLn (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))))); - -end; +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 + | acc zero f := acc + | acc (suc n) f := gen (f (suc n) :: acc) n f; + +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 + | nil := printStringLn "nil" + | (x :: xs) := + printNat x >> printString " :: " >> printListNatLn xs; + +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))))); + diff --git a/tests/Compilation/positive/test033.juvix b/tests/Compilation/positive/test033.juvix index cffba6daae..391dc1c608 100644 --- a/tests/Compilation/positive/test033.juvix +++ b/tests/Compilation/positive/test033.juvix @@ -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; diff --git a/tests/Compilation/positive/test034.juvix b/tests/Compilation/positive/test034.juvix index 8667e08bd9..d12f4f9db4 100644 --- a/tests/Compilation/positive/test034.juvix +++ b/tests/Compilation/positive/test034.juvix @@ -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; diff --git a/tests/Compilation/positive/test035.juvix b/tests/Compilation/positive/test035.juvix index b106023408..a29c150c5a 100644 --- a/tests/Compilation/positive/test035.juvix +++ b/tests/Compilation/positive/test035.juvix @@ -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; - -g leaf := leaf; -g (node (node _ _) r) := r; -g (node l r) := node r l; - -h : Nat -> Nat; -h (suc (suc (suc (suc n)))) := n; -h _ := 0; - -printListNatLn : List Nat → IO; -printListNatLn nil := printStringLn "nil"; -printListNatLn (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); - -end; +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 : Tree → Tree + | leaf := leaf + | (node (node _ _) r) := r + | (node l r) := node r l; + +h : Nat -> Nat + | (suc (suc (suc (suc n)))) := n + | _ := 0; + +printListNatLn : List Nat → IO + | nil := printStringLn "nil" + | (x :: xs) := + printNat x >> printString " :: " >> printListNatLn xs; + +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); + diff --git a/tests/Compilation/positive/test036.juvix b/tests/Compilation/positive/test036.juvix index e9f988e8d8..14ea641d93 100644 --- a/tests/Compilation/positive/test036.juvix +++ b/tests/Compilation/positive/test036.juvix @@ -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; diff --git a/tests/Compilation/positive/test037.juvix b/tests/Compilation/positive/test037.juvix index 5461138b8d..4fd13d6e8e 100644 --- a/tests/Compilation/positive/test037.juvix +++ b/tests/Compilation/positive/test037.juvix @@ -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)); diff --git a/tests/Compilation/positive/test038.juvix b/tests/Compilation/positive/test038.juvix index bb86bdf42e..72d64ae4dd 100644 --- a/tests/Compilation/positive/test038.juvix +++ b/tests/Compilation/positive/test038.juvix @@ -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; diff --git a/tests/Compilation/positive/test039.juvix b/tests/Compilation/positive/test039.juvix index 47958220b1..e3b49a3660 100644 --- a/tests/Compilation/positive/test039.juvix +++ b/tests/Compilation/positive/test039.juvix @@ -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)); diff --git a/tests/Compilation/positive/test040.juvix b/tests/Compilation/positive/test040.juvix index eacb564c13..0b7d6d21e3 100644 --- a/tests/Compilation/positive/test040.juvix +++ b/tests/Compilation/positive/test040.juvix @@ -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)); diff --git a/tests/Compilation/positive/test041.juvix b/tests/Compilation/positive/test041.juvix index 304cd0ce07..2b611d4db7 100644 --- a/tests/Compilation/positive/test041.juvix +++ b/tests/Compilation/positive/test041.juvix @@ -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"); diff --git a/tests/Compilation/positive/test042.juvix b/tests/Compilation/positive/test042.juvix index 6ba1256f7e..f2150da883 100644 --- a/tests/Compilation/positive/test042.juvix +++ b/tests/Compilation/positive/test042.juvix @@ -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"; diff --git a/tests/Compilation/positive/test043.juvix b/tests/Compilation/positive/test043.juvix index 33febce63e..a78d3c7140 100644 --- a/tests/Compilation/positive/test043.juvix +++ b/tests/Compilation/positive/test043.juvix @@ -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; diff --git a/tests/Compilation/positive/test044.juvix b/tests/Compilation/positive/test044.juvix index dd60fdd317..91c26b305e 100644 --- a/tests/Compilation/positive/test044.juvix +++ b/tests/Compilation/positive/test044.juvix @@ -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; diff --git a/tests/Compilation/positive/test045.juvix b/tests/Compilation/positive/test045.juvix index 1c9b6c92c5..d99c2428e6 100644 --- a/tests/Compilation/positive/test045.juvix +++ b/tests/Compilation/positive/test045.juvix @@ -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; diff --git a/tests/Compilation/positive/test046.juvix b/tests/Compilation/positive/test046.juvix index f6573657c3..b2edd3ca27 100644 --- a/tests/Compilation/positive/test046.juvix +++ b/tests/Compilation/positive/test046.juvix @@ -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; diff --git a/tests/Compilation/positive/test047.juvix b/tests/Compilation/positive/test047.juvix index d0a7694684..2edaa87b89 100644 --- a/tests/Compilation/positive/test047.juvix +++ b/tests/Compilation/positive/test047.juvix @@ -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; diff --git a/tests/Compilation/positive/test048.juvix b/tests/Compilation/positive/test048.juvix index 93282e5661..f7355b3e23 100644 --- a/tests/Compilation/positive/test048.juvix +++ b/tests/Compilation/positive/test048.juvix @@ -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"; diff --git a/tests/Compilation/positive/test049.juvix b/tests/Compilation/positive/test049.juvix index e88bd8b9b5..3ccfc19fe9 100644 --- a/tests/Compilation/positive/test049.juvix +++ b/tests/Compilation/positive/test049.juvix @@ -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); diff --git a/tests/Compilation/positive/test050.juvix b/tests/Compilation/positive/test050.juvix index 0127d86543..8617f407a5 100644 --- a/tests/Compilation/positive/test050.juvix +++ b/tests/Compilation/positive/test050.juvix @@ -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; diff --git a/tests/Compilation/positive/test051.juvix b/tests/Compilation/positive/test051.juvix index 9a744a8133..d7bf153fe2 100644 --- a/tests/Compilation/positive/test051.juvix +++ b/tests/Compilation/positive/test051.juvix @@ -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; diff --git a/tests/Compilation/positive/test052.juvix b/tests/Compilation/positive/test052.juvix index 1dc5ca6408..4af2d05f4d 100644 --- a/tests/Compilation/positive/test052.juvix +++ b/tests/Compilation/positive/test052.juvix @@ -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'; - -AppTy := App'; +Expr : Type := Expr' Nat; -Expr : Type; -Expr := Expr' Nat; +Lambda : Type := Lambda' Nat; -Lambda : Type; -Lambda := Lambda' Nat; +App : Type := App' 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 := Val' Nat; +Val : Type := 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 diff --git a/tests/Compilation/positive/test053.juvix b/tests/Compilation/positive/test053.juvix index 38ce41dd6d..ef4dbfc0f5 100644 --- a/tests/Compilation/positive/test053.juvix +++ b/tests/Compilation/positive/test053.juvix @@ -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; diff --git a/tests/Compilation/positive/test054.juvix b/tests/Compilation/positive/test054.juvix index 469b5dc209..03ed5ee5ab 100644 --- a/tests/Compilation/positive/test054.juvix +++ b/tests/Compilation/positive/test054.juvix @@ -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) diff --git a/tests/Compilation/positive/test055.juvix b/tests/Compilation/positive/test055.juvix index 8110d9e420..a952191178 100644 --- a/tests/Compilation/positive/test055.juvix +++ b/tests/Compilation/positive/test055.juvix @@ -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; diff --git a/tests/Compilation/positive/test056.juvix b/tests/Compilation/positive/test056.juvix index f94ec1b354..1c06d38ba1 100644 --- a/tests/Compilation/positive/test056.juvix +++ b/tests/Compilation/positive/test056.juvix @@ -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; diff --git a/tests/Compilation/positive/test057.juvix b/tests/Compilation/positive/test057.juvix index 4d868b4266..978c2eefaf 100644 --- a/tests/Compilation/positive/test057.juvix +++ b/tests/Compilation/positive/test057.juvix @@ -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); diff --git a/tests/Compilation/positive/test058.juvix b/tests/Compilation/positive/test058.juvix index ad1b00c618..699b35ccc3 100644 --- a/tests/Compilation/positive/test058.juvix +++ b/tests/Compilation/positive/test058.juvix @@ -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; diff --git a/tests/Compilation/positive/test059.juvix b/tests/Compilation/positive/test059.juvix index 060c9831b6..03a5be832f 100644 --- a/tests/Compilation/positive/test059.juvix +++ b/tests/Compilation/positive/test059.juvix @@ -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); diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix index 51ec9ab5d0..b9d946b91a 100644 --- a/tests/Compilation/positive/test060.juvix +++ b/tests/Compilation/positive/test060.juvix @@ -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)); diff --git a/tests/Geb/positive/Compilation/test001.juvix b/tests/Geb/positive/Compilation/test001.juvix index ade55a8160..de66290299 100644 --- a/tests/Geb/positive/Compilation/test001.juvix +++ b/tests/Geb/positive/Compilation/test001.juvix @@ -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; diff --git a/tests/Geb/positive/Compilation/test002.juvix b/tests/Geb/positive/Compilation/test002.juvix index 6f4067002b..1d46ad9586 100644 --- a/tests/Geb/positive/Compilation/test002.juvix +++ b/tests/Geb/positive/Compilation/test002.juvix @@ -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); diff --git a/tests/Geb/positive/Compilation/test003.juvix b/tests/Geb/positive/Compilation/test003.juvix index fe99fdefef..7fe822a886 100644 --- a/tests/Geb/positive/Compilation/test003.juvix +++ b/tests/Geb/positive/Compilation/test003.juvix @@ -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); diff --git a/tests/Geb/positive/Compilation/test004.juvix b/tests/Geb/positive/Compilation/test004.juvix index 5ba7ea7ea9..eb2a7a29ea 100644 --- a/tests/Geb/positive/Compilation/test004.juvix +++ b/tests/Geb/positive/Compilation/test004.juvix @@ -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)); diff --git a/tests/Geb/positive/Compilation/test005.juvix b/tests/Geb/positive/Compilation/test005.juvix index 5439a1eb59..595e4165af 100644 --- a/tests/Geb/positive/Compilation/test005.juvix +++ b/tests/Geb/positive/Compilation/test005.juvix @@ -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; diff --git a/tests/Geb/positive/Compilation/test006.juvix b/tests/Geb/positive/Compilation/test006.juvix index e743627c97..84a726cc63 100644 --- a/tests/Geb/positive/Compilation/test006.juvix +++ b/tests/Geb/positive/Compilation/test006.juvix @@ -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 diff --git a/tests/Geb/positive/Compilation/test007.juvix b/tests/Geb/positive/Compilation/test007.juvix index f78e571871..8902a5a69a 100644 --- a/tests/Geb/positive/Compilation/test007.juvix +++ b/tests/Geb/positive/Compilation/test007.juvix @@ -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 diff --git a/tests/Geb/positive/Compilation/test008.juvix b/tests/Geb/positive/Compilation/test008.juvix index 10220a7647..5ddfe43d7d 100644 --- a/tests/Geb/positive/Compilation/test008.juvix +++ b/tests/Geb/positive/Compilation/test008.juvix @@ -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; diff --git a/tests/Geb/positive/Compilation/test009.juvix b/tests/Geb/positive/Compilation/test009.juvix index 5294f14815..1101191521 100644 --- a/tests/Geb/positive/Compilation/test009.juvix +++ b/tests/Geb/positive/Compilation/test009.juvix @@ -1,13 +1,22 @@ -- let module test009; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Nat; -main := - 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 - x + y + z; +main : Nat := + 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 x + y + z; diff --git a/tests/Geb/positive/Compilation/test010.juvix b/tests/Geb/positive/Compilation/test010.juvix index cd843122b5..6fc6e284cd 100644 --- a/tests/Geb/positive/Compilation/test010.juvix +++ b/tests/Geb/positive/Compilation/test010.juvix @@ -1,21 +1,17 @@ -- functions returning functions with variable capture module test010; -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 : Nat; -main := - f 5 6 + - f 6 5 + - f 10 5 + - f 11 5; +main : Nat := f 5 6 + f 6 5 + f 10 5 + f 11 5; diff --git a/tests/Geb/positive/Compilation/test011.juvix b/tests/Geb/positive/Compilation/test011.juvix index a2172595c7..044ae950f8 100644 --- a/tests/Geb/positive/Compilation/test011.juvix +++ b/tests/Geb/positive/Compilation/test011.juvix @@ -1,33 +1,34 @@ -- applications with lets and cases in function position module test011; -open import Stdlib.Prelude; +import Stdlib.Prelude open; type Pair := - pair : ((Nat → Nat) → Nat → Nat) → Nat → Pair; + | pair : ((Nat → Nat) → Nat → Nat) → Nat → Pair; -id' : Nat → Nat; -id' x := x; +id' : Nat → Nat + | x := x; -id'' : (Nat → Nat) → Nat → Nat; -id'' x := x; +id'' : (Nat → Nat) → Nat → Nat + | x := x; -id''' : ((Nat → Nat) → Nat → Nat) → (Nat → Nat) → Nat → Nat; -id''' x := x; +id''' : ((Nat → Nat) → Nat → Nat) → (Nat → Nat) → Nat → Nat + | x := x; -f : Pair → Nat; -f l := (case l - | pair x zero := x - | _ := id'') - (let - y : Nat → Nat; - y := id'; +f : Pair → Nat + | l := + (case l + | pair x zero := x + | _ := id'') + (let + y : Nat → Nat := id'; in (let - z : (Nat → Nat) → Nat → Nat; - z := id''; - in (case l | pair _ zero := id''' | _ := id''') z) - y) - 7; + z : (Nat → Nat) → Nat → Nat := id''; + in (case l + | pair _ zero := id''' + | _ := id''') + z) + y) + 7; -main : Nat; -main := f (pair λ{| x y := x y + 2 } 0); +main : Nat := f (pair λ {| x y := x y + 2} 0); diff --git a/tests/Geb/positive/Compilation/test012.juvix b/tests/Geb/positive/Compilation/test012.juvix index bc6047e457..3adf746083 100644 --- a/tests/Geb/positive/Compilation/test012.juvix +++ b/tests/Geb/positive/Compilation/test012.juvix @@ -1,8 +1,8 @@ -- mid-square hashing (unrolled) module test012; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; pow0 : Nat := 1; @@ -38,72 +38,71 @@ pow15 : Nat := 2 * pow14; pow16 : Nat := 2 * pow15; -hash0 : Nat -> Nat; -hash0 x := 0; +hash0 : Nat -> Nat + | x := 0; -hash1 : Nat -> Nat; -hash1 x := x * x; +hash1 : Nat -> Nat + | x := x * x; -hash2 : Nat -> Nat; -hash2 x := x * x; +hash2 : Nat -> Nat + | x := x * x; -hash3 : Nat -> Nat; -hash3 x := x * x; +hash3 : Nat -> Nat + | x := x * x; -hash4 : Nat -> Nat; -hash4 x := - if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6); +hash4 : Nat -> Nat + | x := + if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6); -hash5 : Nat -> Nat; -hash5 x := - if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6); +hash5 : Nat -> Nat + | x := + if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6); -hash6 : Nat -> Nat; -hash6 x := - if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6); +hash6 : Nat -> Nat + | x := + if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6); -hash7 : Nat -> Nat; -hash7 x := - if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6); +hash7 : Nat -> Nat + | x := + if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6); -hash8 : Nat -> Nat; -hash8 x := - if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6); +hash8 : Nat -> Nat + | x := + if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6); -hash9 : Nat -> Nat; -hash9 x := - if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6); +hash9 : Nat -> Nat + | x := + if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6); -hash10 : Nat -> Nat; -hash10 x := - if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6); +hash10 : Nat -> Nat + | x := + if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6); -hash11 : Nat -> Nat; -hash11 x := - if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6); +hash11 : Nat -> Nat + | x := + if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6); -hash12 : Nat -> Nat; -hash12 x := - if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6); +hash12 : Nat -> Nat + | x := + if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6); -hash13 : Nat -> Nat; -hash13 x := - if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6); +hash13 : Nat -> Nat + | x := + if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6); -hash14 : Nat -> Nat; -hash14 x := - if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6); +hash14 : Nat -> Nat + | x := + if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6); -hash15 : Nat -> Nat; -hash15 x := - if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6); +hash15 : Nat -> Nat + | x := + if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6); -hash16 : Nat -> Nat; -hash16 x := - if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6); +hash16 : Nat -> Nat + | x := + if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6); hash : Nat -> Nat := hash16; -main : Nat; -main := hash 1367; +main : Nat := hash 1367; -- result: 3 diff --git a/tests/Geb/positive/Compilation/test013.juvix b/tests/Geb/positive/Compilation/test013.juvix index 8ffdfa2274..7829995199 100644 --- a/tests/Geb/positive/Compilation/test013.juvix +++ b/tests/Geb/positive/Compilation/test013.juvix @@ -1,11 +1,10 @@ -- recursion module test013; -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 : Nat; -main := sum 100; +main : Nat := sum 100; diff --git a/tests/Geb/positive/Compilation/test014.juvix b/tests/Geb/positive/Compilation/test014.juvix index fb986984e9..0d93968eb4 100644 --- a/tests/Geb/positive/Compilation/test014.juvix +++ b/tests/Geb/positive/Compilation/test014.juvix @@ -1,14 +1,12 @@ -- tail recursion module test014; -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' : Nat → Nat → Nat + | acc zero := acc + | acc (suc x) := sum' (suc x + acc) x; -sum : Nat → Nat; -sum := sum' 0; +sum : Nat → Nat := sum' 0; -main : Nat; -main := sum 100; +main : Nat := sum 100; diff --git a/tests/Geb/positive/Compilation/test015.juvix b/tests/Geb/positive/Compilation/test015.juvix index 75c767d49a..96f7e4be67 100644 --- a/tests/Geb/positive/Compilation/test015.juvix +++ b/tests/Geb/positive/Compilation/test015.juvix @@ -1,14 +1,12 @@ -- tail recursion: Fibonacci numbers in linear time module test015; -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 : Nat; -main := fib 10; +main : Nat := fib 10; diff --git a/tests/Geb/positive/Compilation/test016.juvix b/tests/Geb/positive/Compilation/test016.juvix index cc0e3a60d2..63a3359e3a 100644 --- a/tests/Geb/positive/Compilation/test016.juvix +++ b/tests/Geb/positive/Compilation/test016.juvix @@ -1,26 +1,25 @@ -- local functions with free variables module test016; -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 - if (x == 0) - (f 10) - (if (x < 10) - λ{y := g (f (sub x 1) y)} - g); +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 : Nat; -main := f 100 500 + f 5 0 + f 5 5 + h 10 + g 10 h + g 3 (f 10); +main : Nat := + f 100 500 + f 5 0 + f 5 5 + h 10 + g 10 h + g 3 (f 10); diff --git a/tests/Geb/positive/Compilation/test017.juvix b/tests/Geb/positive/Compilation/test017.juvix index b6515dc1c1..c64f26591a 100644 --- a/tests/Geb/positive/Compilation/test017.juvix +++ b/tests/Geb/positive/Compilation/test017.juvix @@ -1,15 +1,15 @@ -- recursion through higher-order functions module test017; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -g : (Nat → Nat) → Nat → Nat; -g f zero := 0; -g f (suc x) := f x; +g : (Nat → Nat) → Nat → Nat + | f zero := 0 + | f (suc x) := f x; terminating -f : Nat → Nat; -f x := x + g f x; +f : Nat → Nat + | x := x + g f x; -main : Nat; -main := f 10; -- 55 +main : Nat := f 10; +-- 55 diff --git a/tests/Geb/positive/Compilation/test018.juvix b/tests/Geb/positive/Compilation/test018.juvix index b4156e8e6f..15ad7e4e0f 100644 --- a/tests/Geb/positive/Compilation/test018.juvix +++ b/tests/Geb/positive/Compilation/test018.juvix @@ -1,18 +1,16 @@ -- tail recursion through higher-order functions module test018; -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 : Nat → (Nat → Nat → Nat) → Nat → Nat + | acc f zero := acc + | acc f (suc x) := f acc x; terminating -sum' : Nat → Nat → Nat; -sum' acc x := sumb (x + acc) sum' x; +sum' : Nat → Nat → Nat + | acc x := sumb (x + acc) sum' x; -sum : Nat → Nat; -sum := sum' 0; +sum : Nat → Nat := sum' 0; -main : Nat; -main := sum 100; +main : Nat := sum 100; diff --git a/tests/Geb/positive/Compilation/test019.juvix b/tests/Geb/positive/Compilation/test019.juvix index 04861d40f1..a8ac798281 100644 --- a/tests/Geb/positive/Compilation/test019.juvix +++ b/tests/Geb/positive/Compilation/test019.juvix @@ -1,16 +1,15 @@ -- higher-order functions module test019; -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 : Nat; -main := u 2; +main : Nat := u 2; diff --git a/tests/Geb/positive/Compilation/test020.juvix b/tests/Geb/positive/Compilation/test020.juvix index c6f1d1bf73..19d8b8649e 100644 --- a/tests/Geb/positive/Compilation/test020.juvix +++ b/tests/Geb/positive/Compilation/test020.juvix @@ -1,12 +1,11 @@ -- McCarthy's 91 function module test020; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; 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))); -main : Nat; -main := f91 101 + f91 95 + f91 16 + f91 5; +main : Nat := f91 101 + f91 95 + f91 16 + f91 5; diff --git a/tests/Geb/positive/Compilation/test021.juvix b/tests/Geb/positive/Compilation/test021.juvix index 09692a99a1..524a0ca5f9 100644 --- a/tests/Geb/positive/Compilation/test021.juvix +++ b/tests/Geb/positive/Compilation/test021.juvix @@ -1,20 +1,20 @@ -- 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 : Nat; -main := power 2 3 + power 3 7 + power 5 11; +main : Nat := power 2 3 + power 3 7 + power 5 11; diff --git a/tests/Geb/positive/Compilation/test022.juvix b/tests/Geb/positive/Compilation/test022.juvix index 976593c08a..c076b5102a 100644 --- a/tests/Geb/positive/Compilation/test022.juvix +++ b/tests/Geb/positive/Compilation/test022.juvix @@ -1,19 +1,20 @@ -- mutual recursion module test022; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; terminating -f : Nat → Nat; -terminating -g : Nat → Nat; +f : Nat → Nat + + | x := if (x < 1) 1 (2 * x + g (sub x 1)); + terminating -h : Nat → Nat; +g : Nat → Nat + | x := if (x < 1) 1 (x + h (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)); +terminating +h : Nat → Nat + | x := if (x < 1) 1 (x * f (sub x 1)); -main : Nat; -main := f 5 + f 10 + f 20; +main : Nat := f 5 + f 10 + f 20; diff --git a/tests/Geb/positive/Compilation/test023.juvix b/tests/Geb/positive/Compilation/test023.juvix index c42ed406bd..dc99f21d3c 100644 --- a/tests/Geb/positive/Compilation/test023.juvix +++ b/tests/Geb/positive/Compilation/test023.juvix @@ -1,21 +1,17 @@ -- Euclid's algorithm module test023; -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 : Nat; -main := - gcd (3 * 7 * 2) (7 * 2 * 11) + - gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5) + - gcd 3 7 + - gcd 7 3 + - gcd (11 * 7 * 3) (2 * 5 * 13); +main : Nat := + gcd (3 * 7 * 2) (7 * 2 * 11) + + gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5) + + gcd 3 7 + + gcd 7 3 + + gcd (11 * 7 * 3) (2 * 5 * 13); diff --git a/tests/Geb/positive/Compilation/test024.juvix b/tests/Geb/positive/Compilation/test024.juvix index 100338c6d8..42fe9c745b 100644 --- a/tests/Geb/positive/Compilation/test024.juvix +++ b/tests/Geb/positive/Compilation/test024.juvix @@ -1,12 +1,17 @@ -- Ackermann function module test024; -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 : Nat; -main := ack 0 7 + ack 1 7 + ack 1 13 + ack 2 7 + ack 2 13 + ack 3 4; +main : Nat := + ack 0 7 + + ack 1 7 + + ack 1 13 + + ack 2 7 + + ack 2 13 + + ack 3 4; diff --git a/tests/Geb/positive/Compilation/test025.juvix b/tests/Geb/positive/Compilation/test025.juvix index 7251a7d17f..69d4235623 100644 --- a/tests/Geb/positive/Compilation/test025.juvix +++ b/tests/Geb/positive/Compilation/test025.juvix @@ -1,23 +1,22 @@ -- mid-square hashing module test025; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; -pow : Nat -> Nat; -pow zero := 1; -pow (suc n) := 2 * pow n; +pow : Nat -> Nat + | zero := 1 + | (suc n) := 2 * pow n; -hash' : Nat -> Nat -> Nat; -hash' (suc n@(suc (suc m))) x := - if - (x < pow n) - (hash' n x) - (mod (div (x * x) (pow m)) (pow 6)); -hash' _ x := x * x; +hash' : Nat -> Nat -> Nat + | (suc n@(suc (suc m))) x := + if + (x < pow n) + (hash' n x) + (mod (div (x * x) (pow m)) (pow 6)) + | _ x := x * x; hash : Nat -> Nat := hash' 16; -main : Nat; -main := hash 1367; +main : Nat := hash 1367; -- result: 3 diff --git a/tests/Geb/positive/Compilation/test026.juvix b/tests/Geb/positive/Compilation/test026.juvix index 25c6b0da95..183aeed7d7 100644 --- a/tests/Geb/positive/Compilation/test026.juvix +++ b/tests/Geb/positive/Compilation/test026.juvix @@ -1,30 +1,26 @@ -- recursive let module test026; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; -sum : Nat → Nat; -sum := let - sum' : Nat → Nat; - sum' := λ { +sum : Nat → Nat := + let + sum' : Nat → Nat := + λ { zero := zero | (suc n) := suc n + sum' n }; - in sum'; + in sum'; -mutrec : Nat; -mutrec := let +mutrec : Nat := + let terminating - f : Nat → Nat; + f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x); terminating - g : Nat → Nat; + g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1)); 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)); + h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1)); in f 5 + f 10 + g 5 + h 5; -main : Nat; -main := sum 100 + mutrec; +main : Nat := sum 100 + mutrec; diff --git a/tests/Geb/positive/Compilation/test027.juvix b/tests/Geb/positive/Compilation/test027.juvix index a029704071..46435684f5 100644 --- a/tests/Geb/positive/Compilation/test027.juvix +++ b/tests/Geb/positive/Compilation/test027.juvix @@ -1,11 +1,14 @@ -- Simple case expression module test027; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -type Pair := pair : Nat -> Nat -> Pair; +type Pair := + | pair : Nat -> Nat -> Pair; -main : Nat; -main := case pair 1 2 | pair (suc _) zero := 0 | pair (suc _) (suc x) := x | _ := 19; +main : Nat := + case pair 1 2 + | pair (suc _) zero := 0 + | pair (suc _) (suc x) := x + | _ := 19; -end; diff --git a/tests/Geb/positive/Compilation/test028.juvix b/tests/Geb/positive/Compilation/test028.juvix index de67896a95..e63d85742e 100644 --- a/tests/Geb/positive/Compilation/test028.juvix +++ b/tests/Geb/positive/Compilation/test028.juvix @@ -1,21 +1,17 @@ -- Mutually recursive let expressions module test028; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Bool; -main := +main : Bool := 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 odd (plusOne 13) || even (plusOne 12); diff --git a/tests/Geb/positive/Compilation/test029.juvix b/tests/Geb/positive/Compilation/test029.juvix index cadd07f243..e44f6ea710 100644 --- a/tests/Geb/positive/Compilation/test029.juvix +++ b/tests/Geb/positive/Compilation/test029.juvix @@ -1,11 +1,10 @@ -- pattern matching on natural numbers module test029; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -h : Nat -> Nat; -h (suc (suc (suc (suc n)))) := n; -h _ := 0; +h : Nat -> Nat + | (suc (suc (suc (suc n)))) := n + | _ := 0; -main : Nat; -main := h 5 + h 3; +main : Nat := h 5 + h 3; diff --git a/tests/Geb/positive/Compilation/test030.juvix b/tests/Geb/positive/Compilation/test030.juvix index 1ca7d7df7d..d395c9c28b 100644 --- a/tests/Geb/positive/Compilation/test030.juvix +++ b/tests/Geb/positive/Compilation/test030.juvix @@ -1,12 +1,11 @@ -- recursion with unroll pragma module test013; -open import Stdlib.Prelude; +import Stdlib.Prelude open; {-# unroll: 11 #-} -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 : Nat; -main := sum 10; +main : Nat := sum 10; diff --git a/tests/Internal/Core/positive/test006.juvix b/tests/Internal/Core/positive/test006.juvix index 09a88f2205..07314796a3 100644 --- a/tests/Internal/Core/positive/test006.juvix +++ b/tests/Internal/Core/positive/test006.juvix @@ -1,16 +1,13 @@ 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; -e : Nat; -e := (if (3 > 0) 1 loop) + (if (2 < 1) loop (if (7 >= 8) loop 1)); +e : Nat := (if (3 > 0) 1 loop) + (if (2 < 1) loop (if (7 >= 8) loop 1)); -main : IO; -main := printNatLn e; +main : IO := printNatLn e; end; diff --git a/tests/Internal/Core/positive/test011.juvix b/tests/Internal/Core/positive/test011.juvix index 450ca20e12..b5fcf61dd6 100644 --- a/tests/Internal/Core/positive/test011.juvix +++ b/tests/Internal/Core/positive/test011.juvix @@ -1,16 +1,15 @@ module test011; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; -fib' : Nat -> Nat -> Nat -> Nat; -fib' zero x _ := x; -fib' (suc n) x y := fib' n y (x + y); +fib' : Nat -> Nat -> Nat -> Nat + | zero x _ := x + | (suc n) x y := fib' n y (x + y); -fib : Nat -> Nat; -fib n := fib' n zero (suc zero); +fib (n : Nat) : Nat := fib' n zero (suc zero); -main : IO; -main := printNatLn (fib (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))); - -end; +main : IO := + printNatLn + (fib + (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))); diff --git a/tests/Internal/positive/AsPatterns.juvix b/tests/Internal/positive/AsPatterns.juvix index 38b446d418..c441e2a452 100644 --- a/tests/Internal/positive/AsPatterns.juvix +++ b/tests/Internal/positive/AsPatterns.juvix @@ -1,39 +1,42 @@ module AsPatterns; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -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; -f1 : List Nat -> List Nat; -f1 a@(x :: (x' :: xs)) := a; -f1 _ := nil; +f1 : List Nat -> List Nat + | a@(x :: x' :: xs) := a + | _ := nil; -f2 : List Nat -> List Nat; -f2 (x :: a@(x' :: xs)) := a; -f2 _ := nil; +f2 : List Nat -> List Nat + | (x :: a@(x' :: xs)) := a + | _ := nil; -f3 : Nat -> List Nat -> List Nat; -f3 _ a@(x :: (x' :: xs)) := a; +f3 : Nat -> List Nat -> List Nat + | _ a@(x :: x' :: xs) := a; -f4 : Nat -> List Nat -> Nat; -f4 y (x :: a@(x' :: xs)) := y; +f4 : Nat -> List Nat -> Nat + | y (x :: a@(x' :: xs)) := y; -f5 : List Nat -> List Nat -> List Nat; -f5 (x :: a@(x' :: xs)) (y :: b@(y' :: ys)) := b; +f5 : List Nat -> List Nat -> List Nat + | (x :: a@(x' :: xs)) (y :: b@(y' :: ys)) := b; -l1 : List Nat; -l1 := zero :: suc zero :: nil; +l1 : List Nat := zero :: suc zero :: nil; -l2 : List Nat; -l2 := zero :: suc zero :: suc (suc zero) :: suc (suc (suc zero)) :: nil; +l2 : List Nat := + zero + :: suc zero + :: suc (suc zero) + :: suc (suc (suc zero)) + :: nil; -main : IO; -main := printListNatLn (f1 l1) - >> printListNatLn (f2 l1) - >> printListNatLn (f3 zero l1) - >> printNatLn (f4 zero l1) - >> printListNatLn (f5 l1 l2); +main : IO := + printListNatLn (f1 l1) + >> printListNatLn (f2 l1) + >> printListNatLn (f3 zero l1) + >> printNatLn (f4 zero l1) + >> printListNatLn (f5 l1 l2); -end; diff --git a/tests/Internal/positive/BuiltinAdd.juvix b/tests/Internal/positive/BuiltinAdd.juvix index 395eff78c0..c7e022c34b 100644 --- a/tests/Internal/positive/BuiltinAdd.juvix +++ b/tests/Internal/positive/BuiltinAdd.juvix @@ -1,14 +1,10 @@ module BuiltinAdd; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -n : Nat; -n := (suc (suc zero)); +n : Nat := suc (suc zero); -m : Nat; -m := (suc zero); +m : Nat := suc zero; -main : Nat; -main := m + n; +main : Nat := m + n; -end; diff --git a/tests/Internal/positive/BuiltinBool.juvix b/tests/Internal/positive/BuiltinBool.juvix index 1be159bd2d..6fb9f30855 100644 --- a/tests/Internal/positive/BuiltinBool.juvix +++ b/tests/Internal/positive/BuiltinBool.juvix @@ -1,8 +1,6 @@ module BuiltinBool; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Bool; -main := true || false; +main : Bool := true || false; -end; diff --git a/tests/Internal/positive/BuiltinIf.juvix b/tests/Internal/positive/BuiltinIf.juvix index e9afc0c10b..03aa0f5f92 100644 --- a/tests/Internal/positive/BuiltinIf.juvix +++ b/tests/Internal/positive/BuiltinIf.juvix @@ -1,8 +1,6 @@ module BuiltinIf; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Bool; -main := if false (and false) (and true) true; +main : Bool := if false (and false) (and true) true; -end; diff --git a/tests/Internal/positive/BuiltinInductive.juvix b/tests/Internal/positive/BuiltinInductive.juvix index 44de926ef1..706cb37c0e 100644 --- a/tests/Internal/positive/BuiltinInductive.juvix +++ b/tests/Internal/positive/BuiltinInductive.juvix @@ -3,7 +3,5 @@ module BuiltinInductive; builtin string axiom MyString : Type; -main : Type; -main := MyString; +main : Type := MyString; -end; diff --git a/tests/Internal/positive/Case.juvix b/tests/Internal/positive/Case.juvix index 2f4fa4aa32..e950317cbf 100644 --- a/tests/Internal/positive/Case.juvix +++ b/tests/Internal/positive/Case.juvix @@ -1,18 +1,20 @@ module Case; - open import Stdlib.Prelude; - not' : Bool → Bool; - not' b := case b +import Stdlib.Prelude open; + +not' : Bool → Bool + | b := + case b | true := false | false := true; - terminating - andList : List Bool → Bool; - andList l := case l +terminating +andList : List Bool → Bool + | l := + case l | nil := true | x :: xs := x && andList xs; - main : IO; - main := printBoolLn (not' false) +main : IO := + printBoolLn (not' false) >> printBoolLn (andList (true :: false :: nil)); -end; diff --git a/tests/Internal/positive/Church.juvix b/tests/Internal/positive/Church.juvix index 13a84f47bd..b3fb29c400 100644 --- a/tests/Internal/positive/Church.juvix +++ b/tests/Internal/positive/Church.juvix @@ -1,21 +1,17 @@ module Church; -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; -toNat : Num → Nat; -toNat n := n {_} ((+) (suc zero)) zero; +toNat : Num → Nat + | n := n {_} ((+) (suc zero)) zero; -main : IO; -main := - printNatLn (toNat (csuc (czero))); +main : IO := printNatLn (toNat (csuc (czero))); -end; diff --git a/tests/Internal/positive/FunctionReturnConstructor.juvix b/tests/Internal/positive/FunctionReturnConstructor.juvix index 9c5d8a764c..f05cb7da21 100644 --- a/tests/Internal/positive/FunctionReturnConstructor.juvix +++ b/tests/Internal/positive/FunctionReturnConstructor.juvix @@ -1,9 +1,7 @@ module FunctionReturnConstructor; type Foo := - foo : Foo; + | foo : Foo; -main : Foo; -main := foo; +main : Foo := foo; -end; diff --git a/tests/Internal/positive/FunctionType.juvix b/tests/Internal/positive/FunctionType.juvix index 8bfce45c30..e2e84bc48c 100644 --- a/tests/Internal/positive/FunctionType.juvix +++ b/tests/Internal/positive/FunctionType.juvix @@ -1,9 +1,7 @@ module FunctionType; type A := - a : A; + | a : A; -main : Type; -main := (A : Type) -> (B : Type) -> A -> B; +main : Type := (A : Type) -> (B : Type) -> A -> B; -end; diff --git a/tests/Internal/positive/HigherOrderLambda.juvix b/tests/Internal/positive/HigherOrderLambda.juvix index b06042959e..8cc270d9a1 100644 --- a/tests/Internal/positive/HigherOrderLambda.juvix +++ b/tests/Internal/positive/HigherOrderLambda.juvix @@ -1,14 +1,16 @@ module HigherOrderLambda; -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 : Type} → {B : Type} → (A → B) → List A → List B + | f := + \ { + nil := nil + | (h :: t) := f h :: map' f t + }; -lst : List Nat; -lst := zero :: suc zero :: nil; +lst : List Nat := zero :: suc zero :: nil; -main : IO; -main := printNatLn (foldr (+) zero (map' ((+) (suc zero)) lst)); +main : IO := + printNatLn (foldr (+) zero (map' ((+) (suc zero)) lst)); -end; diff --git a/tests/Internal/positive/IdenFunctionArgs.juvix b/tests/Internal/positive/IdenFunctionArgs.juvix index 77418f4972..f40015657c 100644 --- a/tests/Internal/positive/IdenFunctionArgs.juvix +++ b/tests/Internal/positive/IdenFunctionArgs.juvix @@ -1,11 +1,9 @@ module IdenFunctionArgs; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat → Nat → Nat; -f x y := x; +f : Nat → Nat → Nat + | x y := x; -main : Nat; -main := f 100 200; +main : Nat := f 100 200; -end; diff --git a/tests/Internal/positive/IdenFunctionArgsImplicit.juvix b/tests/Internal/positive/IdenFunctionArgsImplicit.juvix index b51cb1db54..e148104da6 100644 --- a/tests/Internal/positive/IdenFunctionArgsImplicit.juvix +++ b/tests/Internal/positive/IdenFunctionArgsImplicit.juvix @@ -1,11 +1,9 @@ module IdenFunctionArgsImplicit; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : {A : Type} → Nat → A → Nat; -f x y := x; +f : {A : Type} → Nat → A → Nat + | x y := x; -main : Nat; -main := f 100 200; +main : Nat := f 100 200; -end; diff --git a/tests/Internal/positive/IdenFunctionIntegerLiteral.juvix b/tests/Internal/positive/IdenFunctionIntegerLiteral.juvix index 351bf60b96..4f0083c7a3 100644 --- a/tests/Internal/positive/IdenFunctionIntegerLiteral.juvix +++ b/tests/Internal/positive/IdenFunctionIntegerLiteral.juvix @@ -1,11 +1,8 @@ module IdenFunctionIntegerLiteral; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat; -f := 1; +f : Nat := 1; -main : Nat; -main := f; +main : Nat := f; -end; diff --git a/tests/Internal/positive/Import/Importee.juvix b/tests/Internal/positive/Import/Importee.juvix index 1fd0fcdb59..9df406e60d 100644 --- a/tests/Internal/positive/Import/Importee.juvix +++ b/tests/Internal/positive/Import/Importee.juvix @@ -1,8 +1,7 @@ module Importee; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat; -f := 1; +f : Nat := 1; end; diff --git a/tests/Internal/positive/Import/Importer.juvix b/tests/Internal/positive/Import/Importer.juvix index 917117c950..54e6abf4e0 100644 --- a/tests/Internal/positive/Import/Importer.juvix +++ b/tests/Internal/positive/Import/Importer.juvix @@ -1,9 +1,8 @@ module Importer; -open import Stdlib.Prelude; -open import Importee; +import Stdlib.Prelude open; +import Importee open; -main : Nat; -main := f; +main : Nat := f; end; diff --git a/tests/Internal/positive/Inductive.juvix b/tests/Internal/positive/Inductive.juvix index 32f57207cd..a145a1bd94 100644 --- a/tests/Internal/positive/Inductive.juvix +++ b/tests/Internal/positive/Inductive.juvix @@ -1,11 +1,10 @@ module Inductive; -type Unit := unit : Unit; +type Unit := + | unit : Unit; type A (B : Type) := - a : A B; + | a : A B; -main : Type; -main := A Unit; +main : Type := A Unit; -end; diff --git a/tests/Internal/positive/IntegerLiteral.juvix b/tests/Internal/positive/IntegerLiteral.juvix index 8e697a687e..733f7cacba 100644 --- a/tests/Internal/positive/IntegerLiteral.juvix +++ b/tests/Internal/positive/IntegerLiteral.juvix @@ -1,8 +1,6 @@ module IntegerLiteral; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Nat; -main := 1; +main : Nat := 1; -end; diff --git a/tests/Internal/positive/Lambda.juvix b/tests/Internal/positive/Lambda.juvix index 288e381f24..b9dfc8fa96 100644 --- a/tests/Internal/positive/Lambda.juvix +++ b/tests/Internal/positive/Lambda.juvix @@ -1,39 +1,43 @@ module Lambda; - open import Stdlib.Prelude public; - id' : {A : Type} → A → A; - id' := λ { - | a := a - }; +import Stdlib.Prelude open public; - uncurry' : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A - × B → C; - uncurry' := λ { - | f (a , b) := f a b - }; +id' : {A : Type} → A → A := λ {| a := a}; - fst' : {A : Type} → {B : Type} → A × B → A; - fst' {_} := λ { - | (a , _) := a - }; +uncurry' + : {A : Type} + → {B : Type} + → {C : Type} + → (A → B → C) + → A × B + → C := λ {| f (a, b) := f a b}; - first' : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A - × B → A' × B; - first' := λ { - | f (a , b) := f a , b - }; +fst' : {A : Type} → {B : Type} → A × B → A + | {_} := λ {| (a, _) := a}; - foldr' : {A : Type} → {B : Type} → (A → B → B) → B → List - A → B; - foldr' := λ { - | _ z nil := z - | f z (h :: hs) := f h (foldr' f z hs) - }; +first' + : {A : Type} + → {B : Type} + → {A' : Type} + → (A → A') + → A × B + → A' × B := λ {| f (a, b) := f a, b}; - main : IO; - main := printNatLn (id' zero) - >> printNatLn (uncurry' (+) (1 , 1)) - >> printNatLn (fst' (zero , 1)) - >> printNatLn (fst (first' ((+) 1) (1 , zero))) +foldr' + : {A : Type} + → {B : Type} + → (A → B → B) + → B + → List A + → B := + λ { + | _ z nil := z + | f z (h :: hs) := f h (foldr' f z hs) + }; + +main : IO := + printNatLn (id' zero) + >> printNatLn (uncurry' (+) (1, 1)) + >> printNatLn (fst' (zero, 1)) + >> printNatLn (fst (first' ((+) 1) (1, zero))) >> printNatLn (foldr' (+) zero (1 :: 2 :: 3 :: nil)); -end; diff --git a/tests/Internal/positive/LitInteger.juvix b/tests/Internal/positive/LitInteger.juvix index 7bcb282990..181d045516 100644 --- a/tests/Internal/positive/LitInteger.juvix +++ b/tests/Internal/positive/LitInteger.juvix @@ -1,14 +1,11 @@ module LitInteger; -open import Stdlib.Prelude public; +import Stdlib.Prelude open public; -main : Nat; -main := 1 + 2; +main : Nat := 1 + 2; -nilNat : List Nat; -nilNat := nil; +nilNat : List Nat := nil; -cons : Nat -> List Nat -> List Nat; -cons a xs := a :: xs; +cons : Nat -> List Nat -> List Nat + | a xs := a :: xs; -end; diff --git a/tests/Internal/positive/LitIntegerToNat.juvix b/tests/Internal/positive/LitIntegerToNat.juvix index 79c9778456..beeb150124 100644 --- a/tests/Internal/positive/LitIntegerToNat.juvix +++ b/tests/Internal/positive/LitIntegerToNat.juvix @@ -1,12 +1,10 @@ module LitIntegerToNat; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat -> Nat; -f (suc x) := x; -f zero := 0; +f : Nat -> Nat + | (suc x) := x + | zero := 0; -main : IO; -main := printNatLn (f 3) >> printNatLn (f 0); +main : IO := printNatLn (f 3) >> printNatLn (f 0); -end; diff --git a/tests/Internal/positive/LitString.juvix b/tests/Internal/positive/LitString.juvix index c279538346..7339ea8093 100644 --- a/tests/Internal/positive/LitString.juvix +++ b/tests/Internal/positive/LitString.juvix @@ -1,8 +1,6 @@ module LitString; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : String; -main := "hello"; +main : String := "hello"; -end; diff --git a/tests/Internal/positive/LitStringIO.juvix b/tests/Internal/positive/LitStringIO.juvix index fe5a447cd5..6d5d261450 100644 --- a/tests/Internal/positive/LitStringIO.juvix +++ b/tests/Internal/positive/LitStringIO.juvix @@ -1,8 +1,6 @@ module LitStringIO; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : IO; -main := printStringLn "hello"; +main : IO := printStringLn "hello"; -end; diff --git a/tests/Internal/positive/MatchConstructor.juvix b/tests/Internal/positive/MatchConstructor.juvix index 08a111de41..16dce607fb 100644 --- a/tests/Internal/positive/MatchConstructor.juvix +++ b/tests/Internal/positive/MatchConstructor.juvix @@ -1,16 +1,14 @@ module MatchConstructor; -open import Stdlib.Prelude hiding {toNat}; +import Stdlib.Prelude open hiding {toNat}; type Foo := - foo1 : Nat → Foo | - foo2 : Foo; + | foo1 : Nat → Foo + | foo2 : Foo; -toNat : Foo → Nat; -toNat (foo1 n) := n; -toNat foo2 := zero; +toNat : Foo → Nat + | (foo1 n) := n + | foo2 := zero; -main : Nat; -main := toNat (foo1 200); +main : Nat := toNat (foo1 200); -end; diff --git a/tests/Internal/positive/Mutual.juvix b/tests/Internal/positive/Mutual.juvix index 5b8fdae1b1..118081c3ad 100644 --- a/tests/Internal/positive/Mutual.juvix +++ b/tests/Internal/positive/Mutual.juvix @@ -1,17 +1,16 @@ module Mutual; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -odd : _; -even : _; +odd : _ + + | zero := false + | (suc n) := even n; -odd zero := false; -odd (suc n) := even n; +even : _ + + | zero := true + | (suc n) := odd n; -even zero := true; -even (suc n) := odd n; +main : Bool := even (suc (suc (suc zero))); -main : Bool; -main := even (suc (suc (suc zero))); - -end; diff --git a/tests/Internal/positive/NatMatch1.juvix b/tests/Internal/positive/NatMatch1.juvix index 1c0a332d02..ff94973eaf 100644 --- a/tests/Internal/positive/NatMatch1.juvix +++ b/tests/Internal/positive/NatMatch1.juvix @@ -1,15 +1,12 @@ module NatMatch1; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat → Nat → Nat; -f zero k := 100; -f (suc n) (suc (suc m)) := m; +f : Nat → Nat → Nat + | zero k := 100 + | (suc n) (suc (suc m)) := m; -n : Nat; -n := suc (suc (suc (suc (suc zero)))); +n : Nat := suc (suc (suc (suc (suc zero)))); -main : Nat; -main := f n n; +main : Nat := f n n; -end; diff --git a/tests/Internal/positive/NatMatch2.juvix b/tests/Internal/positive/NatMatch2.juvix index 547690a3f6..5e1f599e25 100644 --- a/tests/Internal/positive/NatMatch2.juvix +++ b/tests/Internal/positive/NatMatch2.juvix @@ -1,15 +1,12 @@ module NatMatch2; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat → Nat → Nat; -f zero k := zero; -f n (suc (suc m)) := n; +f : Nat → Nat → Nat + | zero k := zero + | n (suc (suc m)) := n; -n : Nat; -n := suc (suc (suc (suc (suc zero)))); +n : Nat := suc (suc (suc (suc (suc zero)))); -main : Nat; -main := f n n; +main : Nat := f n n; -end; diff --git a/tests/Internal/positive/NestedModuleScope/Base.juvix b/tests/Internal/positive/NestedModuleScope/Base.juvix index 3b09f0dad9..3e409b30cd 100644 --- a/tests/Internal/positive/NestedModuleScope/Base.juvix +++ b/tests/Internal/positive/NestedModuleScope/Base.juvix @@ -1,5 +1,5 @@ module Base; module NestedBase; - open import Base2 public; + import Base2 open public; end; diff --git a/tests/Internal/positive/NestedModuleScope/Import.juvix b/tests/Internal/positive/NestedModuleScope/Import.juvix index 3380568e9d..e6ffed9c09 100644 --- a/tests/Internal/positive/NestedModuleScope/Import.juvix +++ b/tests/Internal/positive/NestedModuleScope/Import.juvix @@ -1,7 +1,6 @@ module Import; -open import Base; -open import Base2; +import Base open; +import Base2 open; -main : Foo; -main := foo; +main : Foo := foo; diff --git a/tests/Internal/positive/PatternArgs.juvix b/tests/Internal/positive/PatternArgs.juvix index 72ad3d8654..0f3dd694ac 100644 --- a/tests/Internal/positive/PatternArgs.juvix +++ b/tests/Internal/positive/PatternArgs.juvix @@ -1,12 +1,12 @@ module PatternArgs; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat -> Nat -> Nat; -f zero zero := zero; -f n1@(suc m1) n2@(suc m2) := n1 + m1 + (suc (suc zero)) * (n2 + m2); +f : Nat -> Nat -> Nat + | zero zero := zero + | n1@(suc m1) n2@(suc m2) := + n1 + m1 + suc (suc zero) * (n2 + m2); -main : IO; -main := printNatLn (f (suc (suc zero)) (suc (suc (suc zero)))); +main : IO := + printNatLn (f (suc (suc zero)) (suc (suc (suc zero)))); -end; diff --git a/tests/Internal/positive/QuickSort.juvix b/tests/Internal/positive/QuickSort.juvix index 275bee3a5a..ebfc46f4ac 100644 --- a/tests/Internal/positive/QuickSort.juvix +++ b/tests/Internal/positive/QuickSort.juvix @@ -1,38 +1,45 @@ module QuickSort; -open import Stdlib.Prelude hiding {quickSort}; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open hiding {quickSort}; +import Stdlib.Data.Nat.Ord open; -qsHelper : {A : Type} → A → List A × List A → List A; -qsHelper a (l , r) := l ++ (a :: nil) ++ r; +qsHelper : {A : Type} → A → List A × List A → List A + | a (l, r) := l ++ (a :: nil) ++ r; terminating -quickSort : {A : Type} → (A → A → Ordering) → List A → List A; -quickSort _ nil := nil; -quickSort _ (x :: nil) := x :: nil; -quickSort cmp (x :: xs) := qsHelper x - (both (quickSort cmp) (partition (isGT ∘ cmp x) xs)); +quickSort + : {A : Type} → (A → A → Ordering) → List A → List A + | _ nil := nil + | _ (x :: nil) := x :: nil + | cmp (x :: xs) := + qsHelper + x + (both (quickSort cmp) (partition (isGT ∘ cmp x) xs)); + +uniq + : {A : Type} -> (A -> A -> Ordering) -> List A -> List A + | _ nil := nil + | _ y@(x :: nil) := y + | cmp (x :: x' :: xs) := + if + (isEQ (cmp x x')) + (uniq cmp (x' :: xs)) + (x :: uniq cmp (x' :: xs)); + +gen : Nat -> (Nat -> Nat) -> List Nat -> List Nat + | zero _ acc := acc + | n@(suc n') f acc := gen n' f (f n :: acc); + +gen2 : Nat -> Nat -> List (List Nat) -> List (List Nat) + | _ zero acc := acc + | m n@(suc n') acc := gen2 m n' (gen m ((+) n) nil :: acc); + +three : Nat := suc (suc (suc zero)); + +four : Nat := suc three; + +main : List Nat := + uniq + compare + (quickSort compare (flatten (gen2 three four nil))); -uniq : {A : Type} -> (A -> A -> Ordering) -> List A -> List A; -uniq _ nil := nil; -uniq _ y@(x :: nil) := y; -uniq cmp (x :: x' :: xs) := if (isEQ (cmp x x')) (uniq cmp (x' :: xs)) (x :: (uniq cmp (x' :: xs))); - -gen : Nat -> (Nat -> Nat) -> List Nat -> List Nat; -gen zero _ acc := acc; -gen n@(suc n') f acc := gen n' f (f n :: acc); - -gen2 : Nat -> Nat -> List (List Nat) -> List (List Nat); -gen2 _ zero acc := acc; -gen2 m n@(suc n') acc := gen2 m n' ((gen m ((+) n) nil) :: acc); - -three : Nat; -three := suc (suc (suc zero)); - -four : Nat; -four := suc three; - -main : List Nat; -main := uniq compare (quickSort compare (flatten (gen2 three four nil))); - -end; diff --git a/tests/Internal/positive/Universe.juvix b/tests/Internal/positive/Universe.juvix index 57085cbd2b..5cc6bcf8b5 100644 --- a/tests/Internal/positive/Universe.juvix +++ b/tests/Internal/positive/Universe.juvix @@ -1,6 +1,4 @@ module Universe; -main : Type; -main := Type; +main : Type := Type; -end; diff --git a/tests/VampIR/negative/test001.juvix b/tests/VampIR/negative/test001.juvix index 075666b1ad..630445caf3 100644 --- a/tests/VampIR/negative/test001.juvix +++ b/tests/VampIR/negative/test001.juvix @@ -5,5 +5,4 @@ import Stdlib.Data.Nat.Ord open; {-# argnames: [a, b c] #-} -main : Nat -> Nat -> Nat -> Bool; -main x y z := x + y == z; +main (x y z : Nat) : Bool := x + y == z; diff --git a/tests/VampIR/positive/Compilation/test001.juvix b/tests/VampIR/positive/Compilation/test001.juvix index 6b5161442d..bc2fa5d2eb 100644 --- a/tests/VampIR/positive/Compilation/test001.juvix +++ b/tests/VampIR/positive/Compilation/test001.juvix @@ -1,8 +1,8 @@ -- not function module test001; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; -main : Nat -> Nat; -main x := if (x == 0) 1 0; +main : Nat -> Nat + | x := if (x == 0) 1 0; diff --git a/tests/VampIR/positive/Compilation/test002.juvix b/tests/VampIR/positive/Compilation/test002.juvix index c26ff429c1..4aeeb46b17 100644 --- a/tests/VampIR/positive/Compilation/test002.juvix +++ b/tests/VampIR/positive/Compilation/test002.juvix @@ -8,19 +8,19 @@ type optbool := | Just : Bool -> optbool | Nothing : optbool; -natToBool : Nat -> Bool; -natToBool x := if (x == 0) false true; +natToBool : Nat -> Bool + | x := if (x == 0) false true; -boolToNat : Bool -> Nat; -boolToNat x := if x 1 0; +boolToNat : Bool -> Nat + | x := if x 1 0; {-# public: [b] #-} -main : Nat -> Nat -> Nat; -main a b := - boolToNat - $ λ { - | x (Just b) := if x false b - | _ Nothing := false - } - (natToBool a) - (Just (natToBool b)); +main : Nat -> Nat -> Nat + | a b := + boolToNat + $ λ { + | x (Just b) := if x false b + | _ Nothing := false + } + (natToBool a) + (Just (natToBool b)); diff --git a/tests/VampIR/positive/Compilation/test003.juvix b/tests/VampIR/positive/Compilation/test003.juvix index 159ca63069..575840e407 100644 --- a/tests/VampIR/positive/Compilation/test003.juvix +++ b/tests/VampIR/positive/Compilation/test003.juvix @@ -1,23 +1,26 @@ -- inductive types module test003; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; type enum := -| opt0 : enum -| opt1 : Bool -> enum -| opt2 : Bool -> Bool -> enum; + | opt0 : enum + | opt1 : Bool -> enum + | opt2 : Bool -> Bool -> enum; -natToBool : Nat -> Bool; -natToBool x := if (x == 0) false true; +natToBool : Nat -> Bool + | x := if (x == 0) false true; -boolToNat : Bool -> Nat; -boolToNat x := if x 1 0; +boolToNat : Bool -> Nat + | x := if x 1 0; -main : Nat -> Nat -> Nat; -main x y := boolToNat $ λ{ -| opt0 := false -| (opt1 b) := b -| (opt2 b c) := if b b c -} (opt2 (natToBool x) (natToBool y)); +main : Nat -> Nat -> Nat + | x y := + boolToNat + $ λ { + | opt0 := false + | (opt1 b) := b + | (opt2 b c) := if b b c + } + (opt2 (natToBool x) (natToBool y)); diff --git a/tests/VampIR/positive/Compilation/test004.juvix b/tests/VampIR/positive/Compilation/test004.juvix index f7ccba2faf..fd9c589d7e 100644 --- a/tests/VampIR/positive/Compilation/test004.juvix +++ b/tests/VampIR/positive/Compilation/test004.juvix @@ -1,28 +1,38 @@ -- arithmetic module test004; -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; -func : Nat -> Nat := λ{x := x + 4}; +func : Nat -> Nat := λ {x := x + 4}; vx : Nat := 30; + vy : Nat := 7; -main : Nat -> Nat -> Nat -> Nat -> Nat; -main x y z u := - sub - (func (div y x) + -- 17 div 5 + 4 = 7 - (z * x + y) + -- 17 - (vx + vy * (z + 1)) + -- 37 - f (h g u 3) 4) -- 16 - 45; +main : Nat -> Nat -> Nat -> Nat -> Nat + | x y z u := + sub + (func (div y x) + + -- 17 div 5 + 4 = 7 + (z + * x + + y) + + -- 17 + (vx + + vy * (z + 1)) + + -- 37 + f + (h g u 3) + 4) + -- 16 + 45; -- result: 32 diff --git a/tests/VampIR/positive/Compilation/test005.juvix b/tests/VampIR/positive/Compilation/test005.juvix index bf00d392d5..81f5b476ec 100644 --- a/tests/VampIR/positive/Compilation/test005.juvix +++ b/tests/VampIR/positive/Compilation/test005.juvix @@ -1,15 +1,16 @@ -- single-constructor inductive types module test005; -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 -> Nat -> Nat; -main x y := case box (box2 x y) - | box (box2 x y) := x + y; +main : Nat -> Nat -> Nat + | x y := + case box (box2 x y) + | box (box2 x y) := x + y; -- result: 8 diff --git a/tests/VampIR/positive/Compilation/test006.juvix b/tests/VampIR/positive/Compilation/test006.juvix index c579674e43..115d7b96e5 100644 --- a/tests/VampIR/positive/Compilation/test006.juvix +++ b/tests/VampIR/positive/Compilation/test006.juvix @@ -1,25 +1,29 @@ -- higher-order inductive types module test006; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord 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; -natToBool : Nat -> Bool; -natToBool x := if (x == 0) false true; +natToBool : Nat -> Bool + | x := if (x == 0) false true; -boolToNat : Bool -> Nat; -boolToNat x := if x 1 0; +boolToNat : Bool -> Nat + | x := if x 1 0; -main : Nat -> Nat -> Nat; -main x y := boolToNat $ - case (opt3 (natToBool x) (λ{ x y := if y false x }) (natToBool y)) - | opt0 := false - | opt1 b := b - | opt2 b f := f b - | opt3 b1 f b2 := f b1 b2; +main : Nat -> Nat -> Nat + | x y := + boolToNat + $ case opt3 + (natToBool x) + λ {x y := if y false x} + (natToBool y) + | opt0 := false + | opt1 b := b + | opt2 b f := f b + | opt3 b1 f b2 := f b1 b2; diff --git a/tests/VampIR/positive/Compilation/test007.juvix b/tests/VampIR/positive/Compilation/test007.juvix index 66ec0484c4..dd2444e7ff 100644 --- a/tests/VampIR/positive/Compilation/test007.juvix +++ b/tests/VampIR/positive/Compilation/test007.juvix @@ -1,13 +1,27 @@ -- let module test007; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Nat -> Nat -> Nat; -main a b := - let x : Nat := a in - let x1 : Nat := x + let x2 : Nat := 2 in x2 in - let x3 : Nat := x1 * x1 in - let y : Nat := x3 + b in -- 11 - let z : Nat := x3 + y in -- 20 - x + y + z; +main : Nat -> Nat -> Nat + | a b := + let + x : Nat := a; + in let + x1 : + Nat := + x + + let + x2 : Nat := 2; + in x2; + in let + x3 : Nat := x1 * x1; + in let + y : Nat := x3 + b; + in -- 11 + let + z : Nat := x3 + y; + in -- 20 + x + + y + + z; diff --git a/tests/VampIR/positive/Compilation/test008.juvix b/tests/VampIR/positive/Compilation/test008.juvix index 281e90a4f4..ba643ef029 100644 --- a/tests/VampIR/positive/Compilation/test008.juvix +++ b/tests/VampIR/positive/Compilation/test008.juvix @@ -1,21 +1,18 @@ -- functions returning functions with variable capture module test008; -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 : Nat -> Nat -> Nat; -main x y := - f x (x + 1) + - f (x + 1) x + - f y x + - f (y + 1) x; +main : Nat -> Nat -> Nat + | x y := f x (x + 1) + f (x + 1) x + f y x + f (y + 1) x; diff --git a/tests/VampIR/positive/Compilation/test009.juvix b/tests/VampIR/positive/Compilation/test009.juvix index 2386ed02f0..ddc018fca4 100644 --- a/tests/VampIR/positive/Compilation/test009.juvix +++ b/tests/VampIR/positive/Compilation/test009.juvix @@ -1,21 +1,23 @@ -- applications with lets and cases in function position module test009; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -f : Nat -> ((Nat -> Nat) -> Nat -> Nat) × Nat → Nat; -f a l := (case l - | (x, zero) := x - | _ := id) - (let - y : Nat → Nat; - y := id; +f : Nat -> ((Nat -> Nat) -> Nat -> Nat) × Nat → Nat + | a l := + (case l + | x, zero := x + | _ := id) + (let + y : Nat → Nat := id; in (let - z : (Nat → Nat) → Nat → Nat; - z := id; - in (case l | (_, zero) := id | _ := id) z) - y) - a; + z : (Nat → Nat) → Nat → Nat := id; + in (case l + | _, zero := id + | _ := id) + z) + y) + a; -main : Nat -> Nat -> Nat -> Nat; -main a b c := f a (λ{| x y := x y + b}, c); +main : Nat -> Nat -> Nat -> Nat + | a b c := f a (λ {| x y := x y + b}, c); diff --git a/tests/VampIR/positive/Compilation/test010.juvix b/tests/VampIR/positive/Compilation/test010.juvix index 72b724ed22..d7b2a64867 100644 --- a/tests/VampIR/positive/Compilation/test010.juvix +++ b/tests/VampIR/positive/Compilation/test010.juvix @@ -1,8 +1,8 @@ -- mid-square hashing (unrolled) module test010; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; pow0 : Nat := 1; @@ -38,70 +38,69 @@ pow15 : Nat := 2 * pow14; pow16 : Nat := 2 * pow15; -hash0 : Nat -> Nat; -hash0 x := 0; +hash0 : Nat -> Nat + | x := 0; -hash1 : Nat -> Nat; -hash1 x := x * x; +hash1 : Nat -> Nat + | x := x * x; -hash2 : Nat -> Nat; -hash2 x := x * x; +hash2 : Nat -> Nat + | x := x * x; -hash3 : Nat -> Nat; -hash3 x := x * x; +hash3 : Nat -> Nat + | x := x * x; -hash4 : Nat -> Nat; -hash4 x := - if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6); +hash4 : Nat -> Nat + | x := + if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6); -hash5 : Nat -> Nat; -hash5 x := - if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6); +hash5 : Nat -> Nat + | x := + if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6); -hash6 : Nat -> Nat; -hash6 x := - if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6); +hash6 : Nat -> Nat + | x := + if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6); -hash7 : Nat -> Nat; -hash7 x := - if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6); +hash7 : Nat -> Nat + | x := + if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6); -hash8 : Nat -> Nat; -hash8 x := - if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6); +hash8 : Nat -> Nat + | x := + if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6); -hash9 : Nat -> Nat; -hash9 x := - if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6); +hash9 : Nat -> Nat + | x := + if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6); -hash10 : Nat -> Nat; -hash10 x := - if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6); +hash10 : Nat -> Nat + | x := + if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6); -hash11 : Nat -> Nat; -hash11 x := - if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6); +hash11 : Nat -> Nat + | x := + if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6); -hash12 : Nat -> Nat; -hash12 x := - if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6); +hash12 : Nat -> Nat + | x := + if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6); -hash13 : Nat -> Nat; -hash13 x := - if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6); +hash13 : Nat -> Nat + | x := + if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6); -hash14 : Nat -> Nat; -hash14 x := - if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6); +hash14 : Nat -> Nat + | x := + if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6); -hash15 : Nat -> Nat; -hash15 x := - if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6); +hash15 : Nat -> Nat + | x := + if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6); -hash16 : Nat -> Nat; -hash16 x := - if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6); +hash16 : Nat -> Nat + | x := + if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6); {-# argnames: [val] #-} -main : Nat -> Nat; -main := hash16; +main : Nat -> Nat := hash16; diff --git a/tests/VampIR/positive/Compilation/test011.juvix b/tests/VampIR/positive/Compilation/test011.juvix index 024f4c6c0d..ae11e30c6b 100644 --- a/tests/VampIR/positive/Compilation/test011.juvix +++ b/tests/VampIR/positive/Compilation/test011.juvix @@ -1,12 +1,11 @@ -- recursion module test011; -open import Stdlib.Prelude; +import Stdlib.Prelude open; {-# unroll: 11 #-} -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 : Nat -> Nat; -main := sum; +main : Nat -> Nat := sum; diff --git a/tests/VampIR/positive/Compilation/test012.juvix b/tests/VampIR/positive/Compilation/test012.juvix index 6b19b4544f..a2afee2a01 100644 --- a/tests/VampIR/positive/Compilation/test012.juvix +++ b/tests/VampIR/positive/Compilation/test012.juvix @@ -1,15 +1,13 @@ -- tail recursion module test012; -open import Stdlib.Prelude; +import Stdlib.Prelude open; {-# unroll: 11 #-} -sum' : Nat → Nat → Nat; -sum' acc zero := acc; -sum' acc (suc x) := sum' (suc x + acc) x; +sum' : Nat → Nat → Nat + | acc zero := acc + | acc (suc x) := sum' (suc x + acc) x; -sum : Nat → Nat; -sum := sum' 0; +sum : Nat → Nat := sum' 0; -main : Nat -> Nat; -main := sum; +main : Nat -> Nat := sum; diff --git a/tests/VampIR/positive/Compilation/test013.juvix b/tests/VampIR/positive/Compilation/test013.juvix index d295af4126..a0bd32b98d 100644 --- a/tests/VampIR/positive/Compilation/test013.juvix +++ b/tests/VampIR/positive/Compilation/test013.juvix @@ -1,15 +1,13 @@ -- tail recursion: Fibonacci numbers in linear time module test013; -open import Stdlib.Prelude; +import Stdlib.Prelude open; {-# unroll: 11 #-} -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 : Nat -> Nat; -main := fib; +main : Nat -> Nat := fib; diff --git a/tests/VampIR/positive/Compilation/test014.juvix b/tests/VampIR/positive/Compilation/test014.juvix index 7068842333..26cb552e59 100644 --- a/tests/VampIR/positive/Compilation/test014.juvix +++ b/tests/VampIR/positive/Compilation/test014.juvix @@ -1,16 +1,15 @@ -- recursion through higher-order functions module test014; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -g : (Nat → Nat) → Nat → Nat; -g f zero := 0; -g f (suc x) := f x; +g : (Nat → Nat) → Nat → Nat + | f zero := 0 + | f (suc x) := f x; {-# unroll: 11 #-} terminating -f : Nat → Nat; -f x := x + g f x; +f : Nat → Nat + | x := x + g f x; -main : Nat -> Nat; -main := f; +main : Nat -> Nat := f; diff --git a/tests/VampIR/positive/Compilation/test015.juvix b/tests/VampIR/positive/Compilation/test015.juvix index b7314621b4..b7d472c329 100644 --- a/tests/VampIR/positive/Compilation/test015.juvix +++ b/tests/VampIR/positive/Compilation/test015.juvix @@ -1,19 +1,17 @@ -- tail recursion through higher-order functions module test015; -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 : Nat → (Nat → Nat → Nat) → Nat → Nat + | acc f zero := acc + | acc f (suc x) := f acc x; {-# unroll: 11 #-} terminating -sum' : Nat → Nat → Nat; -sum' acc x := sumb (x + acc) sum' x; +sum' : Nat → Nat → Nat + | acc x := sumb (x + acc) sum' x; -sum : Nat → Nat; -sum := sum' 0; +sum : Nat → Nat := sum' 0; -main : Nat -> Nat; -main := sum; +main : Nat -> Nat := sum; diff --git a/tests/VampIR/positive/Compilation/test016.juvix b/tests/VampIR/positive/Compilation/test016.juvix index f6abdb85a4..2b732f6ca8 100644 --- a/tests/VampIR/positive/Compilation/test016.juvix +++ b/tests/VampIR/positive/Compilation/test016.juvix @@ -1,16 +1,15 @@ -- higher-order functions module test016; -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 → Nat; -u x y := f (h y) + x; +u : Nat → Nat → Nat + | x y := f (h y) + x; -main : Nat → Nat → Nat; -main := u; +main : Nat → Nat → Nat := u; diff --git a/tests/VampIR/positive/Compilation/test017.juvix b/tests/VampIR/positive/Compilation/test017.juvix index 1405795973..102f98154f 100644 --- a/tests/VampIR/positive/Compilation/test017.juvix +++ b/tests/VampIR/positive/Compilation/test017.juvix @@ -1,20 +1,31 @@ -- mutual recursion module test017; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; {-# unroll: 11 #-} terminating -f : Nat → Nat; -terminating -g : Nat → Nat; +f : Nat → Nat + + | x := + case x + | zero := 1 + | suc y := 2 * x + g y; + terminating -h : Nat → Nat; +g : Nat → Nat + | x := + case x + | zero := 1 + | suc y := x + h y; -f x := case x | zero := 1 | suc y := 2 * x + g y; -g x := case x | zero := 1 | suc y := x + h y; -h x := case x | zero := 1 | suc y := x * f y; +terminating +h : Nat → Nat + | x := + case x + | zero := 1 + | suc y := x * f y; -main : Nat → Nat; -main x := f x + f (2 * x); +main : Nat → Nat + | x := f x + f (2 * x); diff --git a/tests/VampIR/positive/Compilation/test018.juvix b/tests/VampIR/positive/Compilation/test018.juvix index 1cdaaf7a5d..9724065eaf 100644 --- a/tests/VampIR/positive/Compilation/test018.juvix +++ b/tests/VampIR/positive/Compilation/test018.juvix @@ -1,22 +1,21 @@ -- mid-square hashing module test018; -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; -pow : Nat -> Nat; -pow zero := 1; -pow (suc n) := 2 * pow n; +pow : Nat -> Nat + | zero := 1 + | (suc n) := 2 * pow n; -hash' : Nat -> Nat -> Nat; -hash' (suc n@(suc (suc m))) x := - if - (x < pow n) - (hash' n x) - (mod (div (x * x) (pow m)) (pow 6)); -hash' _ x := x * x; +hash' : Nat -> Nat -> Nat + | (suc n@(suc (suc m))) x := + if + (x < pow n) + (hash' n x) + (mod (div (x * x) (pow m)) (pow 6)) + | _ x := x * x; hash : Nat -> Nat := hash' 16; -main : Nat -> Nat; -main := hash; +main : Nat -> Nat := hash; diff --git a/tests/VampIR/positive/Compilation/test019.juvix b/tests/VampIR/positive/Compilation/test019.juvix index bbdbf29b25..eed14dfaf6 100644 --- a/tests/VampIR/positive/Compilation/test019.juvix +++ b/tests/VampIR/positive/Compilation/test019.juvix @@ -1,9 +1,10 @@ -- polymorphism module test019; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -main : Nat -> Nat -> Nat; -main x y := case tail (id (x :: y :: nil)) - | nil := 0 - | h :: _ := h; +main : Nat -> Nat -> Nat + | x y := + case tail (id (x :: y :: nil)) + | nil := 0 + | h :: _ := h; diff --git a/tests/VampIR/positive/Compilation/test020.juvix b/tests/VampIR/positive/Compilation/test020.juvix index 30f3240e7b..877a305e7b 100644 --- a/tests/VampIR/positive/Compilation/test020.juvix +++ b/tests/VampIR/positive/Compilation/test020.juvix @@ -4,9 +4,9 @@ module test020; import Stdlib.Prelude open; {-# unroll: 10 #-} -compose : {A : Type} → Nat → (A → A) → A → A; -compose zero _ := id; -compose (suc n) f := f ∘ compose n f; +compose : {A : Type} → Nat → (A → A) → A → A + | zero _ := id + | (suc n) f := f ∘ compose n f; -main : Nat → Bool → Bool; -main n b := compose n not b; +main : Nat → Bool → Bool + | n b := compose n not b; diff --git a/tests/VampIR/positive/Compilation/test021.juvix b/tests/VampIR/positive/Compilation/test021.juvix index d39440c694..5bdba00afe 100644 --- a/tests/VampIR/positive/Compilation/test021.juvix +++ b/tests/VampIR/positive/Compilation/test021.juvix @@ -4,13 +4,11 @@ module test021; import Stdlib.Prelude open; import Stdlib.Data.Nat.Ord open; -power : Nat → Nat → Nat; -power := +power : Nat → Nat → Nat := let {-# unroll: 4 #-} terminating - power' : Nat → Nat → Nat → Nat; - power' acc a b := + power' (acc a b : Nat) : Nat := if (b == 0) acc @@ -20,5 +18,4 @@ power := (power' (acc * a) (a * a) (div b 2))); in power' 1; -main : Nat -> Nat -> Nat; -main := power; +main : Nat -> Nat -> Nat := power; diff --git a/tests/VampIR/positive/Compilation/test022.juvix b/tests/VampIR/positive/Compilation/test022.juvix index a79eb9a109..7105ee3a2e 100644 --- a/tests/VampIR/positive/Compilation/test022.juvix +++ b/tests/VampIR/positive/Compilation/test022.juvix @@ -4,17 +4,14 @@ module test022; import Stdlib.Prelude open; import Stdlib.Data.Nat.Ord open; -power : Nat → Nat → Nat; -power := +power : Nat → Nat → Nat := let {-# unroll: 10 #-} terminating - power' : Nat → Nat → Nat → Nat; - power' acc a b := + power' (acc a b : Nat) : Nat := let acc' : Nat := if (mod b 2 == 0) acc (acc * a); in if (b == 0) acc (power' acc' (a * a) (div b 2)); in power' 1; -main : Nat -> Nat -> Nat; -main := power; +main : Nat -> Nat -> Nat := power; diff --git a/tests/VampIR/positive/Compilation/test023.juvix b/tests/VampIR/positive/Compilation/test023.juvix index 17c86898f3..d4e487ca6c 100644 --- a/tests/VampIR/positive/Compilation/test023.juvix +++ b/tests/VampIR/positive/Compilation/test023.juvix @@ -4,6 +4,7 @@ module test023; import Stdlib.Prelude open; import Stdlib.Data.Nat.Ord open; -main : Nat → Nat → Nat; -main x y := case (λ { z := if (x == z) (x, 0) (x, z) } (y + x)) - | (a, b) := a + b +main : Nat → Nat → Nat + | x y := + case λ {z := if (x == z) (x, 0) (x, z)} (y + x) + | a, b := a + b; diff --git a/tests/benchmark/ackermann/juvix/ackermann.juvix b/tests/benchmark/ackermann/juvix/ackermann.juvix index 4294979b1d..48ecdace3f 100644 --- a/tests/benchmark/ackermann/juvix/ackermann.juvix +++ b/tests/benchmark/ackermann/juvix/ackermann.juvix @@ -1,18 +1,17 @@ -- Ackermann function (higher-order definition) module ackermann; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - iter : {A : Type} → (A → A) → Nat → A → A; - iter f zero := id; - iter f (suc n) := f ∘ iter f n; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - step : (Nat → Nat) → Nat → Nat; - step f n := iter f (suc n) 1; +iter : {A : Type} → (A → A) → Nat → A → A + | f zero := id + | f (suc n) := f ∘ iter f n; - ackermann : Nat → Nat → Nat; - ackermann m := iter step m suc; +step : (Nat → Nat) → Nat → Nat + | f n := iter f (suc n) 1; - main : IO; - main := printNatLn (ackermann 3 11); -end; +ackermann : Nat → Nat → Nat + | m := iter step m suc; + +main : IO := printNatLn (ackermann 3 11); diff --git a/tests/benchmark/combinations/juvix/combinations.juvix b/tests/benchmark/combinations/juvix/combinations.juvix index d01a9dce2c..6a3c752b64 100644 --- a/tests/benchmark/combinations/juvix/combinations.juvix +++ b/tests/benchmark/combinations/juvix/combinations.juvix @@ -1,20 +1,20 @@ -- count combinations of numbers 1 to N having sum N module combinations; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - terminating - go : Nat → Nat → Nat; - go _ zero := 1; - go zero _ := 0; - go n s := if - (s < n) - (go (sub n 1) s) - (go n (sub s n) + go (sub n 1) s); +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - combinations : Nat → Nat; - combinations n := go n n; +terminating +go : Nat → Nat → Nat + | _ zero := 1 + | zero _ := 0 + | n s := + if + (s < n) + (go (sub n 1) s) + (go n (sub s n) + go (sub n 1) s); - main : IO; - main := printNatLn (combinations 100); -end; +combinations : Nat → Nat + | n := go n n; + +main : IO := printNatLn (combinations 100); diff --git a/tests/benchmark/cps/juvix/cps.juvix b/tests/benchmark/cps/juvix/cps.juvix index 5705c64607..9942c7fb29 100644 --- a/tests/benchmark/cps/juvix/cps.juvix +++ b/tests/benchmark/cps/juvix/cps.juvix @@ -1,19 +1,18 @@ -- compute the Nth Fibonacci number modulo 2 ^ 28 with CPS module cps; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - step : Nat → Nat → Nat → (Nat → Nat → Nat → Nat) → Nat; - step zero n _ _ := n; - step (suc k) n m cont := cont k m (mod (n + m) 268435456); +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - terminating - go : Nat → Nat → Nat → Nat; - go k n m := step k n m go; +step : Nat → Nat → Nat → (Nat → Nat → Nat → Nat) → Nat + | zero n _ _ := n + | (suc k) n m cont := cont k m (mod (n + m) 268435456); - fib : Nat → Nat; - fib n := go n 0 1; +terminating +go : Nat → Nat → Nat → Nat + | k n m := step k n m go; - main : IO; - main := printNatLn (fib 100000000); -end; +fib : Nat → Nat + | n := go n 0 1; + +main : IO := printNatLn (fib 100000000); diff --git a/tests/benchmark/fibonacci/juvix/fibonacci.juvix b/tests/benchmark/fibonacci/juvix/fibonacci.juvix index 6debae0711..f4d3419f1a 100644 --- a/tests/benchmark/fibonacci/juvix/fibonacci.juvix +++ b/tests/benchmark/fibonacci/juvix/fibonacci.juvix @@ -1,15 +1,14 @@ -- compute the Nth Fibonacci number modulo 2^28 module fibonacci; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - go : Nat → Nat → Nat → Nat; - go zero n _ := n; - go (suc k) n m := go k m (mod (n + m) 268435456); +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - fib : Nat → Nat; - fib n := go n 0 1; +go : Nat → Nat → Nat → Nat + | zero n _ := n + | (suc k) n m := go k m (mod (n + m) 268435456); - main : IO; - main := printNatLn (fib 100000000); -end; +fib : Nat → Nat + | n := go n 0 1; + +main : IO := printNatLn (fib 100000000); diff --git a/tests/benchmark/fold/juvix/fold.juvix b/tests/benchmark/fold/juvix/fold.juvix index 2d8dd3b95e..51f2d3a978 100644 --- a/tests/benchmark/fold/juvix/fold.juvix +++ b/tests/benchmark/fold/juvix/fold.juvix @@ -1,19 +1,18 @@ -- fold a list of N integers module fold; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - plusMod : Nat → Nat → Nat; - plusMod x y := mod (x + y) 268435456; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - run : Nat → Nat → List Nat → Nat; - run zero acc lst := foldl plusMod acc lst; - run (suc n) acc lst := run n (foldl plusMod acc lst) lst; +plusMod : Nat → Nat → Nat + | x y := mod (x + y) 268435456; - gen : Nat → List Nat → List Nat; - gen zero acc := acc; - gen (suc n) acc := gen n (suc n :: acc); +run : Nat → Nat → List Nat → Nat + | zero acc lst := foldl plusMod acc lst + | (suc n) acc lst := run n (foldl plusMod acc lst) lst; - main : IO; - main := printNatLn (run 1000 0 (gen 100000 nil)); -end; +gen : Nat → List Nat → List Nat + | zero acc := acc + | (suc n) acc := gen n (suc n :: acc); + +main : IO := printNatLn (run 1000 0 (gen 100000 nil)); diff --git a/tests/benchmark/mapfold/juvix/mapfold.juvix b/tests/benchmark/mapfold/juvix/mapfold.juvix index 0ee686d0c2..247e1ae7a3 100644 --- a/tests/benchmark/mapfold/juvix/mapfold.juvix +++ b/tests/benchmark/mapfold/juvix/mapfold.juvix @@ -1,19 +1,16 @@ -- map and fold a list of N integers K times module mapfold; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - run : Nat → Nat → List Nat → Nat; - run zero acc lst := acc; - run (suc n) acc lst := run - n - (sub (foldl (+) 0 lst) acc) - (map suc lst); +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - terminating - gen : Nat → Nat → List Nat; - gen k n := if (k == n) (k :: nil) (k :: gen (suc k) n); +run : Nat → Nat → List Nat → Nat + | zero acc lst := acc + | (suc n) acc lst := + run n (sub (foldl (+) 0 lst) acc) (map suc lst); - main : IO; - main := printNatLn (run 10000 0 (gen 1 10000)); -end; +terminating +gen : Nat → Nat → List Nat + | k n := if (k == n) (k :: nil) (k :: gen (suc k) n); + +main : IO := printNatLn (run 10000 0 (gen 1 10000)); diff --git a/tests/benchmark/mapfun/juvix/mapfun.juvix b/tests/benchmark/mapfun/juvix/mapfun.juvix index 2c61f8125f..7b35aae2bc 100644 --- a/tests/benchmark/mapfun/juvix/mapfun.juvix +++ b/tests/benchmark/mapfun/juvix/mapfun.juvix @@ -1,36 +1,35 @@ -- successively map K functions to a list of N integers module mapfun; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - mapfun : {A : Type} → List (A → A) → List A → List A; - mapfun nil xs := xs; - mapfun (f :: fs) xs := mapfun fs (map f xs); +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - genfs : Nat → List (Nat → Nat); - genfs zero := nil; - genfs (suc n) := sub (suc n) :: genfs n; +mapfun : {A : Type} → List (A → A) → List A → List A + | nil xs := xs + | (f :: fs) xs := mapfun fs (map f xs); - step : Nat → (Nat → Nat) → Nat → Nat; - step n f x := f (x + n); +genfs : Nat → List (Nat → Nat) + | zero := nil + | (suc n) := sub (suc n) :: genfs n; - genffs : Nat → List ((Nat → Nat) → Nat → Nat); - genffs zero := nil; - genffs (suc n) := step (suc n) :: genffs n; +step : Nat → (Nat → Nat) → Nat → Nat + | n f x := f (x + n); - sum_go : Nat → List Nat → Nat; - sum_go acc nil := acc; - sum_go acc (h :: t) := sum_go (acc + h) t; +genffs : Nat → List ((Nat → Nat) → Nat → Nat) + | zero := nil + | (suc n) := step (suc n) :: genffs n; - sum : List Nat → Nat; - sum := sum_go 0; +sum_go : Nat → List Nat → Nat + | acc nil := acc + | acc (h :: t) := sum_go (acc + h) t; - terminating - gen : Nat → Nat → List Nat; - gen k n := if (k == n) (k :: nil) (k :: gen (suc k) n); +sum : List Nat → Nat := sum_go 0; - main : IO; - main := printNatLn +terminating +gen : Nat → Nat → List Nat + | k n := if (k == n) (k :: nil) (k :: gen (suc k) n); + +main : IO := + printNatLn (sum (mapfun (mapfun (genffs 100) (genfs 100)) (gen 1 10000))); -end; diff --git a/tests/benchmark/maybe/juvix/maybe.juvix b/tests/benchmark/maybe/juvix/maybe.juvix index 2b222768d9..01b64a072f 100644 --- a/tests/benchmark/maybe/juvix/maybe.juvix +++ b/tests/benchmark/maybe/juvix/maybe.juvix @@ -1,58 +1,51 @@ -- optionally sum N integers from a binary tree K times module maybe; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - type Tree := - | leaf : Tree - | node : Nat → Tree → Tree → Tree; +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - mknode : Nat → Tree → Tree; - mknode n t := node n t t; +type Tree := + | leaf : Tree + | node : Nat → Tree → Tree → Tree; - gen : Nat → Tree; - gen zero := leaf; - gen (suc n) := mknode (suc n) (gen n); +mknode : Nat → Tree → Tree + | n t := node n t t; - terminating - sum : Nat → Tree → Maybe Nat; +gen : Nat → Tree + | zero := leaf + | (suc n) := mknode (suc n) (gen n); - step2 : Nat → Maybe Nat → Maybe Nat; +terminating +sum : Nat → Tree → Maybe Nat + + | x leaf := just 0 + | x (node y l r) := + if (x == y) nothing (step1 x y (sum x l) r); - terminating - step1 : Nat → Nat → Maybe Nat → Tree → Maybe Nat; - step1 x y (just s1) t := step2 (y + s1) (sum x t); - step1 _ _ nothing _ := nothing; +step2 : Nat → Maybe Nat → Maybe Nat + | x (just y) := just (x + y) + | _ nothing := nothing; - step2 x (just y) := just (x + y); - step2 _ nothing := nothing; +terminating +step1 : Nat → Nat → Maybe Nat → Tree → Maybe Nat + | x y (just s1) t := step2 (y + s1) (sum x t) + | _ _ nothing _ := nothing; - sum x leaf := just 0; - sum x (node y l r) := if - (x == y) - nothing - (step1 x y (sum x l) r); +maybeStepRun : Nat → Nat → Maybe Nat + | x y := just (sub y x); - maybeStepRun : Nat → Nat → Maybe Nat; - maybeStepRun x y := just (sub y x); +run : Nat → Tree → Maybe Nat + + | zero t := sum 0 t + | (suc n) t := stepRun (suc n) t (run n t); - run : Nat → Tree → Maybe Nat; +stepRun : Nat → Tree → Maybe Nat → Maybe Nat + + | n t nothing := sum n t + | n t (just x) := maybe nothing (maybeStepRun x) (sum n t); - stepRun : Nat → Tree → Maybe Nat → Maybe Nat; +printMaybeNat : Maybe Nat → IO + | (just x) := printNatLn x + | _ := printStringLn "nothing"; - run zero t := sum 0 t; - run (suc n) t := stepRun (suc n) t (run n t); - - stepRun n t nothing := sum n t; - stepRun n t (just x) := maybe - nothing - (maybeStepRun x) - (sum n t); - - printMaybeNat : Maybe Nat → IO; - printMaybeNat (just x) := printNatLn x; - printMaybeNat _ := printStringLn "nothing"; - - main : IO; - main := printMaybeNat (run 101 (gen 20)); -end; +main : IO := printMaybeNat (run 101 (gen 20)); diff --git a/tests/benchmark/mergesort/juvix/mergesort.juvix b/tests/benchmark/mergesort/juvix/mergesort.juvix index a6faaea7f2..8006ec93de 100644 --- a/tests/benchmark/mergesort/juvix/mergesort.juvix +++ b/tests/benchmark/mergesort/juvix/mergesort.juvix @@ -1,51 +1,52 @@ -- Merge sort a list of N integers module mergesort; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - - split_go : {A : Type} → List A → List A → List A → List A - × List A; - split_go nil ys zs := ys , zs; - split_go (x :: xs') ys zs := split_go xs' zs (x :: ys); - - split : {A : Type} → List A → List A × List A; - split xs := split_go xs nil nil; - - revappend : {A : Type} → List A → List A → List A; - revappend nil ys := ys; - revappend (x :: xs) ys := revappend xs (x :: ys); - - merget : List Nat → List Nat → List Nat → List Nat; - merget nil ys acc := revappend acc ys; - merget xs nil acc := revappend acc xs; - merget (x :: xs') (y :: ys') acc := if - (x <= y) - (merget xs' (y :: ys') (x :: acc)) - (merget (x :: xs') ys' (y :: acc)); - - terminating - sort' : List Nat × List Nat → List Nat; - - terminating - sort : List Nat → List Nat; - sort nil := nil; - sort (x :: nil) := x :: nil; - sort xs := sort' (split xs); - - sort' (l1 , l2) := merget (sort l1) (sort l2) nil; - - sorted : List Nat → Bool; - sorted nil := true; - sorted (_ :: nil) := true; - sorted (x :: y :: t) := if (x <= y) (sorted (y :: t)) false; - - gen : Nat → List Nat → List Nat; - gen zero acc := acc; - gen (suc n) acc := gen n (suc n :: acc); - - main : IO; - main := if + +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; + +split_go + : {A : Type} → List A → List A → List A → List A × List A + | nil ys zs := ys, zs + | (x :: xs') ys zs := split_go xs' zs (x :: ys); + +split : {A : Type} → List A → List A × List A + | xs := split_go xs nil nil; + +revappend : {A : Type} → List A → List A → List A + | nil ys := ys + | (x :: xs) ys := revappend xs (x :: ys); + +merget : List Nat → List Nat → List Nat → List Nat + | nil ys acc := revappend acc ys + | xs nil acc := revappend acc xs + | (x :: xs') (y :: ys') acc := + if + (x <= y) + (merget xs' (y :: ys') (x :: acc)) + (merget (x :: xs') ys' (y :: acc)); + +terminating +sort' : List Nat × List Nat → List Nat + + | (l1, l2) := merget (sort l1) (sort l2) nil; + +terminating +sort : List Nat → List Nat + | nil := nil + | (x :: nil) := x :: nil + | xs := sort' (split xs); + +sorted : List Nat → Bool + | nil := true + | (_ :: nil) := true + | (x :: y :: t) := if (x <= y) (sorted (y :: t)) false; + +gen : Nat → List Nat → List Nat + | zero acc := acc + | (suc n) acc := gen n (suc n :: acc); + +main : IO := + if (sorted (sort (gen 2000000 nil))) (printStringLn "true") (printStringLn "false"); -end; diff --git a/tests/benchmark/prime/juvix/prime.juvix b/tests/benchmark/prime/juvix/prime.juvix index 723aab93d9..d5a9150100 100644 --- a/tests/benchmark/prime/juvix/prime.juvix +++ b/tests/benchmark/prime/juvix/prime.juvix @@ -1,28 +1,25 @@ -- Compute the Nth prime module prime; - open import Stdlib.Prelude; - open import Stdlib.Data.Nat.Ord; - checkDivisible : Nat → List Nat → Bool; - checkDivisible p nil := false; - checkDivisible p (h :: t) := if - (mod p h == 0) - true - (checkDivisible p t); +import Stdlib.Prelude open; +import Stdlib.Data.Nat.Ord open; - terminating - go : Nat → Nat → List Nat → Nat; - go n p lst := if - (n == 0) - (head lst) - (if - (checkDivisible p lst) - (go n (p + 1) lst) - (go (sub n 1) (p + 1) (p :: lst))); +checkDivisible : Nat → List Nat → Bool + | p nil := false + | p (h :: t) := if (mod p h == 0) true (checkDivisible p t); - prime : Nat → Nat; - prime n := go n 2 nil; +terminating +go : Nat → Nat → List Nat → Nat + | n p lst := + if + (n == 0) + (head lst) + (if + (checkDivisible p lst) + (go n (p + 1) lst) + (go (sub n 1) (p + 1) (p :: lst))); - main : IO; - main := printNatLn (prime 16384); -end; +prime : Nat → Nat + | n := go n 2 nil; + +main : IO := printNatLn (prime 16384); diff --git a/tests/negative/230/Prod.juvix b/tests/negative/230/Prod.juvix index b21b2181ba..362e4f6b46 100644 --- a/tests/negative/230/Prod.juvix +++ b/tests/negative/230/Prod.juvix @@ -1,10 +1,9 @@ module Prod; -open import Stdlib.Prelude; -open import Foo; - import Foo.Data.Bool; +import Stdlib.Prelude open; +import Foo open; +import Foo.Data.Bool; -fi : Foo.Data.Bool; -fi := Foo.Data.Bool.false; +fi : Foo.Data.Bool := Foo.Data.Bool.false; end; diff --git a/tests/negative/AmbiguousConstructor.juvix b/tests/negative/AmbiguousConstructor.juvix index e54d48d38f..a58306ddc2 100644 --- a/tests/negative/AmbiguousConstructor.juvix +++ b/tests/negative/AmbiguousConstructor.juvix @@ -12,6 +12,6 @@ module AmbiguousConstructor; open M; open N; - f : T1 -> T2; - f A := N.A; + f : T1 -> T2 + | A := N.A; end; diff --git a/tests/negative/AsPatternAlias.juvix b/tests/negative/AsPatternAlias.juvix index da9da2d072..67d21e1648 100644 --- a/tests/negative/AsPatternAlias.juvix +++ b/tests/negative/AsPatternAlias.juvix @@ -1,6 +1,6 @@ module AsPatternAlias; -f : Type -> Type; -f a@b := b; +f : Type -> Type +| a@b := b; end; diff --git a/tests/negative/BindGroupConflict/Clause.juvix b/tests/negative/BindGroupConflict/Clause.juvix index 4e7533c3a8..296754cf47 100644 --- a/tests/negative/BindGroupConflict/Clause.juvix +++ b/tests/negative/BindGroupConflict/Clause.juvix @@ -3,7 +3,7 @@ module Clause; type Pair (a : Type) (b : Type) := mkPair : a → b → Pair a b; - fst : (a : Type) → (b : Type) → Pair a b → a ; - fst _ _ (mkPair _ _ x x) := x; + fst : (a : Type) → (b : Type) → Pair a b → a + | _ _ (mkPair _ _ x x) := x; end; diff --git a/tests/negative/BindGroupConflict/Lambda.juvix b/tests/negative/BindGroupConflict/Lambda.juvix index 87bf252df0..bdb133b84d 100644 --- a/tests/negative/BindGroupConflict/Lambda.juvix +++ b/tests/negative/BindGroupConflict/Lambda.juvix @@ -2,7 +2,6 @@ module Lambda; type Pair (a : Type) (b : Type) := mkPair : a → b → Pair a b; - fst : (a : Type) → (b : Type) → Pair a b → a ; - fst := λ { _ _ (mkPair _ _ x x) := x }; + fst : (a : Type) → (b : Type) → Pair a b → a := λ { _ _ (mkPair _ _ x x) := x }; end; diff --git a/tests/negative/InfixErrorP.juvix b/tests/negative/InfixErrorP.juvix index 69ba8c845c..93a8a4ead7 100644 --- a/tests/negative/InfixErrorP.juvix +++ b/tests/negative/InfixErrorP.juvix @@ -7,7 +7,7 @@ module InfixErrorP; type Pair := , : Type → Type → Pair; - fst : Pair → Type; - fst (x , ) := x; + fst : Pair → Type + | (x , ) := x; end; diff --git a/tests/negative/Iterators1.juvix b/tests/negative/Iterators1.juvix index 7686afe028..51cd1794d9 100644 --- a/tests/negative/Iterators1.juvix +++ b/tests/negative/Iterators1.juvix @@ -1,13 +1,12 @@ module Iterators1; syntax iterator map {init: 0}; -map : {A B : Type} → (A → B) → A → B; -map f x := f x; +map : {A B : Type} → (A → B) → A → B +| f x := f x; builtin bool type Bool := | true : Bool | false : Bool; -main : Bool; -main := map (y := false) (x in true) x; +main : Bool := map (y := false) (x in true) x; diff --git a/tests/negative/Iterators2.juvix b/tests/negative/Iterators2.juvix index 5b0ce5d747..2fae6c3c48 100644 --- a/tests/negative/Iterators2.juvix +++ b/tests/negative/Iterators2.juvix @@ -1,13 +1,12 @@ module Iterators2; syntax iterator bind {range: 1}; -bind : {A B : Type} → (A → B) → A → B; -bind f x := f x; +bind : {A B : Type} → (A → B) → A → B +| f x := f x; builtin bool type Bool := | true : Bool | false : Bool; -main : Bool; -main := bind (x in true; y in false) x; +main : Bool := bind (x in true; y in false) x; diff --git a/tests/negative/Iterators3.juvix b/tests/negative/Iterators3.juvix index 1fe533b541..08c4e487c0 100644 --- a/tests/negative/Iterators3.juvix +++ b/tests/negative/Iterators3.juvix @@ -1,12 +1,11 @@ module Iterators3; -map : {A B : Type} → (A → B) → A → B; -map f x := f x; +map : {A B : Type} → (A → B) → A → B +| f x := f x; builtin bool type Bool := | true : Bool | false : Bool; -main : Bool; -main := map (x in true) x; +main : Bool := map (x in true) x; diff --git a/tests/negative/Iterators4.juvix b/tests/negative/Iterators4.juvix index 408055c6ae..174049b7c8 100644 --- a/tests/negative/Iterators4.juvix +++ b/tests/negative/Iterators4.juvix @@ -2,13 +2,11 @@ module Iterators4; syntax iterator map; syntax iterator map {init: 0}; -map : {A B : Type} → (A → B) → A → B; -map f x := f x; +map {A B} (f : A → B) (x : A) : B := f x; builtin bool type Bool := | true : Bool | false : Bool; -main : Bool; -main := map (y := false) (x in true) x; +main : Bool := map (y := false) (x in true) x; diff --git a/tests/negative/Iterators5.juvix b/tests/negative/Iterators5.juvix index f86ec66edd..274f2e9e38 100644 --- a/tests/negative/Iterators5.juvix +++ b/tests/negative/Iterators5.juvix @@ -7,5 +7,4 @@ type Bool := | true : Bool | false : Bool; -main : Bool; -main := true; +main : Bool := true; diff --git a/tests/negative/LacksFunctionClause.juvix b/tests/negative/LacksFunctionClause.juvix deleted file mode 100644 index 3c1223f91b..0000000000 --- a/tests/negative/LacksFunctionClause.juvix +++ /dev/null @@ -1,3 +0,0 @@ -module LacksFunctionClause; - -id : Type → Type → Type; diff --git a/tests/negative/LacksTypeSig.juvix b/tests/negative/LacksTypeSig.juvix deleted file mode 100644 index 8f78b2bea0..0000000000 --- a/tests/negative/LacksTypeSig.juvix +++ /dev/null @@ -1,6 +0,0 @@ -module LacksTypeSig; - - some := Type; - - -end; diff --git a/tests/negative/LacksTypeSig2.juvix b/tests/negative/LacksTypeSig2.juvix deleted file mode 100644 index 7b812a3124..0000000000 --- a/tests/negative/LacksTypeSig2.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module LacksTypeSig2; - -open import Stdlib.Prelude; - - x : Nat; - - y : Nat; - y := let x := 1 in 3; - -end; diff --git a/tests/negative/LetMissingClause.juvix b/tests/negative/LetMissingClause.juvix deleted file mode 100644 index c1763db51b..0000000000 --- a/tests/negative/LetMissingClause.juvix +++ /dev/null @@ -1,7 +0,0 @@ -module LetMissingClause; - -id : {A : Type} → A → A - | {A} := - let - id' : A → A; - in id'; diff --git a/tests/negative/NestedAsPatterns.juvix b/tests/negative/NestedAsPatterns.juvix index e0bc2fbe24..299090d1c7 100644 --- a/tests/negative/NestedAsPatterns.juvix +++ b/tests/negative/NestedAsPatterns.juvix @@ -1,6 +1,6 @@ module NestedAsPatterns; -f : Type -> Type; -f a@b@_ := a; +f : Type -> Type +| a@b@_ := a; end; diff --git a/tests/negative/NestedPatternBraces.juvix b/tests/negative/NestedPatternBraces.juvix index eed23ef4fc..3b28c0abf1 100644 --- a/tests/negative/NestedPatternBraces.juvix +++ b/tests/negative/NestedPatternBraces.juvix @@ -1,6 +1,6 @@ module NestedPatternBraces; -a : {A : Type} → Type; -a {{A}} := a; +a : {A : Type} → Type +| {{A}} := a; end; diff --git a/tests/negative/NotARecord.juvix b/tests/negative/NotARecord.juvix index cdc8ca4f2a..d43f61d7a7 100644 --- a/tests/negative/NotARecord.juvix +++ b/tests/negative/NotARecord.juvix @@ -2,5 +2,4 @@ module NotARecord; type T := t; -f : T; -f := t @T{x := 1}; +f : T := t @T{x := 1}; diff --git a/tests/negative/PragmasFormat.juvix b/tests/negative/PragmasFormat.juvix index 3e3ce48a79..deed97aaf4 100644 --- a/tests/negative/PragmasFormat.juvix +++ b/tests/negative/PragmasFormat.juvix @@ -3,5 +3,4 @@ module PragmasFormat; open import Stdlib.Prelude; {-# inline: Tre #-} -main : Nat; -main := 0; +main : Nat := 0; diff --git a/tests/negative/PragmasYAML.juvix b/tests/negative/PragmasYAML.juvix index 4de5cdc5bd..beac15a6f4 100644 --- a/tests/negative/PragmasYAML.juvix +++ b/tests/negative/PragmasYAML.juvix @@ -3,5 +3,4 @@ module PragmasYAML; open import Stdlib.Prelude; {-# {inline: true, unroll: 500} #-} -main : Nat; -main := 0; +main : Nat := 0; diff --git a/tests/negative/StdlibConflict/Input.juvix b/tests/negative/StdlibConflict/Input.juvix index 0187348c7c..f86d774f8e 100644 --- a/tests/negative/StdlibConflict/Input.juvix +++ b/tests/negative/StdlibConflict/Input.juvix @@ -1,5 +1,5 @@ module Input; -open import Stdlib.Data.Bool; +import Stdlib.Data.Bool open; end; diff --git a/tests/negative/UnexpectedFieldUpdate.juvix b/tests/negative/UnexpectedFieldUpdate.juvix index ecee0e04f7..dfa7cacc00 100644 --- a/tests/negative/UnexpectedFieldUpdate.juvix +++ b/tests/negative/UnexpectedFieldUpdate.juvix @@ -6,5 +6,4 @@ type R := mkR { r : T; }; -f : R; -f := (mkR t) @R{x := 1}; +f : R := (mkR t) @R{x := 1}; diff --git a/tests/positive/Adt.juvix b/tests/positive/Adt.juvix index 7497453431..ffba13c8ba 100644 --- a/tests/positive/Adt.juvix +++ b/tests/positive/Adt.juvix @@ -11,17 +11,12 @@ type Nat := | zero | suc Nat; -c1 : Bool; -c1 := true; +c1 : Bool := true; -c2 : Bool; -c2 := false; +c2 : Bool := false; -c3 : Pair Bool Bool; -c3 := mkPair true false; +c3 : Pair Bool Bool := mkPair true false; -c4 : Nat; -c4 := zero; +c4 : Nat := zero; -c5 : Nat; -c5 := suc zero; +c5 : Nat := suc zero; diff --git a/tests/positive/FormatPragma.juvix b/tests/positive/FormatPragma.juvix index 3a35fb8d25..a5400bbcca 100644 --- a/tests/positive/FormatPragma.juvix +++ b/tests/positive/FormatPragma.juvix @@ -1,14 +1,13 @@ {-# format: false #-} module FormatPragma; -open import Stdlib.Prelude; +import Stdlib.Prelude open; -- Bam, bam! -- unformatted module -fun : {A B C D : Type} -> (A -> A) -> (B -> C -> D) -> (A -> B -> C) -> (D -> C -> C) -> A -> B -> C; -fun f g h i a b := +fun {A B C D} (f : A -> A) (g : B -> C -> D) (h : A -> B -> C) (i : D -> C -> C) (a : A) (b : B) : C := i (g b (h (f a) b)) (h a b); diff --git a/tests/positive/LambdaCalculus.juvix b/tests/positive/LambdaCalculus.juvix index a5a1e3a81a..11ec71dfe1 100644 --- a/tests/positive/LambdaCalculus.juvix +++ b/tests/positive/LambdaCalculus.juvix @@ -1,8 +1,8 @@ module LambdaCalculus; -LambdaTy : Type -> Type := Lambda; +LambdaTy : Type -> Type := Lambda; -AppTy : Type -> Type := App; +AppTy : Type -> Type := App; type Expr (V : Type) := | var : V -> Expr V diff --git a/tests/positive/MutualLet.juvix b/tests/positive/MutualLet.juvix index deae77efc6..93234cf54b 100644 --- a/tests/positive/MutualLet.juvix +++ b/tests/positive/MutualLet.juvix @@ -5,10 +5,10 @@ import Stdlib.Data.Bool open; main : _ := let - odd : _; - even : _; - odd zero := false; - odd (suc n) := not (even n); - even zero := true; - even (suc n) := not (odd n); + odd : _ + | zero := false + | (suc n) := not (even n); + even : _ + | zero := true + | (suc n) := not (odd n); in even 5; diff --git a/tests/positive/MutualType.juvix b/tests/positive/MutualType.juvix index b671b7e32c..8175ce2c14 100644 --- a/tests/positive/MutualType.juvix +++ b/tests/positive/MutualType.juvix @@ -11,7 +11,7 @@ type List (a : Type) := :: : a → List a → List a; Forest : Type -> Type - + | A := List (Tree A); --- N-Ary tree. diff --git a/tests/positive/OmitType.juvix b/tests/positive/OmitType.juvix index 37c3476f33..159c78d189 100644 --- a/tests/positive/OmitType.juvix +++ b/tests/positive/OmitType.juvix @@ -1,6 +1,8 @@ module OmitType; -type List A := nil | cons A (List A); +type List A := + | nil + | cons A (List A); map {A B} (f : A → B) : List A → List B | nil := nil diff --git a/tests/positive/Projections.juvix b/tests/positive/Projections.juvix index daab2c761f..bb677c142c 100644 --- a/tests/positive/Projections.juvix +++ b/tests/positive/Projections.juvix @@ -23,9 +23,9 @@ module M; p1 : RecA T (Maybe T) := mkRecA (arg := just - (mkRecB - (arg := mkRecA (arg := nothing; arg2 := t); arg2 := t)); - arg2 := t); + (mkRecB + (arg := mkRecA (arg := nothing; arg2 := t); arg2 := t)); + arg2 := t); end; p3 : T := M.RecA.arg2 M.p1; diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix index 89bb24cf96..bbfe290254 100644 --- a/tests/positive/Records.juvix +++ b/tests/positive/Records.juvix @@ -25,7 +25,7 @@ type EnumRecord := p2 : Pair EnumRecord EnumRecord := mkPair (fst := C1 (c1a := constructT; c1b := constructT); - snd := C2 (c2a := constructT; c2b := constructT)); + snd := C2 (c2a := constructT; c2b := constructT)); type newtype := | mknewtype {f : T}; diff --git a/tests/positive/Records2.juvix b/tests/positive/Records2.juvix index 1f34b74fa8..10eea1ab38 100644 --- a/tests/positive/Records2.juvix +++ b/tests/positive/Records2.juvix @@ -8,8 +8,7 @@ type Pair (A B : Type) := psnd : B }; -main : Pair Nat Nat; -main := +main : Pair Nat Nat := let p : Pair Nat Nat := mkPair 2 2; in p @Pair{pfst := pfst + psnd}; diff --git a/tests/positive/SignatureWithBody.juvix b/tests/positive/SignatureWithBody.juvix index 6c59876bf1..c88f949556 100644 --- a/tests/positive/SignatureWithBody.juvix +++ b/tests/positive/SignatureWithBody.juvix @@ -10,10 +10,9 @@ isNull : {A : Type} → List A → Bool := isNull' : {A : Type} → List A → Bool := let - aux : - {A : Type} → List A → Bool := - λ { - | nil := true - | _ := false - }; + aux : {A : Type} → List A → Bool := + λ { + | nil := true + | _ := false + }; in aux; diff --git a/tests/positive/StdlibList/Data/List.juvix b/tests/positive/StdlibList/Data/List.juvix index 81af5f3a4e..75ba0de7f5 100644 --- a/tests/positive/StdlibList/Data/List.juvix +++ b/tests/positive/StdlibList/Data/List.juvix @@ -44,9 +44,9 @@ length : (a : Type) → List a → ℕ reverse : (a : Type) → List a → List a | a l := let - rev : List a → List a → List a; - rev nil a := a; - rev (:: x xs) a := rev xs (:: x a); + rev : List a → List a → List a + | nil a := a + | (:: x xs) a := rev xs (:: x a); in rev l nil; replicate : (a : Type) → ℕ → a → List a @@ -100,16 +100,14 @@ quickSort | a _ (:: x nil) := :: x nil | a cmp (:: x ys) := let - ltx : a → Bool; - ltx y := + ltx (y : a) : Bool := match (cmp y x) λ { | LT := true | _ := false }; - gex : a → Bool; - gex y := not (ltx y); + gex (y : a) : Bool := not (ltx y); in ++ a (quickSort a cmp (filter a ltx ys)) diff --git a/tests/positive/issue1879/LetSynonym.juvix b/tests/positive/issue1879/LetSynonym.juvix index 5cff9095b8..2252069c92 100644 --- a/tests/positive/issue1879/LetSynonym.juvix +++ b/tests/positive/issue1879/LetSynonym.juvix @@ -5,8 +5,6 @@ type T := main : T := let - A : Type; - A := T; - x : A; - x := t; + A : Type := T; + x : A := t; in x; diff --git a/tests/positive/issue2248/Bug.juvix b/tests/positive/issue2248/Bug.juvix index b54c908c22..63ddc316d6 100644 --- a/tests/positive/issue2248/Bug.juvix +++ b/tests/positive/issue2248/Bug.juvix @@ -2,7 +2,6 @@ module Bug; type A := mkA : A; -aliasA : Type; -aliasA := A; +aliasA : Type := A; type C := mkC : aliasA -> C; diff --git a/tests/positive/issue2296/M.juvix b/tests/positive/issue2296/M.juvix index 7d5cd8f450..b77a65ee53 100644 --- a/tests/positive/issue2296/M.juvix +++ b/tests/positive/issue2296/M.juvix @@ -1,4 +1,4 @@ module M; -f : (F : Type → Type) → (A : Type) → F A → F A; -f _ _ x := x; +f : (F : Type → Type) → (A : Type) → F A → F A + | _ _ x := x; diff --git a/tests/smoke/Commands/dev/highlight.smoke.yaml b/tests/smoke/Commands/dev/highlight.smoke.yaml index ee9d0472da..168b794808 100644 --- a/tests/smoke/Commands/dev/highlight.smoke.yaml +++ b/tests/smoke/Commands/dev/highlight.smoke.yaml @@ -57,8 +57,7 @@ tests: import Stdlib.Prelude open; - main : Nat; - main := 5; + main : Nat := 5; stdout: contains: 'function' exit-status: 0 diff --git a/tests/smoke/Commands/dev/repl.smoke.yaml b/tests/smoke/Commands/dev/repl.smoke.yaml index 4dd2bdf1c4..60eb4f82b6 100644 --- a/tests/smoke/Commands/dev/repl.smoke.yaml +++ b/tests/smoke/Commands/dev/repl.smoke.yaml @@ -15,7 +15,7 @@ tests: - juvix - dev - repl - stdin: ":type let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10" + stdin: ":type let odd : _ | zero := false | (suc n) := not (even n); even : _ | zero := true | (suc n) := not (odd n) in even 10" stdout: contains: "Bool" @@ -26,7 +26,7 @@ tests: - juvix - dev - repl - stdin: "let even : Nat → Bool; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10" + stdin: "let odd : _ | zero := false | (suc n) := not (even n); even : Nat → Bool | zero := true | (suc n) := not (odd n) in even 10" stdout: contains: "true" @@ -155,7 +155,7 @@ tests: - juvix - dev - repl - stdin: "let x : Nat; x := 2 + 1 in x" + stdin: "let x : Nat := 2 + 1 in x" stdout: contains: "3" diff --git a/tests/smoke/Commands/format.smoke.yaml b/tests/smoke/Commands/format.smoke.yaml index 3832fd7f59..67970624db 100644 --- a/tests/smoke/Commands/format.smoke.yaml +++ b/tests/smoke/Commands/format.smoke.yaml @@ -272,15 +272,14 @@ tests: - --stdin - format - positive/Format.juvix - stdin: 'module Format; import Stdlib.Prelude open; main : Nat; main := 5; ' + stdin: 'module Format; import Stdlib.Prelude open; main : Nat := 5; ' stdout: contains: | module Format; import Stdlib.Prelude open; - main : Nat; - main := 5; + main : Nat := 5; exit-status: 0 - name: format-stdin-file-does-not-exist @@ -289,7 +288,7 @@ tests: - --stdin - format - positive/NonExistingFormat.juvix - stdin: 'module Format; import Stdlib.Prelude open; main : Nat; main := 5; ' + stdin: 'module Format; import Stdlib.Prelude open; main : Nat := 5; ' stderr: contains: | positive/NonExistingFormat.juvix" does not exist @@ -301,7 +300,7 @@ tests: - --stdin - format - positive/Format.juvix - stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5; ' + stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat := 5; ' stderr: contains: 'is defined in the file' exit-status: 1 @@ -311,22 +310,21 @@ tests: - juvix - --stdin - format - stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5; ' + stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat := 5; ' stdout: contains: | module OtherFormat; import Stdlib.Prelude open; - main : Nat; - main := 5; + main : Nat := 5; exit-status: 0 - name: format-no-stdin-no-file-name command: - juvix - format - stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5;; ' + stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat := 5module OtherFormat; import Stdlib.Prelude open; main : Nat := 5;; ' stdout: contains: juvix format error exit-status: 1 diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml index 2091a767e4..36e97d2ab1 100644 --- a/tests/smoke/Commands/repl.smoke.yaml +++ b/tests/smoke/Commands/repl.smoke.yaml @@ -94,7 +94,7 @@ tests: command: - juvix - repl - stdin: ":type let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10" + stdin: ":type let odd : _ | zero := false | (suc n) := not (even n); even : _ | zero := true | (suc n) := not (odd n) in even 10" stdout: contains: "Bool" @@ -104,7 +104,7 @@ tests: command: - juvix - repl - stdin: "let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10" + stdin: "let odd : _ | zero := false | (suc n) := not (even n); even : _ | zero := true | (suc n) := not (odd n) in even 10" stdout: contains: "true" @@ -223,7 +223,7 @@ tests: command: - juvix - repl - stdin: "let x : Nat; x := 2 + 1 in x" + stdin: "let x : Nat := 2 + 1 in x" stdout: contains: "3" @@ -446,15 +446,6 @@ tests: exit-status: 0 - name: open-import-from-stdlib - command: - - juvix - - repl - stdin: "open import Stdlib.Data.Int.Ord\n1 == 1" - stdout: - contains: "true" - exit-status: 0 - - - name: open-import-from-stdlib-new-syntax command: - juvix - repl