From 803d2008d9c58b6e4142db0d125e88c071e8af43 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Fri, 30 Sep 2022 02:55:32 +0200 Subject: [PATCH] =?UTF-8?q?remove=20=E2=89=94=20from=20the=20language=20an?= =?UTF-8?q?d=20replace=20it=20by=20:=3D=20(#1563)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * remove ≔ from the language and replace it by := * revert accidental changes in juvix input mode * update stdlib submodule * rename ℕ by Nat in the tests and examples * fix shell tests --- README.org | 2 +- .../backend-specific/minic-hello-world.org | 2 +- .../validity-predicates/PolyFungibleToken.org | 76 +++++------ docs/org/language-reference/builtins.org | 4 +- .../org/language-reference/foreign-blocks.org | 2 +- docs/org/language-reference/functions.org | 8 +- .../inductive-data-types.org | 8 +- docs/org/notes/builtins.org | 4 +- docs/org/notes/monomorphization.org | 24 ++-- docs/org/tutorials/nodejs-interop.org | 2 +- examples/milestone/Collatz/Collatz.juvix | 44 +++---- examples/milestone/Fibonacci/Fibonacci.juvix | 12 +- examples/milestone/Hanoi/Hanoi.juvix | 30 ++--- .../milestone/HelloWorld/HelloWorld.juvix | 2 +- .../PascalsTriangle/PascalsTriangle.juvix | 34 ++--- .../milestone/TicTacToe/CLI/TicTacToe.juvix | 22 ++-- .../milestone/TicTacToe/Logic/Board.juvix | 20 +-- .../milestone/TicTacToe/Logic/Extra.juvix | 8 +- examples/milestone/TicTacToe/Logic/Game.juvix | 14 +- .../milestone/TicTacToe/Logic/GameState.juvix | 10 +- .../milestone/TicTacToe/Logic/Square.juvix | 20 +-- .../milestone/TicTacToe/Logic/Symbol.juvix | 14 +- .../milestone/TicTacToe/Web/TicTacToe.juvix | 120 +++++++++--------- .../ValidityPredicates/Anoma/Base.juvix | 12 +- .../ValidityPredicates/Data/Int/Ops.juvix | 4 +- .../SimpleFungibleToken.juvix | 12 +- .../milestone/ValidityPredicates/Tests.juvix | 18 +-- juvix-stdlib | 2 +- .../Concrete/Translation/FromSource.hs | 3 +- .../Concrete/Translation/FromSource/Lexer.hs | 2 +- .../Core/Translation/FromSource/Lexer.hs | 2 +- src/Juvix/Data/CodeAnn.hs | 4 +- src/Juvix/Extra/Strings.hs | 3 - src/Juvix/Parser/Lexer.hs | 18 +-- tests/CLI/Commands/dev/internal.test | 2 +- tests/CLI/Commands/typecheck.test | 2 +- tests/Core/positive/lambda-lifting/test1.out | 4 +- tests/Core/positive/lambda-lifting/test2.out | 10 +- tests/Core/positive/lambda-lifting/test3.out | 10 +- tests/negative/230/Foo/Data/Bool.juvix | 16 +-- tests/negative/230/Prod.juvix | 2 +- tests/negative/265/M.juvix | 4 +- tests/negative/AmbiguousConstructor.juvix | 2 +- tests/negative/AppLeftImplicit.juvix | 2 +- tests/negative/BindGroupConflict/Clause.juvix | 2 +- tests/negative/BindGroupConflict/Lambda.juvix | 2 +- tests/negative/InfixErrorP.juvix | 2 +- .../Internal/ExpectedExplicitArgument.juvix | 2 +- .../Internal/ExpectedExplicitPattern.juvix | 2 +- .../Internal/ExpectedFunctionType.juvix | 2 +- tests/negative/Internal/FunctionApplied.juvix | 2 +- tests/negative/Internal/FunctionPattern.juvix | 2 +- .../Internal/LhsTooManyPatterns.juvix | 2 +- tests/negative/Internal/MultiWrongType.juvix | 4 +- .../Internal/PatternConstructor.juvix | 2 +- .../negative/Internal/TooManyArguments.juvix | 2 +- tests/negative/Internal/UnsolvedMeta.juvix | 2 +- .../Internal/WrongConstructorArity.juvix | 2 +- tests/negative/Internal/WrongType.juvix | 2 +- tests/negative/LacksTypeSig.juvix | 2 +- tests/negative/NestedPatternBraces.juvix | 2 +- tests/negative/Termination/Data/Bool.juvix | 16 +-- tests/negative/Termination/Data/Nat.juvix | 16 +-- .../negative/Termination/Data/QuickSort.juvix | 18 +-- tests/negative/issue1344/D.juvix | 2 +- tests/negative/issue1344/M.juvix | 2 +- tests/positive/265/M.juvix | 4 +- tests/positive/272/M.juvix | 6 +- .../MonoSimpleFungibleToken.juvix | 84 ++++++------ .../SimpleFungibleTokenImplicit.juvix | 76 +++++------ tests/positive/Imports/A.juvix | 2 +- tests/positive/Internal/Box.juvix | 6 +- tests/positive/Internal/HoleInSignature.juvix | 2 +- tests/positive/Internal/Implicit.juvix | 68 +++++----- tests/positive/Internal/Lambda.juvix | 4 +- tests/positive/Internal/LiteralInt.juvix | 4 +- tests/positive/Internal/LiteralString.juvix | 2 +- tests/positive/Internal/Mutual.juvix | 12 +- tests/positive/Internal/Simple.juvix | 18 +-- tests/positive/Judoc.juvix | 4 +- .../positive/MiniC/AlwaysValidVP/Input.juvix | 6 +- .../positive/MiniC/AxiomNoCompile/Input.juvix | 2 +- tests/positive/MiniC/Builtins/Input.juvix | 14 +- tests/positive/MiniC/ClosureEnv/Input.juvix | 40 +++--- tests/positive/MiniC/ClosureNoEnv/Input.juvix | 22 ++-- tests/positive/MiniC/ExportName/Input.juvix | 4 +- .../positive/MiniC/ExportNameArgs/Input.juvix | 4 +- tests/positive/MiniC/HelloWorld/Input.juvix | 2 +- tests/positive/MiniC/HigherOrder/Input.juvix | 28 ++-- .../MiniC/ImportExportName/Input.juvix | 2 +- tests/positive/MiniC/Lib/Data/Bool.juvix | 8 +- tests/positive/MiniC/Lib/Data/Nat.juvix | 8 +- tests/positive/MiniC/Lib/Data/Pair.juvix | 2 +- .../MiniC/MultiModules/Data/Bool.juvix | 8 +- .../MiniC/MultiModules/Data/Nat.juvix | 8 +- .../MiniC/MultiModules/Data/Pair.juvix | 2 +- tests/positive/MiniC/MultiModules/Input.juvix | 8 +- .../MiniC/MutuallyRecursive/Data/Bool.juvix | 8 +- .../MiniC/MutuallyRecursive/Data/Nat.juvix | 8 +- .../MiniC/MutuallyRecursive/Data/Pair.juvix | 2 +- .../MiniC/MutuallyRecursive/Input.juvix | 16 +-- tests/positive/MiniC/Nat/Input.juvix | 44 +++---- tests/positive/MiniC/NestedList/Input.juvix | 4 +- tests/positive/MiniC/Polymorphism/Input.juvix | 12 +- .../MiniC/PolymorphismHoles/Input.juvix | 10 +- .../SimpleFungibleTokenImplicit/Input.juvix | 78 ++++++------ tests/positive/MiniC/StdlibImport/Input.juvix | 2 +- tests/positive/MiniHaskell/HelloWorld.juvix | 14 +- tests/positive/Operators.juvix | 6 +- tests/positive/Parsing.juvix | 2 +- tests/positive/Polymorphism.juvix | 60 ++++----- tests/positive/PolymorphismHoles.juvix | 56 ++++---- tests/positive/QualifiedConstructor/M.juvix | 2 +- tests/positive/Reachability/Data/Bool.juvix | 12 +- tests/positive/Reachability/Data/Nat.juvix | 8 +- .../positive/StdlibImport/StdlibImport.juvix | 6 +- tests/positive/StdlibList/Data/Bool.juvix | 12 +- tests/positive/StdlibList/Data/List.juvix | 64 +++++----- tests/positive/StdlibList/Data/Nat.juvix | 8 +- tests/positive/Symbols.juvix | 34 ++--- tests/positive/Termination/Ack.juvix | 6 +- tests/positive/Termination/Data/Bool.juvix | 16 +-- tests/positive/Termination/Data/List.juvix | 38 +++--- tests/positive/Termination/Data/Nat.juvix | 16 +-- tests/positive/Termination/Fib.juvix | 4 +- tests/positive/TypeAlias.juvix | 16 +-- 126 files changed, 864 insertions(+), 866 deletions(-) diff --git a/README.org b/README.org index 8f09ead84..f1515ec09 100644 --- a/README.org +++ b/README.org @@ -126,7 +126,7 @@ module HelloWorld; open import Stdlib.Prelude; main : IO; -main ≔ putStrLn "hello world!"; +main := putStrLn "hello world!"; end; #+end_src diff --git a/docs/org/examples/backend-specific/minic-hello-world.org b/docs/org/examples/backend-specific/minic-hello-world.org index 450a7262f..cf07e594b 100755 --- a/docs/org/examples/backend-specific/minic-hello-world.org +++ b/docs/org/examples/backend-specific/minic-hello-world.org @@ -25,7 +25,7 @@ compile put-str-ln { }; main : Action; -main ≔ put-str-ln "hello world!"; +main := put-str-ln "hello world!"; end; #+end_src diff --git a/docs/org/examples/validity-predicates/PolyFungibleToken.org b/docs/org/examples/validity-predicates/PolyFungibleToken.org index 05069c966..6899afb26 100644 --- a/docs/org/examples/validity-predicates/PolyFungibleToken.org +++ b/docs/org/examples/validity-predicates/PolyFungibleToken.org @@ -19,17 +19,17 @@ inductive Bool { infixr 2 ||; || : Bool → Bool → Bool; -|| false a ≔ a; -|| true _ ≔ true; +|| false a := a; +|| true _ := true; infixr 3 &&; && : Bool → Bool → Bool; -&& false _ ≔ false; -&& true a ≔ a; +&& false _ := false; +&& true a := a; if : {A : Type} → Bool → A → A → A; -if true a _ ≔ a; -if false _ b ≔ b; +if true a _ := a; +if false _ b := b; -------------------------------------------------------------------------------- -- Backend Booleans @@ -67,14 +67,14 @@ compile bool { }; from-backend-bool : BackendBool → Bool; -from-backend-bool bb ≔ bool bb true false; +from-backend-bool bb := bool bb true false; -------------------------------------------------------------------------------- -- Functions -------------------------------------------------------------------------------- id : {A : Type} → A → A; -id a ≔ a; +id a := a; -------------------------------------------------------------------------------- -- Integers @@ -93,7 +93,7 @@ compile <' { infix 4 <; < : Int → Int → Bool; -< i1 i2 ≔ from-backend-bool (i1 <' i2); +< i1 i2 := from-backend-bool (i1 <' i2); axiom eqInt : Int → Int → BackendBool; compile eqInt { @@ -102,7 +102,7 @@ compile eqInt { infix 4 ==Int; ==Int : Int → Int → Bool; -==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2); +==Int i1 i2 := from-backend-bool (eqInt i1 i2); infixl 6 -; axiom - : Int -> Int -> Int; @@ -132,7 +132,7 @@ compile eqString { infix 4 ==String; ==String : String → String → Bool; -==String s1 s2 ≔ from-backend-bool (eqString s1 s2); +==String s1 s2 := from-backend-bool (eqString s1 s2); -------------------------------------------------------------------------------- -- Lists @@ -145,12 +145,12 @@ inductive List (A : Type) { }; elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil ≔ false; -elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs; +elem _ _ nil := false; +elem eq s (x ∷ xs) := eq s x || elem eq s xs; foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil ≔ z; -foldl f z (h ∷ hs) ≔ foldl f (f z h) hs; +foldl f z nil := z; +foldl f z (h ∷ hs) := foldl f (f z h) hs; -------------------------------------------------------------------------------- -- Pair @@ -172,17 +172,17 @@ inductive Maybe (A : Type) { }; from-int : Int → Maybe Int; -from-int i ≔ if (i < 0) nothing (just i); +from-int i := if (i < 0) nothing (just i); maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; -maybe b _ nothing ≔ b; -maybe _ f (just x) ≔ f x; +maybe b _ nothing := b; +maybe _ f (just x) := f x; from-string : String → Maybe String; -from-string s ≔ if (s ==String "") nothing (just s); +from-string s := if (s ==String "") nothing (just s); pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString ≔ maybe (0 , false); +pair-from-optionString := maybe (0 , false); -------------------------------------------------------------------------------- -- Anoma @@ -204,26 +204,26 @@ compile isBalanceKey { }; read-pre : String → Maybe Int; -read-pre s ≔ from-int (readPre s); +read-pre s := from-int (readPre s); read-post : String → Maybe Int; -read-post s ≔ from-int (readPost s); +read-post s := from-int (readPost s); is-balance-key : String → String → Maybe String; -is-balance-key token key ≔ from-string (isBalanceKey token key); +is-balance-key token key := from-string (isBalanceKey token key); unwrap-default : Maybe Int → Int; -unwrap-default ≔ maybe 0 id; +unwrap-default := maybe 0 id; -------------------------------------------------------------------------------- -- Validity Predicate -------------------------------------------------------------------------------- change-from-key : String → Int; -change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key); +change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner ≔ +check-vp verifiers key change owner := if (change-from-key key < 0) -- make sure the spender approved the transaction @@ -231,17 +231,17 @@ check-vp verifiers key change owner ≔ (change + (change-from-key key), true); check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change , is-success) key ≔ +check-keys token verifiers (change , is-success) key := if is-success (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) (0 , false); check-result : Int × Bool → Bool; -check-result (change , all-checked) ≔ (change ==Int 0) && all-checked; +check-result (change , all-checked) := (change ==Int 0) && all-checked; vp : String → List String → List String → Bool; -vp token keys-changed verifiers ≔ +vp token keys-changed verifiers := check-result (foldl (check-keys token verifiers) @@ -274,33 +274,33 @@ compile >> { }; show-result : Bool → String; -show-result true ≔ "OK"; -show-result false ≔ "FAIL"; +show-result true := "OK"; +show-result false := "FAIL"; -------------------------------------------------------------------------------- -- Testing VP -------------------------------------------------------------------------------- token : String; -token ≔ "owner-token"; +token := "owner-token"; owner-address : String; -owner-address ≔ "owner-address"; +owner-address := "owner-address"; change1-key : String; -change1-key ≔ "change1-key"; +change1-key := "change1-key"; change2-key : String; -change2-key ≔ "change2-key"; +change2-key := "change2-key"; verifiers : List String; -verifiers ≔ owner-address ∷ nil; +verifiers := owner-address ∷ nil; keys-changed : List String; -keys-changed ≔ change1-key ∷ change2-key ∷ nil; +keys-changed := change1-key ∷ change2-key ∷ nil; main : Action; -main ≔ +main := (putStr "VP Status: ") >> (putStrLn (show-result (vp token keys-changed verifiers))); diff --git a/docs/org/language-reference/builtins.org b/docs/org/language-reference/builtins.org index 628c89778..8e6efb818 100755 --- a/docs/org/language-reference/builtins.org +++ b/docs/org/language-reference/builtins.org @@ -19,8 +19,8 @@ Juvix has support for the built-in natural type and a few functions that are com inifl 6 +; builtin natural-plus + : Nat → Nat → Nat; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); #+end_example 3. Builtin axiom definitions. diff --git a/docs/org/language-reference/foreign-blocks.org b/docs/org/language-reference/foreign-blocks.org index 01e48bd71..d149ff546 100644 --- a/docs/org/language-reference/foreign-blocks.org +++ b/docs/org/language-reference/foreign-blocks.org @@ -32,5 +32,5 @@ compile <' { infix 4 <; < : Int → Int → Bool; -< a b ≔ from-backend-bool (a <' b); +< a b := from-backend-bool (a <' b); #+end_example diff --git a/docs/org/language-reference/functions.org b/docs/org/language-reference/functions.org index 217a1faac..fed4844ea 100644 --- a/docs/org/language-reference/functions.org +++ b/docs/org/language-reference/functions.org @@ -42,9 +42,9 @@ odd : Nat → Bool; even : Nat → Bool; -odd zero ≔ false; -odd (suc n) ≔ even n; +odd zero := false; +odd (suc n) := even n; -even zero ≔ true; -even (suc n) ≔ odd n; +even zero := true; +even (suc n) := odd n; #+end_example diff --git a/docs/org/language-reference/inductive-data-types.org b/docs/org/language-reference/inductive-data-types.org index b753ae523..a132e3a3f 100755 --- a/docs/org/language-reference/inductive-data-types.org +++ b/docs/org/language-reference/inductive-data-types.org @@ -30,8 +30,8 @@ Let us define, for example, the function for adding two natural numbers. #+begin_src text inifl 6 +; + : Nat → Nat → Nat; -+ zero b ≔ b; -+ (suc a) b ≔ suc (a + b); ++ zero b := b; ++ (suc a) b := suc (a + b); #+end_src As mentioned earlier, an inductive type may have type parameters. The canonical @@ -49,8 +49,8 @@ inductive List (A : Type) { }; elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil ≔ false; -elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs; +elem _ _ nil := false; +elem eq s (x ∷ xs) := eq s x || elem eq s xs; #+end_example To see more examples of inductive types and how to use them, please check out diff --git a/docs/org/notes/builtins.org b/docs/org/notes/builtins.org index bba13582b..fb77ba016 100644 --- a/docs/org/notes/builtins.org +++ b/docs/org/notes/builtins.org @@ -22,8 +22,8 @@ of definitions: inifl 6 +; builtin natural-plus + : Nat → Nat → Nat; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); #+end_src 3. Builtin axiom definitions. For example: diff --git a/docs/org/notes/monomorphization.org b/docs/org/notes/monomorphization.org index 15e6a34c0..e845f1068 100644 --- a/docs/org/notes/monomorphization.org +++ b/docs/org/notes/monomorphization.org @@ -10,22 +10,22 @@ Example: #+begin_src juvix id : (A : Type) → A → A; - id _ a ≔ a; + id _ a := a; b : Bool; - b ≔ id Bool true; + b := id Bool true; n : Nat; - n ≔ id Nat zero; + n := id Nat zero; #+end_src Is translated into: #+begin_src juvix id_Bool : Bool → Bool; - id_Bool a ≔ a; + id_Bool a := a; id_Nat : Nat → Nat; - id_Nat a ≔ a; + id_Nat a := a; #+end_src * More examples @@ -37,14 +37,14 @@ inductive List (A : Type) { }; even : (A : Type) → List A → Bool; -even A nil ≔ true ; -even A (cons _ xs) ≔ not (odd A xs) ; +even A nil := true ; +even A (cons _ xs) := not (odd A xs) ; odd : (A : Type) → List A → Bool; -odd A nil ≔ false ; -odd A (cons _ xs) ≔ not (even A xs) ; +odd A nil := false ; +odd A (cons _ xs) := not (even A xs) ; --- main ≔ even Bool .. odd Nat; +-- main := even Bool .. odd Nat; #+end_src * Collection algorithm @@ -158,7 +158,7 @@ list of concrete type applications involving =f=: =f â₁, …, f âₙ=. be the variables bound in =pₘ₊₁, …, pₖ=. Let =w'₁, …, w'ₛ= be fresh variables. Then let =δ = {w₁ ↦ w'₁, …, wₛ ↦ w'ₛ}=. - Now let =𝒞'= have patterns =δ(pₘ₊₁), …, δ(pₖ)= and let =e' ≔ (σ ∪ δ)(e)=. It + Now let =𝒞'= have patterns =δ(pₘ₊₁), …, δ(pₖ)= and let =e' := (σ ∪ δ)(e)=. It should be clear that =e'= has no type variables in it and that all local variable references in =e'= are among =w'₁, …, w'ₛ=. Note that =e'= is not yet monomorphized. Proceed to the next step to achieve that. @@ -172,7 +172,7 @@ list of concrete type applications involving =f=: =f â₁, …, f âₙ=. view of the application: =f a₁ … aₘ=. Then, if =f= is either a constructor, or a function, let =A₁, …, Aₖ= with =k ≤ m= be the list of type parameters of =f=. - If =f= is a function and =f a₁ … aₖ ∉ ℒ= then recurse normally, otherwise, - let =â ≔ a₁ … aₖ= and replace the original expression =f a₁ … aₘ=, by =⋆(f â) + let =â := a₁ … aₖ= and replace the original expression =f a₁ … aₘ=, by =⋆(f â) aₖ₊₁' … aₘ'= where =aₖ₊₁' … aₘ'= are the monomorphization of =aₖ₊₁ … aₘ= respectively. - If =f= is a constructor, let =d= be its inductive type. Then check =d a₁ … aₖ diff --git a/docs/org/tutorials/nodejs-interop.org b/docs/org/tutorials/nodejs-interop.org index 37589fe44..ecad4c2d7 100644 --- a/docs/org/tutorials/nodejs-interop.org +++ b/docs/org/tutorials/nodejs-interop.org @@ -27,7 +27,7 @@ open import Stdlib.Prelude; axiom hostDisplayString : String → IO; juvixRender : IO; -juvixRender ≔ hostDisplayString "Hello World from Juvix!"; +juvixRender := hostDisplayString "Hello World from Juvix!"; end; #+end_src diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix index dcdffa644..810611c35 100644 --- a/examples/milestone/Collatz/Collatz.juvix +++ b/examples/milestone/Collatz/Collatz.juvix @@ -3,21 +3,21 @@ module Collatz; open import Stdlib.Prelude; mapMaybe : {A : Type} → {B : Type} → (A → B) → Maybe A → Maybe B; -mapMaybe _ nothing ≔ nothing; -mapMaybe f (just x) ≔ just (f x); +mapMaybe _ nothing := nothing; +mapMaybe f (just x) := just (f x); -div2 : ℕ → Maybe ℕ; -div2 zero ≔ just zero; -div2 (suc (suc n)) ≔ mapMaybe suc (div2 n); -div2 _ ≔ nothing; +div2 : Nat → Maybe Nat; +div2 zero := just zero; +div2 (suc (suc n)) := mapMaybe suc (div2 n); +div2 _ := nothing; -collatzNext : ℕ → ℕ; -collatzNext n ≔ fromMaybe (suc (3 * n)) (div2 n); +collatzNext : Nat → Nat; +collatzNext n := fromMaybe (suc (3 * n)) (div2 n); -collatz : ℕ → ℕ; -collatz zero ≔ zero; -collatz (suc zero) ≔ suc zero; -collatz (suc (suc n)) ≔ collatzNext (suc (suc n)); +collatz : Nat → Nat; +collatz zero := zero; +collatz (suc zero) := suc zero; +collatz (suc (suc n)) := collatzNext (suc (suc n)); -------------------------------------------------------------------------------- -- IO @@ -28,27 +28,27 @@ compile readline { c ↦ "readline()"; }; -axiom parsePositiveInt : String → ℕ; +axiom parsePositiveInt : String → Nat; compile parsePositiveInt { c ↦ "parsePositiveInt"; }; -getInitial : ℕ; -getInitial ≔ parsePositiveInt (readline); +getInitial : Nat; +getInitial := parsePositiveInt (readline); -output : ℕ → ℕ × IO; -output n ≔ (n, putStrLn (natToStr n)); +output : Nat → Nat × IO; +output n := (n, putStrLn (natToStr n)); terminating -run : (ℕ → ℕ) → ℕ → IO; -run _ (suc zero) ≔ putStrLn "Finished!"; -run f n ≔ run f (fst (output (f n))); +run : (Nat → Nat) → Nat → IO; +run _ (suc zero) := putStrLn "Finished!"; +run f n := run f (fst (output (f n))); welcome : String; -welcome ≔ "Collatz calculator\n------------------\n\nType a number then ENTER"; +welcome := "Collatz calculator\n------------------\n\nType a number then ENTER"; main : IO; -main ≔ putStrLn welcome >> run collatz getInitial; +main := putStrLn welcome >> run collatz getInitial; end; diff --git a/examples/milestone/Fibonacci/Fibonacci.juvix b/examples/milestone/Fibonacci/Fibonacci.juvix index ad5e1dd25..5cc8025e5 100644 --- a/examples/milestone/Fibonacci/Fibonacci.juvix +++ b/examples/milestone/Fibonacci/Fibonacci.juvix @@ -2,14 +2,14 @@ module Fibonacci; open import Stdlib.Prelude; -fib : ℕ → ℕ → ℕ → ℕ; -fib zero x1 _ ≔ x1; -fib (suc n) x1 x2 ≔ fib n x2 (x1 + x2); +fib : Nat → Nat → Nat → Nat; +fib zero x1 _ := x1; +fib (suc n) x1 x2 := fib n x2 (x1 + x2); -fibonacci : ℕ → ℕ; -fibonacci n ≔ fib n 0 1; +fibonacci : Nat → Nat; +fibonacci n := fib n 0 1; main : IO; -main ≔ putStrLn (natToStr (fibonacci 25)); +main := putStrLn (natToStr (fibonacci 25)); end; diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix index e33737e2a..93de2ada3 100644 --- a/examples/milestone/Hanoi/Hanoi.juvix +++ b/examples/milestone/Hanoi/Hanoi.juvix @@ -25,22 +25,22 @@ compile ++str { --- --- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil; concat : List String → String; -concat ≔ foldl (++str) ""; +concat := foldl (++str) ""; intercalate : String → List String → String; -intercalate sep xs ≔ concat (intersperse sep xs); +intercalate sep xs := concat (intersperse sep xs); --- Joins a list of strings with the newline character unlines : List String → String; -unlines ≔ intercalate "\n"; +unlines := intercalate "\n"; --- Produce a singleton List singleton : {A : Type} → A → List A; -singleton a ≔ a ∷ nil; +singleton a := a ∷ nil; ---- Produce a ;String; representation of a ;List ℕ; -showList : List ℕ → String; -showList xs ≔ "[" ++str intercalate "," (map natToStr xs) ++str "]"; +--- Produce a ;String; representation of a ;List Nat; +showList : List Nat → String; +showList xs := "[" ++str intercalate "," (map natToStr xs) ++str "]"; --- A Peg represents a peg in the towers of Hanoi game inductive Peg { @@ -50,9 +50,9 @@ inductive Peg { }; showPeg : Peg → String; -showPeg left ≔ "left"; -showPeg middle ≔ "middle"; -showPeg right ≔ "right"; +showPeg left := "left"; +showPeg middle := "middle"; +showPeg right := "right"; --- A Move represents a move between pegs @@ -61,14 +61,14 @@ inductive Move { }; showMove : Move → String; -showMove (move from to) ≔ showPeg from ++str " -> " ++str showPeg to; +showMove (move from to) := showPeg from ++str " -> " ++str showPeg to; --- Produce a list of ;Move;s that solves the towers of Hanoi game -hanoi : ℕ → Peg → Peg → Peg → List Move; -hanoi zero _ _ _ ≔ nil; -hanoi (suc n) p1 p2 p3 ≔ hanoi n p1 p3 p2 ++ singleton (move p1 p2) ++ hanoi n p3 p2 p1; +hanoi : Nat → Peg → Peg → Peg → List Move; +hanoi zero _ _ _ := nil; +hanoi (suc n) p1 p2 p3 := hanoi n p1 p3 p2 ++ singleton (move p1 p2) ++ hanoi n p3 p2 p1; main : IO; -main ≔ putStrLn (unlines (map showMove (hanoi 5 left middle right))); +main := putStrLn (unlines (map showMove (hanoi 5 left middle right))); end; diff --git a/examples/milestone/HelloWorld/HelloWorld.juvix b/examples/milestone/HelloWorld/HelloWorld.juvix index c9728d274..fb72a17b9 100644 --- a/examples/milestone/HelloWorld/HelloWorld.juvix +++ b/examples/milestone/HelloWorld/HelloWorld.juvix @@ -4,6 +4,6 @@ module HelloWorld; open import Stdlib.Prelude; main : IO; -main ≔ putStrLn "hello world!"; +main := putStrLn "hello world!"; end; diff --git a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix index 1ccc0e84b..7d65af56b 100644 --- a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix +++ b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix @@ -10,18 +10,18 @@ module PascalsTriangle; open import Stdlib.Prelude; zipWith : {A : Type} → {B : Type} → {C : Type} → (A → B → C) -> List A → List B → List C; -zipWith f nil _ ≔ nil; -zipWith f _ nil ≔ nil; -zipWith f (x ∷ xs) (y ∷ ys) ≔ f x y ∷ zipWith f xs ys; +zipWith f nil _ := nil; +zipWith f _ nil := nil; +zipWith f (x ∷ xs) (y ∷ ys) := f x y ∷ zipWith f xs ys; --- Return a list of repeated applications of a given function -iterate : {A : Type} → ℕ → (A → A) → A → List A; -iterate zero _ _ ≔ nil; -iterate (suc n) f a ≔ a ∷ iterate n f (f a); +iterate : {A : Type} → Nat → (A → A) → A → List A; +iterate zero _ _ := nil; +iterate (suc n) f a := a ∷ iterate n f (f a); --- Produce a singleton List singleton : {A : Type} → A → List A; -singleton a ≔ a ∷ nil; +singleton a := a ∷ nil; --- Concatenation of ;String;s infixr 5 ++str; @@ -34,27 +34,27 @@ compile ++str { --- --- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil; concat : List String → String; -concat ≔ foldl (++str) ""; +concat := foldl (++str) ""; intercalate : String → List String → String; -intercalate sep xs ≔ concat (intersperse sep xs); +intercalate sep xs := concat (intersperse sep xs); --- Joins a list of strings with the newline character unlines : List String → String; -unlines ≔ intercalate "\n"; +unlines := intercalate "\n"; -showList : List ℕ → String; -showList xs ≔ "[" ++str intercalate "," (map natToStr xs) ++str "]"; +showList : List Nat → String; +showList xs := "[" ++str intercalate "," (map natToStr xs) ++str "]"; --- Compute the next row of Pascal's triangle -pascalNextRow : List ℕ → List ℕ; -pascalNextRow row ≔ zipWith (+) (singleton zero ++ row) (row ++ singleton zero); +pascalNextRow : List Nat → List Nat; +pascalNextRow row := zipWith (+) (singleton zero ++ row) (row ++ singleton zero); --- Produce Pascal's triangle to a given depth -pascal : ℕ → List (List ℕ); -pascal rows ≔ iterate rows pascalNextRow (singleton one); +pascal : Nat → List (List Nat); +pascal rows := iterate rows pascalNextRow (singleton one); main : IO; -main ≔ putStrLn (unlines (map showList (pascal 10))); +main := putStrLn (unlines (map showList (pascal 10))); end; diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix index 1d0ee8d2e..440c532cb 100644 --- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix +++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix @@ -16,35 +16,35 @@ compile readline { c ↦ "readline()"; }; -axiom parsePositiveInt : String → ℕ; +axiom parsePositiveInt : String → Nat; compile parsePositiveInt { c ↦ "parsePositiveInt"; }; --- | Reads a ;ℕ; from stdin -getMove : Maybe ℕ; -getMove ≔ validMove (parsePositiveInt (readline)); +-- | Reads a ;Nat; from stdin +getMove : Maybe Nat; +getMove := validMove (parsePositiveInt (readline)); do : IO × GameState -> GameState; -do (_, s) ≔ playMove getMove s; +do (_, s) := playMove getMove s; -- | A ;String; that prompts the user for their input prompt : GameState → String; -prompt x ≔ "\n" ++str (showGameState x) ++str "\nPlayer " ++str showSymbol (player x) ++str ": "; +prompt x := "\n" ++str (showGameState x) ++str "\nPlayer " ++str showSymbol (player x) ++str ": "; -- | Main loop terminating run : (IO × GameState → GameState) → GameState → IO; -run _ (state b p (terminate msg)) ≔ putStrLn ("\n" ++str (showGameState (state b p noError)) ++str "\n" ++str msg); -run f (state b p (continue msg)) ≔ run f (f (putStr (msg ++str prompt (state b p noError)), state b p noError)); -run f x ≔ run f (f (putStr (prompt x), x)); +run _ (state b p (terminate msg)) := putStrLn ("\n" ++str (showGameState (state b p noError)) ++str "\n" ++str msg); +run f (state b p (continue msg)) := run f (f (putStr (msg ++str prompt (state b p noError)), state b p noError)); +run f x := run f (f (putStr (prompt x), x)); --- The welcome message welcome : String; -welcome ≔ "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move"; +welcome := "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move"; --- The entry point of the program main : IO; -main ≔ putStrLn welcome >> run do beginState; +main := putStrLn welcome >> run do beginState; end; diff --git a/examples/milestone/TicTacToe/Logic/Board.juvix b/examples/milestone/TicTacToe/Logic/Board.juvix index 5723379ac..c5a297a75 100644 --- a/examples/milestone/TicTacToe/Logic/Board.juvix +++ b/examples/milestone/TicTacToe/Logic/Board.juvix @@ -11,29 +11,29 @@ inductive Board { }; --- Returns the list of numbers corresponding to the empty ;Square;s -possibleMoves : List Square → List ℕ; -possibleMoves nil ≔ nil; -possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs; -possibleMoves (_ ∷ xs) ≔ possibleMoves xs; +possibleMoves : List Square → List Nat; +possibleMoves nil := nil; +possibleMoves ((empty n) ∷ xs) := n ∷ possibleMoves xs; +possibleMoves (_ ∷ xs) := possibleMoves xs; --- ;true; if all the ;Square;s in the list are equal full : List Square → Bool; -full (a ∷ b ∷ c ∷ nil) ≔ (==Square a b) && (==Square b c); +full (a ∷ b ∷ c ∷ nil) := (==Square a b) && (==Square b c); diagonals : List (List Square) → List (List Square); -diagonals ((a1 ∷ _ ∷ b1 ∷ nil) ∷ (_ ∷ c ∷ _ ∷ nil) ∷ (b2 ∷ _ ∷ a2 ∷ nil) ∷ nil) ≔ (a1 ∷ c ∷ a2 ∷ nil) ∷ (b1 ∷ c ∷ b2 ∷ nil) ∷ nil; +diagonals ((a1 ∷ _ ∷ b1 ∷ nil) ∷ (_ ∷ c ∷ _ ∷ nil) ∷ (b2 ∷ _ ∷ a2 ∷ nil) ∷ nil) := (a1 ∷ c ∷ a2 ∷ nil) ∷ (b1 ∷ c ∷ b2 ∷ nil) ∷ nil; columns : List (List Square) → List (List Square); -columns ≔ transpose; +columns := transpose; rows : List (List Square) → List (List Square); -rows ≔ id; +rows := id; --- Textual representation of a ;List Square; showRow : List Square → String; -showRow xs ≔ concat (surround "|" (map showSquare xs)); +showRow xs := concat (surround "|" (map showSquare xs)); showBoard : Board → String; -showBoard (board squares) ≔ unlines (surround "+---+---+---+" (map showRow squares)); +showBoard (board squares) := unlines (surround "+---+---+---+" (map showRow squares)); end; diff --git a/examples/milestone/TicTacToe/Logic/Extra.juvix b/examples/milestone/TicTacToe/Logic/Extra.juvix index c9154c807..fb91faa74 100644 --- a/examples/milestone/TicTacToe/Logic/Extra.juvix +++ b/examples/milestone/TicTacToe/Logic/Extra.juvix @@ -15,18 +15,18 @@ compile ++str { --- --- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil; concat : List String → String; -concat ≔ foldl (++str) ""; +concat := 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; -surround x xs ≔ (x ∷ intersperse x xs) ++ (x ∷ nil); +surround x xs := (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; -intercalate sep xs ≔ concat (intersperse sep xs); +intercalate sep xs := concat (intersperse sep xs); --- Joins a list of strings with the newline character unlines : List String → String; -unlines ≔ intercalate "\n"; +unlines := intercalate "\n"; end; diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix index d7d76130a..45351b0b3 100644 --- a/examples/milestone/TicTacToe/Logic/Game.juvix +++ b/examples/milestone/TicTacToe/Logic/Game.juvix @@ -14,7 +14,7 @@ open import Logic.GameState public; --- Checks if we reached the end of the game. checkState : GameState → GameState; -checkState (state b p e) ≔ +checkState (state b p e) := if (won (state b p e)) (state b p (terminate ("Player " ++str (showSymbol (switch p)) ++str " wins!"))) (if (draw (state b p e)) @@ -22,18 +22,18 @@ checkState (state b p e) ≔ (state b p e)); --- Given a player attempted move, updates the state accordingly. -playMove : Maybe ℕ → GameState → GameState; -playMove nothing (state b p _) ≔ +playMove : Maybe Nat → GameState → GameState; +playMove nothing (state b p _) := state b p (continue "\nInvalid number, try again\n"); -playMove (just k) (state (board s) player e) ≔ +playMove (just k) (state (board s) player e) := if (not (elem (==) k (possibleMoves (flatten s)))) (state (board s) player (continue "\nThe square is already occupied, try again\n")) (checkState (state (board (map (map (replace player k)) s)) (switch player) noError)); ---- Returns ;just; if the given ;ℕ; is in range of 1..9 -validMove : ℕ → Maybe ℕ; -validMove n ≔ if ((n <= nine) && (n >= one)) (just n) nothing; +--- Returns ;just; if the given ;Nat; is in range of 1..9 +validMove : Nat → Maybe Nat; +validMove n := if ((n <= nine) && (n >= one)) (just n) nothing; end; diff --git a/examples/milestone/TicTacToe/Logic/GameState.juvix b/examples/milestone/TicTacToe/Logic/GameState.juvix index ea92ce167..d9b6cd997 100644 --- a/examples/milestone/TicTacToe/Logic/GameState.juvix +++ b/examples/milestone/TicTacToe/Logic/GameState.juvix @@ -19,25 +19,25 @@ inductive GameState { --- Textual representation of a ;GameState; showGameState : GameState → String; -showGameState (state b _ _) ≔ showBoard b; +showGameState (state b _ _) := showBoard b; --- Projects the player player : GameState → Symbol; -player (state _ p _) ≔ p; +player (state _ p _) := p; --- initial ;GameState; beginState : GameState; -beginState ≔ state +beginState := state (board (map (map empty) ((one ∷ two ∷ three ∷ nil) ∷ (four ∷ five ∷ six ∷ nil) ∷ (seven ∷ eight ∷ nine ∷ nil) ∷ nil))) X noError; --- ;true; if some player has won the game won : GameState → Bool; -won (state (board squares) _ _) ≔ any full (diagonals squares ++ rows squares ++ columns squares); +won (state (board squares) _ _) := any full (diagonals squares ++ rows squares ++ columns squares); --- ;true; if there is a draw draw : GameState → Bool; -draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares)); +draw (state (board squares) _ _) := null (possibleMoves (flatten squares)); end; diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix index e1770aa78..f1953dd98 100644 --- a/examples/milestone/TicTacToe/Logic/Square.juvix +++ b/examples/milestone/TicTacToe/Logic/Square.juvix @@ -7,26 +7,26 @@ open import Logic.Extra; --- A square is each of the holes in a board inductive Square { - --- An empty square has a ;ℕ; that uniquely identifies it - empty : ℕ → Square; + --- An empty square has a ;Nat; that uniquely identifies it + empty : Nat → Square; --- An occupied square has a ;Symbol; in it occupied : Symbol → Square; }; --- Equality for ;Square;s ==Square : Square → Square → Bool; -==Square (empty m) (empty n) ≔ m == n; -==Square (occupied s) (occupied t) ≔ ==Symbol s t; -==Square _ _ ≔ false; +==Square (empty m) (empty n) := m == n; +==Square (occupied s) (occupied t) := ==Symbol s t; +==Square _ _ := false; --- Textual representation of a ;Square; showSquare : Square → String; -showSquare (empty n) ≔ " " ++str natToStr n ++str " "; -showSquare (occupied s) ≔ " " ++str showSymbol s ++str " "; +showSquare (empty n) := " " ++str natToStr n ++str " "; +showSquare (occupied s) := " " ++str showSymbol s ++str " "; -replace : Symbol → ℕ → Square → Square; -replace player k (empty n) ≔ if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n); -replace _ _ s ≔ s; +replace : Symbol → Nat → Square → Square; +replace player k (empty n) := if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n); +replace _ _ s := s; end; diff --git a/examples/milestone/TicTacToe/Logic/Symbol.juvix b/examples/milestone/TicTacToe/Logic/Symbol.juvix index edc1eca57..eb6ab5cda 100644 --- a/examples/milestone/TicTacToe/Logic/Symbol.juvix +++ b/examples/milestone/TicTacToe/Logic/Symbol.juvix @@ -13,18 +13,18 @@ inductive Symbol { --- Equality for ;Symbol;s ==Symbol : Symbol → Symbol → Bool; -==Symbol O O ≔ true; -==Symbol X X ≔ true; -==Symbol _ _ ≔ false; +==Symbol O O := true; +==Symbol X X := true; +==Symbol _ _ := false; --- Turns ;O; into ;X; and ;X; into ;O; switch : Symbol → Symbol; -switch O ≔ X; -switch X ≔ O; +switch O := X; +switch X := O; --- Textual representation of a ;Symbol; showSymbol : Symbol → String; -showSymbol O ≔ "O"; -showSymbol X ≔ "X"; +showSymbol O := "O"; +showSymbol X := "X"; end; diff --git a/examples/milestone/TicTacToe/Web/TicTacToe.juvix b/examples/milestone/TicTacToe/Web/TicTacToe.juvix index 75a87c240..80efc21be 100644 --- a/examples/milestone/TicTacToe/Web/TicTacToe.juvix +++ b/examples/milestone/TicTacToe/Web/TicTacToe.juvix @@ -16,10 +16,10 @@ open import Logic.Game; axiom hostLog : String → IO; -- XCoord → YCoord → Width → Height → Color → IO -axiom hostFillRect : ℕ → ℕ → ℕ → ℕ → String → IO; +axiom hostFillRect : Nat → Nat → Nat → Nat → String → IO; -- XCoord → YCoord → Text → Size → Color → Align → IO -axiom hostFillText : ℕ → ℕ → String → ℕ → String → ℕ → IO; +axiom hostFillText : Nat → Nat → String → Nat → String → Nat → IO; -- Nat extension @@ -30,7 +30,7 @@ foreign c { }; infixl 7 div; -axiom div : ℕ → ℕ → ℕ; +axiom div : Nat → Nat → Nat; compile div { c ↦ "div"; @@ -44,52 +44,52 @@ compile IOUnit { }; sequenceIO : List IO → IO; -sequenceIO ≔ foldr (>>) IOUnit; +sequenceIO := foldr (>>) IOUnit; mapIO : {A : Type} → (A → IO) → List A → IO; -mapIO f xs ≔ sequenceIO (map f xs); +mapIO f xs := sequenceIO (map f xs); -- List extensions zip : {A : Type} → {B : Type} → List A → List B → List (A × B); -zip (a ∷ as) (b ∷ bs) ≔ (a, b) ∷ zip as bs; -zip _ _ ≔ nil; +zip (a ∷ as) (b ∷ bs) := (a, b) ∷ zip as bs; +zip _ _ := nil; -rangeAux : ℕ → ℕ → List ℕ; -rangeAux _ zero ≔ nil; -rangeAux m (suc n) ≔ m ∷ rangeAux (suc m) n; +rangeAux : Nat → Nat → List Nat; +rangeAux _ zero := nil; +rangeAux m (suc n) := m ∷ rangeAux (suc m) n; -range : ℕ → List ℕ; -range n ≔ rangeAux zero n; +range : Nat → List Nat; +range n := rangeAux zero n; -enumerate : {A : Type} → List A → List (ℕ × A); -enumerate l ≔ zip (range (length l)) l; +enumerate : {A : Type} → List A → List (Nat × A); +enumerate l := zip (range (length l)) l; -- Formatting constants -squareWidth : ℕ; -squareWidth ≔ 100; +squareWidth : Nat; +squareWidth := 100; -textSize : ℕ; -textSize ≔ 30; +textSize : Nat; +textSize := 30; -xTextOffset : ℕ; -xTextOffset ≔ 50; +xTextOffset : Nat; +xTextOffset := 50; -yTextOffset : ℕ; -yTextOffset ≔ 60; +yTextOffset : Nat; +yTextOffset := 60; -canvasPadding : ℕ; -canvasPadding ≔ 8; +canvasPadding : Nat; +canvasPadding := 8; textColor : String; -textColor ≔ "#000000"; +textColor := "#000000"; backgroundColor : String; -backgroundColor ≔ "#c4434e"; +backgroundColor := "#c4434e"; lightBackgroundColor : String; -lightBackgroundColor ≔ "#c7737a"; +lightBackgroundColor := "#c7737a"; -- Rendering @@ -99,66 +99,66 @@ inductive Align { center : Align; }; -alignNum : Align → ℕ; -alignNum left ≔ zero; -alignNum right ≔ one; -alignNum center ≔ two; +alignNum : Align → Nat; +alignNum left := zero; +alignNum right := one; +alignNum center := two; -renderText : String → ℕ → ℕ → Align → IO; -renderText t row col a ≔ hostFillText ((squareWidth * row) + xTextOffset) ((squareWidth * col) + yTextOffset) t textSize textColor (alignNum a); +renderText : String → Nat → Nat → Align → IO; +renderText t row col a := hostFillText ((squareWidth * row) + xTextOffset) ((squareWidth * col) + yTextOffset) t textSize textColor (alignNum a); -renderSymbol : Symbol → ℕ → ℕ → IO; -renderSymbol s row col ≔ renderText (showSymbol s) row col center; +renderSymbol : Symbol → Nat → Nat → IO; +renderSymbol s row col := renderText (showSymbol s) row col center; -renderNumber : ℕ → ℕ → ℕ → IO; -renderNumber n row col ≔ renderText (natToStr n) row col center; +renderNumber : Nat → Nat → Nat → IO; +renderNumber n row col := renderText (natToStr n) row col center; -renderSquare : ℕ → ℕ → Square → IO; -renderSquare row col (occupied s) ≔ +renderSquare : Nat → Nat → Square → IO; +renderSquare row col (occupied s) := hostFillRect (squareWidth * row) (squareWidth * col) squareWidth squareWidth backgroundColor >> renderSymbol s row col; -renderSquare row col (empty n) ≔ +renderSquare row col (empty n) := hostFillRect (squareWidth * row) (squareWidth * col) squareWidth squareWidth lightBackgroundColor >> renderNumber n row col; -renderRowAux : ℕ → (ℕ × Square) → IO; -renderRowAux col (row, s) ≔ renderSquare row col s; +renderRowAux : Nat → (Nat × Square) → IO; +renderRowAux col (row, s) := renderSquare row col s; -renderRow : ℕ × (List Square) → IO; -renderRow (n, xs) ≔ mapIO (renderRowAux n) (enumerate xs); +renderRow : Nat × (List Square) → IO; +renderRow (n, xs) := mapIO (renderRowAux n) (enumerate xs); renderBoard : Board → IO; -renderBoard (board squares) ≔ mapIO renderRow (enumerate squares); +renderBoard (board squares) := mapIO renderRow (enumerate squares); renderFooterText : String → IO; -renderFooterText msg ≔ renderText msg 0 3 left; +renderFooterText msg := renderText msg 0 3 left; nextPlayerText : Symbol → String; -nextPlayerText s ≔ "Next player: " ++str (showSymbol s); +nextPlayerText s := "Next player: " ++str (showSymbol s); renderError : Error → IO; -renderError noError ≔ IOUnit; -renderError (continue msg) ≔ renderText msg 0 3 left; -renderError (terminate msg) ≔ renderText msg 0 3 left; +renderError noError := IOUnit; +renderError (continue msg) := renderText msg 0 3 left; +renderError (terminate msg) := renderText msg 0 3 left; renderGameState : GameState → IO; -renderGameState (state b _ (terminate msg)) ≔ renderBoard b >> renderFooterText msg; -renderGameState (state b p (continue msg)) ≔ renderBoard b >> renderFooterText (nextPlayerText p) >> renderText (msg) 0 4 left; -renderGameState (state b p _) ≔ renderBoard b >> renderFooterText (nextPlayerText p); +renderGameState (state b _ (terminate msg)) := renderBoard b >> renderFooterText msg; +renderGameState (state b p (continue msg)) := renderBoard b >> renderFooterText (nextPlayerText p) >> renderText (msg) 0 4 left; +renderGameState (state b p _) := renderBoard b >> renderFooterText (nextPlayerText p); renderAndReturn : GameState → GameState; -renderAndReturn s ≔ const s (renderGameState s); +renderAndReturn s := const s (renderGameState s); -selectedSquare : ℕ → ℕ → ℕ; -selectedSquare row col ≔ 3 * (col div squareWidth) + (row div squareWidth) + 1; +selectedSquare : Nat → Nat → Nat; +selectedSquare row col := 3 * (col div squareWidth) + (row div squareWidth) + 1; -- API initGame : GameState; -initGame ≔ const beginState (renderGameState beginState >> renderText "Click on a square to make a move" 0 4 left); +initGame := const beginState (renderGameState beginState >> renderText "Click on a square to make a move" 0 4 left); -move : GameState → ℕ → ℕ → GameState; -move (state b p (terminate e)) x y ≔ renderAndReturn (state b p (terminate e)); -move s x y ≔ renderAndReturn (playMove (validMove (selectedSquare x y)) s); +move : GameState → Nat → Nat → GameState; +move (state b p (terminate e)) x y := renderAndReturn (state b p (terminate e)); +move s x y := renderAndReturn (playMove (validMove (selectedSquare x y)) s); end; diff --git a/examples/milestone/ValidityPredicates/Anoma/Base.juvix b/examples/milestone/ValidityPredicates/Anoma/Base.juvix index 5b745533d..e7167873a 100644 --- a/examples/milestone/ValidityPredicates/Anoma/Base.juvix +++ b/examples/milestone/ValidityPredicates/Anoma/Base.juvix @@ -36,10 +36,10 @@ open import Data.Int.Ops; import Stdlib.Data.String.Ord; from-int : Int → Maybe Int; -from-int i ≔ if (i < Int_0) nothing (just i); +from-int i := if (i < Int_0) nothing (just i); from-string : String → Maybe String; -from-string s ≔ if (s Stdlib.Data.String.Ord.== "") nothing (just s); +from-string s := if (s Stdlib.Data.String.Ord.== "") nothing (just s); -------------------------------------------------------------------------------- -- Anoma @@ -64,15 +64,15 @@ compile isBalanceKey { }; read-pre : String → Maybe Int; -read-pre s ≔ from-int (readPre s); +read-pre s := from-int (readPre s); read-post : String → Maybe Int; -read-post s ≔ from-int (readPost s); +read-post s := from-int (readPost s); is-balance-key : String → String → Maybe String; -is-balance-key token key ≔ from-string (isBalanceKey token key); +is-balance-key token key := from-string (isBalanceKey token key); unwrap-default : Maybe Int → Int; -unwrap-default ≔ maybe Int_0 id; +unwrap-default := maybe Int_0 id; end; diff --git a/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix b/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix index 8543299ac..a15ff2b8b 100644 --- a/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix +++ b/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix @@ -29,7 +29,7 @@ compile <' { infix 4 <; < : Int → Int → Bool; -< i1 i2 ≔ from-backend-bool (i1 <' i2); +< i1 i2 := from-backend-bool (i1 <' i2); axiom eqInt : Int → Int → BackendBool; compile eqInt { @@ -38,7 +38,7 @@ compile eqInt { infix 4 ==; == : Int → Int → Bool; -== i1 i2 ≔ from-backend-bool (eqInt i1 i2); +== i1 i2 := from-backend-bool (eqInt i1 i2); infixl 6 -; axiom - : Int -> Int -> Int; diff --git a/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix b/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix index ce0795471..809699f0e 100644 --- a/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix +++ b/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix @@ -9,15 +9,15 @@ import Data.Int.Ops; -- Misc pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString ≔ maybe (Int_0, false); +pair-from-optionString := maybe (Int_0, false); -- Validity Predicate change-from-key : String → Int; -change-from-key key ≔ unwrap-default (read-post key) Data.Int.Ops.- unwrap-default (read-pre key); +change-from-key key := unwrap-default (read-post key) Data.Int.Ops.- unwrap-default (read-pre key); check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner ≔ +check-vp verifiers key change owner := if (change-from-key key Data.Int.Ops.< Int_0) -- make sure the spender approved the transaction @@ -25,17 +25,17 @@ check-vp verifiers key change owner ≔ (change Data.Int.Ops.+ (change-from-key key), true); check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change, is-success) key ≔ +check-keys token verifiers (change, is-success) key := if is-success (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) (Int_0, false); check-result : Int × Bool → Bool; -check-result (change, all-checked) ≔ (change Data.Int.Ops.== Int_0) && all-checked; +check-result (change, all-checked) := (change Data.Int.Ops.== Int_0) && all-checked; vp : String → List String → List String → Bool; -vp token keys-changed verifiers ≔ +vp token keys-changed verifiers := check-result (foldl (check-keys token verifiers) diff --git a/examples/milestone/ValidityPredicates/Tests.juvix b/examples/milestone/ValidityPredicates/Tests.juvix index 19aa0795c..8a8008b42 100644 --- a/examples/milestone/ValidityPredicates/Tests.juvix +++ b/examples/milestone/ValidityPredicates/Tests.juvix @@ -8,29 +8,29 @@ open import SimpleFungibleToken; -------------------------------------------------------------------------------- token : String; -token ≔ "owner-token"; +token := "owner-token"; owner-address : String; -owner-address ≔ "owner-address"; +owner-address := "owner-address"; change1-key : String; -change1-key ≔ "change1-key"; +change1-key := "change1-key"; change2-key : String; -change2-key ≔ "change2-key"; +change2-key := "change2-key"; verifiers : List String; -verifiers ≔ owner-address ∷ nil; +verifiers := owner-address ∷ nil; keys-changed : List String; -keys-changed ≔ change1-key ∷ change2-key ∷ nil; +keys-changed := change1-key ∷ change2-key ∷ nil; show-result : Bool → String; -show-result true ≔ "OK"; -show-result false ≔ "FAIL"; +show-result true := "OK"; +show-result false := "FAIL"; main : IO; -main ≔ +main := (putStr "VP Status: ") >> (putStrLn (show-result (vp token keys-changed verifiers))); diff --git a/juvix-stdlib b/juvix-stdlib index 5228caaf1..2c7658902 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 5228caaf13c55db942a60dba50bce8cbc74d0497 +Subproject commit 2c765890271b536f1c6247a4f00ce6f5e688aed0 diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index fd07ad03d..aad96ce28 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -271,8 +271,7 @@ operatorSyntaxDef = do where arity :: ParsecS r OperatorArity arity = - do - Binary AssocRight <$ kwInfixr + Binary AssocRight <$ kwInfixr <|> Binary AssocLeft <$ kwInfixl <|> Binary AssocNone <$ kwInfix <|> Unary AssocPostfix <$ kwPostfix diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs index e63ceda11..e3a9bd384 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs @@ -150,7 +150,7 @@ kwBuiltin :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwBuiltin = keyword Str.builtin kwAssign :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () -kwAssign = keywordUnicode Str.assignAscii Str.assignUnicode +kwAssign = keyword Str.assignAscii kwAxiom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwAxiom = keyword Str.axiom diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs index e1850d5ab..b53c9dff0 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs @@ -110,7 +110,7 @@ braces :: ParsecS r a -> ParsecS r a braces = between (symbol "{") (symbol "}") kwAssign :: ParsecS r () -kwAssign = keyword Str.assignUnicode <|> keyword Str.assignAscii +kwAssign = keyword Str.assignAscii kwLet :: ParsecS r () kwLet = keyword Str.let_ diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs index a86d4fd08..1216bdea0 100644 --- a/src/Juvix/Data/CodeAnn.hs +++ b/src/Juvix/Data/CodeAnn.hs @@ -76,7 +76,7 @@ kwData :: Doc Ann kwData = keyword Str.data_ kwAssign :: Doc Ann -kwAssign = keyword Str.assignUnicode +kwAssign = keyword Str.assignAscii kwEquals :: Doc Ann kwEquals = keyword Str.equal @@ -142,7 +142,7 @@ kwInfix :: Doc Ann kwInfix = keyword Str.infix_ kwAssignment :: Doc Ann -kwAssignment = keyword Str.assignUnicode +kwAssignment = keyword Str.assignAscii kwColonZero :: Doc Ann kwColonZero = keyword Str.colonZero diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index b759f8230..0bbe6486c 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -122,9 +122,6 @@ using = "using" where_ :: IsString s => s where_ = "where" -assignUnicode :: IsString s => s -assignUnicode = "≔" - assignAscii :: IsString s => s assignAscii = ":=" diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index c7f5380b3..987237ca5 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -65,19 +65,18 @@ string' :: ParsecS r Text string' = pack <$> (char '"' >> manyTill L.charLiteral (char '"')) keyword' :: ParsecS r () -> Text -> ParsecS r () -keyword' spc kw = do +keyword' spc kw = P.try $ do P.chunk kw notFollowedBy (satisfy validTailChar) spc keywordL' :: Member (Reader ParserParams) r => ParsecS r () -> Text -> ParsecS r Interval -keywordL' spc kw = do - P.try $ do - i <- snd <$> interval (P.chunk kw) - notFollowedBy (satisfy validTailChar) - spc - return i +keywordL' spc kw = P.try $ do + i <- onlyInterval (P.chunk kw) + notFollowedBy (satisfy validTailChar) + spc + return i keywordSymbol' :: ParsecS r () -> Text -> ParsecS r () keywordSymbol' spc kw = do @@ -103,7 +102,7 @@ delimiterSymbols :: [Char] delimiterSymbols = "," reservedSymbols :: [Char] -reservedSymbols = "@\";(){}[].≔λ\\" +reservedSymbols = "@\";(){}[].λ\\" validFirstChar :: Char -> Bool validFirstChar c = not (isNumber c || isSpace c || (c `elem` reservedSymbols)) @@ -115,6 +114,9 @@ curLoc = do root <- lift (asks (^. parserParamsRoot)) return (mkLoc root offset sp) +onlyInterval :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r Interval +onlyInterval = fmap snd . interval + interval :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (a, Interval) interval ma = do start <- curLoc diff --git a/tests/CLI/Commands/dev/internal.test b/tests/CLI/Commands/dev/internal.test index fd5c929f7..c4374fae8 100644 --- a/tests/CLI/Commands/dev/internal.test +++ b/tests/CLI/Commands/dev/internal.test @@ -16,6 +16,6 @@ $ juvix --only-errors dev internal typecheck tests/positive/Internal/Simple.juvi >= 0 $ juvix --no-colors dev internal typecheck tests/negative/Internal/MultiWrongType.juvix ->2 /(.+)\/([^\/]+)\.juvix\:14\:7\-8\: error.* +>2 /(.+)\/([^\/]+)\.juvix\:[0-9]*\:[0-9]*\-[0-9]*\: error.* .*/ >= 1 diff --git a/tests/CLI/Commands/typecheck.test b/tests/CLI/Commands/typecheck.test index f77914af2..81c8ae5f9 100644 --- a/tests/CLI/Commands/typecheck.test +++ b/tests/CLI/Commands/typecheck.test @@ -20,6 +20,6 @@ $ juvix --only-errors typecheck tests/positive/Internal/Simple.juvix >= 0 $ juvix --no-colors typecheck tests/negative/Internal/MultiWrongType.juvix ->2 /(.+)\/([^\/]+)\.juvix\:14\:7\-8\: error.* +>2 /(.+)\/([^\/]+)\.juvix\:[0-9]*\:[0-9]*\-[0-9]*\: error.* .*/ >= 1 diff --git a/tests/Core/positive/lambda-lifting/test1.out b/tests/Core/positive/lambda-lifting/test1.out index a9851d55a..12b80c3cc 100644 --- a/tests/Core/positive/lambda-lifting/test1.out +++ b/tests/Core/positive/lambda-lifting/test1.out @@ -1,3 +1,3 @@ -- IdentContext -def 1 ≔ λg λx λy λz g$3 x$2 -def t1 ≔ λg λf f$0 (!1 g$1) +def 1 := λg λx λy λz g$3 x$2 +def t1 := λg λf f$0 (!1 g$1) diff --git a/tests/Core/positive/lambda-lifting/test2.out b/tests/Core/positive/lambda-lifting/test2.out index 1114fee20..11bd69ce5 100644 --- a/tests/Core/positive/lambda-lifting/test2.out +++ b/tests/Core/positive/lambda-lifting/test2.out @@ -1,6 +1,6 @@ -- IdentContext -def 1 ≔ λx λw w$0 x$1 -def 2 ≔ λy λx λe y$2 e$0 x$1 y$2 -def 3 ≔ λy λx λz z$0 y$2 x$1 (!1 x$1) (!2 x$1 y$2) -def 4 ≔ λs λx λy s$2 y$0 (!3 x$1 y$0) -def t2 ≔ λr λs r$1 (!4 s$0) +def 1 := λx λw w$0 x$1 +def 2 := λy λx λe y$2 e$0 x$1 y$2 +def 3 := λy λx λz z$0 y$2 x$1 (!1 x$1) (!2 x$1 y$2) +def 4 := λs λx λy s$2 y$0 (!3 x$1 y$0) +def t2 := λr λs r$1 (!4 s$0) diff --git a/tests/Core/positive/lambda-lifting/test3.out b/tests/Core/positive/lambda-lifting/test3.out index 6514b1d04..2cd9e3f7c 100644 --- a/tests/Core/positive/lambda-lifting/test3.out +++ b/tests/Core/positive/lambda-lifting/test3.out @@ -1,6 +1,6 @@ -- IdentContext -def 3 ≔ λx x$0 -def 4 ≔ λr λx r$1 -def const ≔ λx λy x$1 -def id ≔ λx x$0 -def t3 ≔ λr λs const !3 (id (!4 r$1)) +def 3 := λx x$0 +def 4 := λr λx r$1 +def const := λx λy x$1 +def id := λx x$0 +def t3 := λr λs const !3 (id (!4 r$1)) diff --git a/tests/negative/230/Foo/Data/Bool.juvix b/tests/negative/230/Foo/Data/Bool.juvix index 98263b3e1..730dac79a 100644 --- a/tests/negative/230/Foo/Data/Bool.juvix +++ b/tests/negative/230/Foo/Data/Bool.juvix @@ -8,21 +8,21 @@ import Stdlib.Data.Bool; }; not : Bool → Bool; - not true ≔ false; - not false ≔ true; + not true := false; + not false := true; infixr 2 ||; || : Bool → Bool → Bool; - || false a ≔ a; - || true _ ≔ true; + || false a := a; + || true _ := true; infixr 2 &&; && : Bool → Bool → Bool; - && false _ ≔ false; - && true a ≔ a; + && false _ := false; + && true a := a; if : {A : Type} → Bool → A → A → A; - if true a _ ≔ a; - if false _ b ≔ b; + if true a _ := a; + if false _ b := b; end; diff --git a/tests/negative/230/Prod.juvix b/tests/negative/230/Prod.juvix index d6b9a109a..b21b2181b 100644 --- a/tests/negative/230/Prod.juvix +++ b/tests/negative/230/Prod.juvix @@ -5,6 +5,6 @@ open import Foo; import Foo.Data.Bool; fi : Foo.Data.Bool; -fi ≔ Foo.Data.Bool.false; +fi := Foo.Data.Bool.false; end; diff --git a/tests/negative/265/M.juvix b/tests/negative/265/M.juvix index dbd2ec223..6a7f2c10a 100644 --- a/tests/negative/265/M.juvix +++ b/tests/negative/265/M.juvix @@ -10,7 +10,7 @@ inductive Pair (A : Type) (B : Type) { }; f : _ → _; -f (mkPair false true) ≔ true; -f true ≔ false; +f (mkPair false true) := true; +f true := false; end; diff --git a/tests/negative/AmbiguousConstructor.juvix b/tests/negative/AmbiguousConstructor.juvix index a1f55b569..46ef6a91f 100644 --- a/tests/negative/AmbiguousConstructor.juvix +++ b/tests/negative/AmbiguousConstructor.juvix @@ -15,5 +15,5 @@ module AmbiguousConstructor; open N; f : T1 -> T2; - f A ≔ N.A; + f A := N.A; end; diff --git a/tests/negative/AppLeftImplicit.juvix b/tests/negative/AppLeftImplicit.juvix index 046ccae3d..29ad7b5c9 100644 --- a/tests/negative/AppLeftImplicit.juvix +++ b/tests/negative/AppLeftImplicit.juvix @@ -1,6 +1,6 @@ module AppLeftImplicit; x : Type; - x ≔ {x}; + x := {x}; end; diff --git a/tests/negative/BindGroupConflict/Clause.juvix b/tests/negative/BindGroupConflict/Clause.juvix index edafc0f31..5660d1053 100644 --- a/tests/negative/BindGroupConflict/Clause.juvix +++ b/tests/negative/BindGroupConflict/Clause.juvix @@ -5,6 +5,6 @@ module Clause; }; fst : (a : Type) → (b : Type) → Pair a b → a ; - fst _ _ (mkPair _ _ x x) ≔ x; + fst _ _ (mkPair _ _ x x) := x; end; diff --git a/tests/negative/BindGroupConflict/Lambda.juvix b/tests/negative/BindGroupConflict/Lambda.juvix index 7aec355f1..ea502e725 100644 --- a/tests/negative/BindGroupConflict/Lambda.juvix +++ b/tests/negative/BindGroupConflict/Lambda.juvix @@ -5,6 +5,6 @@ module Lambda; }; fst : (a : Type) → (b : Type) → Pair a b → a ; - fst ≔ λ { _ _ (mkPair _ _ x x) := x }; + fst := λ { _ _ (mkPair _ _ x x) := x }; end; diff --git a/tests/negative/InfixErrorP.juvix b/tests/negative/InfixErrorP.juvix index e52087cc7..b6f428c90 100644 --- a/tests/negative/InfixErrorP.juvix +++ b/tests/negative/InfixErrorP.juvix @@ -7,6 +7,6 @@ module InfixErrorP; }; fst : Pair → Type; - fst (x , ) ≔ x; + fst (x , ) := x; end; diff --git a/tests/negative/Internal/ExpectedExplicitArgument.juvix b/tests/negative/Internal/ExpectedExplicitArgument.juvix index 43e6f4220..355d1fc92 100644 --- a/tests/negative/Internal/ExpectedExplicitArgument.juvix +++ b/tests/negative/Internal/ExpectedExplicitArgument.juvix @@ -4,5 +4,5 @@ module ExpectedExplicitArgument; }; f : {A : Type} → A → T A; - f {A} a ≔ c {A} {a}; + f {A} a := c {A} {a}; end; diff --git a/tests/negative/Internal/ExpectedExplicitPattern.juvix b/tests/negative/Internal/ExpectedExplicitPattern.juvix index 7f604351a..a0ef395fa 100644 --- a/tests/negative/Internal/ExpectedExplicitPattern.juvix +++ b/tests/negative/Internal/ExpectedExplicitPattern.juvix @@ -4,5 +4,5 @@ module ExpectedExplicitPattern; }; f : {A : Type} → T A → A; - f {_} {c a} ≔ a; + f {_} {c a} := a; end; diff --git a/tests/negative/Internal/ExpectedFunctionType.juvix b/tests/negative/Internal/ExpectedFunctionType.juvix index c9a49e321..749da537e 100644 --- a/tests/negative/Internal/ExpectedFunctionType.juvix +++ b/tests/negative/Internal/ExpectedFunctionType.juvix @@ -8,5 +8,5 @@ module ExpectedFunctionType; }; f : Pair B → Pair B; - f (mkPair a b) ≔ a b; + f (mkPair a b) := a b; end; diff --git a/tests/negative/Internal/FunctionApplied.juvix b/tests/negative/Internal/FunctionApplied.juvix index bd84a5f83..1f37c1e67 100644 --- a/tests/negative/Internal/FunctionApplied.juvix +++ b/tests/negative/Internal/FunctionApplied.juvix @@ -4,5 +4,5 @@ module FunctionApplied; }; f : {A : Type} → A → T A; - f {A} a ≔ c {(A → A) A} a; + f {A} a := c {(A → A) A} a; end; diff --git a/tests/negative/Internal/FunctionPattern.juvix b/tests/negative/Internal/FunctionPattern.juvix index 913dea1db..bc36be117 100644 --- a/tests/negative/Internal/FunctionPattern.juvix +++ b/tests/negative/Internal/FunctionPattern.juvix @@ -4,5 +4,5 @@ module FunctionPattern; }; f : (T → T) → T; - f A ≔ A; + f A := A; end; diff --git a/tests/negative/Internal/LhsTooManyPatterns.juvix b/tests/negative/Internal/LhsTooManyPatterns.juvix index eecb85fb0..5fcd4be9b 100644 --- a/tests/negative/Internal/LhsTooManyPatterns.juvix +++ b/tests/negative/Internal/LhsTooManyPatterns.juvix @@ -4,5 +4,5 @@ module LhsTooManyPatterns; }; f : T → T; - f A x ≔ A; + f A x := A; end; diff --git a/tests/negative/Internal/MultiWrongType.juvix b/tests/negative/Internal/MultiWrongType.juvix index a49798ecf..c15f0a1f0 100644 --- a/tests/negative/Internal/MultiWrongType.juvix +++ b/tests/negative/Internal/MultiWrongType.juvix @@ -8,8 +8,8 @@ module MultiWrongType; }; f : A; - f ≔ b; + f := b; g : B; - g ≔ a; + g := a; end; diff --git a/tests/negative/Internal/PatternConstructor.juvix b/tests/negative/Internal/PatternConstructor.juvix index f06d756b9..4b5bd2a8d 100644 --- a/tests/negative/Internal/PatternConstructor.juvix +++ b/tests/negative/Internal/PatternConstructor.juvix @@ -8,6 +8,6 @@ inductive B { }; f : A → B; - f b ≔ b; + f b := b; end; diff --git a/tests/negative/Internal/TooManyArguments.juvix b/tests/negative/Internal/TooManyArguments.juvix index 8ac5aab4b..c39ae0a40 100644 --- a/tests/negative/Internal/TooManyArguments.juvix +++ b/tests/negative/Internal/TooManyArguments.juvix @@ -4,5 +4,5 @@ module TooManyArguments; }; f : {A : Type} → A → T A; - f {A} a ≔ c {A} a a {a} ; + f {A} a := c {A} a a {a} ; end; diff --git a/tests/negative/Internal/UnsolvedMeta.juvix b/tests/negative/Internal/UnsolvedMeta.juvix index 5dba2237d..e4eadddba 100644 --- a/tests/negative/Internal/UnsolvedMeta.juvix +++ b/tests/negative/Internal/UnsolvedMeta.juvix @@ -5,6 +5,6 @@ inductive Proxy (A : Type) { }; t : Proxy _; -t ≔ x; +t := x; end; diff --git a/tests/negative/Internal/WrongConstructorArity.juvix b/tests/negative/Internal/WrongConstructorArity.juvix index 52009e959..79867e5df 100644 --- a/tests/negative/Internal/WrongConstructorArity.juvix +++ b/tests/negative/Internal/WrongConstructorArity.juvix @@ -4,5 +4,5 @@ module WrongConstructorArity; }; f : T → T; - f (A i x) ≔ i; + f (A i x) := i; end; diff --git a/tests/negative/Internal/WrongType.juvix b/tests/negative/Internal/WrongType.juvix index d3e6111a7..5bf78b712 100644 --- a/tests/negative/Internal/WrongType.juvix +++ b/tests/negative/Internal/WrongType.juvix @@ -8,5 +8,5 @@ module WrongType; }; f : A; - f ≔ b; + f := b; end; diff --git a/tests/negative/LacksTypeSig.juvix b/tests/negative/LacksTypeSig.juvix index ae3ff4d1c..8f78b2bea 100644 --- a/tests/negative/LacksTypeSig.juvix +++ b/tests/negative/LacksTypeSig.juvix @@ -1,6 +1,6 @@ module LacksTypeSig; - some ≔ Type; + some := Type; end; diff --git a/tests/negative/NestedPatternBraces.juvix b/tests/negative/NestedPatternBraces.juvix index 4b21a8aa5..eed23ef4f 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}} := a; end; diff --git a/tests/negative/Termination/Data/Bool.juvix b/tests/negative/Termination/Data/Bool.juvix index f1d697dd2..909165703 100644 --- a/tests/negative/Termination/Data/Bool.juvix +++ b/tests/negative/Termination/Data/Bool.juvix @@ -5,21 +5,21 @@ module Data.Bool; }; not : Bool → Bool; - not true ≔ false; - not false ≔ true; + not true := false; + not false := true; infixr 2 ||; || : Bool → Bool → Bool; - || false a ≔ a; - || true _ ≔ true; + || false a := a; + || true _ := true; infixr 2 &&; && : Bool → Bool → Bool; - && false _ ≔ false; - && true a ≔ a; + && false _ := false; + && true a := a; ite : (a : Type) → Bool → a → a → a; - ite _ true a _ ≔ a; - ite _ false _ b ≔ b; + ite _ true a _ := a; + ite _ false _ b := b; end; diff --git a/tests/negative/Termination/Data/Nat.juvix b/tests/negative/Termination/Data/Nat.juvix index ddf832bbf..991df50bd 100644 --- a/tests/negative/Termination/Data/Nat.juvix +++ b/tests/negative/Termination/Data/Nat.juvix @@ -6,13 +6,13 @@ module Data.Nat; infixl 6 +; + : ℕ → ℕ → ℕ; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); infixl 7 *; * : ℕ → ℕ → ℕ; - * zero b ≔ zero; - * (suc a) b ≔ b + a * b; + * zero b := zero; + * (suc a) b := b + a * b; import Data.Bool; open Data.Bool; @@ -20,9 +20,9 @@ module Data.Nat; even : ℕ → Bool; odd : ℕ → Bool; - even zero ≔ true; - even (suc n) ≔ odd n; + even zero := true; + even (suc n) := odd n; - odd zero ≔ false; - odd (suc n) ≔ even n; + odd zero := false; + odd (suc n) := even n; end; diff --git a/tests/negative/Termination/Data/QuickSort.juvix b/tests/negative/Termination/Data/QuickSort.juvix index 02f1ee57b..672d66ba6 100644 --- a/tests/negative/Termination/Data/QuickSort.juvix +++ b/tests/negative/Termination/Data/QuickSort.juvix @@ -12,25 +12,25 @@ inductive List (A : Type) { }; filter : (A : Type) → (A → Bool) → List A → List A; -filter A f nil ≔ nil A; -filter A f (cons h hs) ≔ ite (List A) (f h) +filter A f nil := nil A; +filter A f (cons h hs) := ite (List A) (f h) (cons A h (filter A f hs)) (filter A f hs); concat : (A : Type) → List A → List A → List A; -concat A nil ys ≔ ys; -concat A (cons x xs) ys ≔ cons A x (concat A xs ys); +concat A nil ys := ys; +concat A (cons x xs) ys := cons A x (concat A xs ys); ltx : (A : Type) → (A → A → Bool) → A → A → Bool; -ltx A lessThan x y ≔ lessThan y x; +ltx A lessThan x y := lessThan y x; gex : (A : Type) → (A → A → Bool) → A → A → Bool; -gex A lessThan x y ≔ not (ltx A lessThan x y) ; +gex A lessThan x y := not (ltx A lessThan x y) ; quicksort : (A : Type) → (A → A → Bool) → List A → List A; -quicksort A _ nil ≔ nil A; -quicksort A _ (cons x nil) ≔ cons A x (nil A); -quicksort A lessThan (cons x ys) ≔ +quicksort A _ nil := nil A; +quicksort A _ (cons x nil) := cons A x (nil A); +quicksort A lessThan (cons x ys) := concat A (quicksort A lessThan (filter A (ltx A lessThan x) ys)) (concat A (cons A x (nil A)) diff --git a/tests/negative/issue1344/D.juvix b/tests/negative/issue1344/D.juvix index ba23c0e34..dc0110011 100644 --- a/tests/negative/issue1344/D.juvix +++ b/tests/negative/issue1344/D.juvix @@ -3,6 +3,6 @@ module D; import U; u : Other.Unit; - u ≔ U.t; + u := U.t; end; diff --git a/tests/negative/issue1344/M.juvix b/tests/negative/issue1344/M.juvix index f055108ed..f332bf534 100644 --- a/tests/negative/issue1344/M.juvix +++ b/tests/negative/issue1344/M.juvix @@ -6,6 +6,6 @@ module M; }; u : Other.Unit; - u ≔ t; + u := t; end; diff --git a/tests/positive/265/M.juvix b/tests/positive/265/M.juvix index 9c9dcd29e..3cd5312cb 100644 --- a/tests/positive/265/M.juvix +++ b/tests/positive/265/M.juvix @@ -10,7 +10,7 @@ inductive Pair (A : Type) (B : Type) { }; f : _ → _; -f (mkPair false true) ≔ true; -f _ ≔ false; +f (mkPair false true) := true; +f _ := false; end; diff --git a/tests/positive/272/M.juvix b/tests/positive/272/M.juvix index f0e584632..910b044a8 100644 --- a/tests/positive/272/M.juvix +++ b/tests/positive/272/M.juvix @@ -15,14 +15,14 @@ inductive Nat { }; f : _; -f false false ≔ true; -f true _ ≔ false; +f false false := true; +f true _ := false; inductive Pair (A : Type) (B : Type) { mkPair : A → B → Pair A B; }; g : _; -g (mkPair (mkPair zero false) true) ≔ mkPair false zero; +g (mkPair (mkPair zero false) true) := mkPair false zero; end; diff --git a/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix b/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix index cd90612ed..a65d3dd4d 100644 --- a/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix +++ b/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix @@ -15,13 +15,13 @@ inductive Bool { infixr 2 ||; || : Bool → Bool → Bool; -|| false a ≔ a; -|| true _ ≔ true; +|| false a := a; +|| true _ := true; infixr 3 &&; && : Bool → Bool → Bool; -&& false _ ≔ false; -&& true a ≔ a; +&& false _ := false; +&& true a := a; -------------------------------------------------------------------------------- -- Backend Booleans @@ -58,7 +58,7 @@ compile bool { }; from-backend-bool : BackendBool → Bool; -from-backend-bool bb ≔ bool bb true false; +from-backend-bool bb := bool bb true false; -------------------------------------------------------------------------------- -- Integers @@ -81,7 +81,7 @@ compile lt { infix 4 <; < : Int → Int → Bool; -< i1 i2 ≔ from-backend-bool (lt i1 i2); +< i1 i2 := from-backend-bool (lt i1 i2); axiom eqInt : Int → Int → BackendBool; compile eqInt { @@ -90,7 +90,7 @@ compile eqInt { infix 4 ==Int; ==Int : Int → Int → Bool; -==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2); +==Int i1 i2 := from-backend-bool (eqInt i1 i2); infixl 6 -; axiom - : Int -> Int -> Int; @@ -120,7 +120,7 @@ compile eqString { infix 4 ==String; ==String : String → String → Bool; -==String s1 s2 ≔ from-backend-bool (eqString s1 s2); +==String s1 s2 := from-backend-bool (eqString s1 s2); -------------------------------------------------------------------------------- -- Lists @@ -132,8 +132,8 @@ inductive ListString { }; elem : String → ListString → Bool; -elem s Nil ≔ false; -elem s (Cons x xs) ≔ (s ==String x) || elem s xs; +elem s Nil := false; +elem s (Cons x xs) := (s ==String x) || elem s xs; -------------------------------------------------------------------------------- -- Pair @@ -144,8 +144,8 @@ inductive PairIntBool { }; if-pairIntBool : Bool → PairIntBool → PairIntBool → PairIntBool; -if-pairIntBool true x _ ≔ x; -if-pairIntBool false _ y ≔ y; +if-pairIntBool true x _ := x; +if-pairIntBool false _ y := y; -------------------------------------------------------------------------------- -- Optionals @@ -157,15 +157,15 @@ inductive OptionInt { }; if-optionInt : Bool → OptionInt → OptionInt → OptionInt; -if-optionInt true x _ ≔ x; -if-optionInt false _ y ≔ y; +if-optionInt true x _ := x; +if-optionInt false _ y := y; from-int : Int → OptionInt; -from-int i ≔ if-optionInt (i < Int_0) NothingInt (JustInt i); +from-int i := if-optionInt (i < Int_0) NothingInt (JustInt i); maybe-int : Int → OptionInt → Int; -maybe-int d NothingInt ≔ d; -maybe-int _ (JustInt i) ≔ i; +maybe-int d NothingInt := d; +maybe-int _ (JustInt i) := i; inductive OptionString { NothingString : OptionString; @@ -173,23 +173,23 @@ inductive OptionString { }; if-optionString : Bool → OptionString → OptionString → OptionString; -if-optionString true x _ ≔ x; -if-optionString false _ y ≔ y; +if-optionString true x _ := x; +if-optionString false _ y := y; from-string : String → OptionString; -from-string s ≔ if-optionString (s ==String "") NothingString (JustString s); +from-string s := if-optionString (s ==String "") NothingString (JustString s); pair-from-optionString : (String → PairIntBool) → OptionString → PairIntBool; -pair-from-optionString _ NothingString ≔ MakePair Int_0 false; -pair-from-optionString f (JustString o) ≔ f o; +pair-from-optionString _ NothingString := MakePair Int_0 false; +pair-from-optionString f (JustString o) := f o; -------------------------------------------------------------------------------- -- foldl -------------------------------------------------------------------------------- foldl : (PairIntBool → String → PairIntBool) → PairIntBool → ListString → PairIntBool; -foldl f z Nil ≔ z; -foldl f z (Cons h hs) ≔ foldl f (f z h) hs; +foldl f z Nil := z; +foldl f z (Cons h hs) := foldl f (f z h) hs; -------------------------------------------------------------------------------- -- Anoma @@ -211,26 +211,26 @@ compile isBalanceKey { }; read-pre : String → OptionInt; -read-pre s ≔ from-int (readPre s); +read-pre s := from-int (readPre s); read-post : String → OptionInt; -read-post s ≔ from-int (readPost s); +read-post s := from-int (readPost s); is-balance-key : String → String → OptionString; -is-balance-key token key ≔ from-string (isBalanceKey token key); +is-balance-key token key := from-string (isBalanceKey token key); unwrap-default : OptionInt → Int; -unwrap-default o ≔ maybe-int Int_0 o; +unwrap-default o := maybe-int Int_0 o; -------------------------------------------------------------------------------- -- Validity Predicate -------------------------------------------------------------------------------- change-from-key : String → Int; -change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key); +change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); check-vp : ListString → String → Int → String → PairIntBool; -check-vp verifiers key change owner ≔ +check-vp verifiers key change owner := if-pairIntBool (change-from-key key < Int_0) -- make sure the spender approved the transaction @@ -238,17 +238,17 @@ check-vp verifiers key change owner ≔ (MakePair (change + (change-from-key key)) true); check-keys : String → ListString → PairIntBool → String → PairIntBool; -check-keys token verifiers (MakePair change is-success) key ≔ +check-keys token verifiers (MakePair change is-success) key := if-pairIntBool is-success (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) (MakePair Int_0 false); check-result : PairIntBool → Bool; -check-result (MakePair change all-checked) ≔ (change ==Int Int_0) && all-checked; +check-result (MakePair change all-checked) := (change ==Int Int_0) && all-checked; vp : String → ListString → ListString → Bool; -vp token keys-changed verifiers ≔ +vp token keys-changed verifiers := check-result (foldl (check-keys token verifiers) @@ -282,33 +282,33 @@ compile >> { }; show-result : Bool → String; -show-result true ≔ "OK"; -show-result false ≔ "FAIL"; +show-result true := "OK"; +show-result false := "FAIL"; -------------------------------------------------------------------------------- -- Testing VP -------------------------------------------------------------------------------- token : String; -token ≔ "owner-token"; +token := "owner-token"; owner-address : String; -owner-address ≔ "owner-address"; +owner-address := "owner-address"; change1-key : String; -change1-key ≔ "change1-key"; +change1-key := "change1-key"; change2-key : String; -change2-key ≔ "change2-key"; +change2-key := "change2-key"; verifiers : ListString; -verifiers ≔ Cons owner-address Nil; +verifiers := Cons owner-address Nil; keys-changed : ListString; -keys-changed ≔ Cons change1-key (Cons change2-key Nil); +keys-changed := Cons change1-key (Cons change2-key Nil); main : Action; -main ≔ +main := (putStr "VP Status: ") >> (putStrLn (show-result (vp token keys-changed verifiers))); diff --git a/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix index 1b22e9815..b3dc5b9ad 100644 --- a/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix +++ b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix @@ -15,17 +15,17 @@ inductive Bool { infixr 2 ||; || : Bool → Bool → Bool; -|| false a ≔ a; -|| true _ ≔ true; +|| false a := a; +|| true _ := true; infixr 3 &&; && : Bool → Bool → Bool; -&& false _ ≔ false; -&& true a ≔ a; +&& false _ := false; +&& true a := a; if : {A : Type} → Bool → A → A → A; -if true a _ ≔ a; -if false _ b ≔ b; +if true a _ := a; +if false _ b := b; -------------------------------------------------------------------------------- -- Backend Booleans @@ -63,14 +63,14 @@ compile bool { }; from-backend-bool : BackendBool → Bool; -from-backend-bool bb ≔ bool bb true false; +from-backend-bool bb := bool bb true false; -------------------------------------------------------------------------------- -- Functions -------------------------------------------------------------------------------- id : {A : Type} → A → A; -id a ≔ a; +id a := a; -------------------------------------------------------------------------------- -- Integers @@ -100,7 +100,7 @@ compile <' { infix 4 <; < : Int → Int → Bool; -< i1 i2 ≔ from-backend-bool (i1 <' i2); +< i1 i2 := from-backend-bool (i1 <' i2); axiom eqInt : Int → Int → BackendBool; compile eqInt { @@ -109,7 +109,7 @@ compile eqInt { infix 4 ==Int; ==Int : Int → Int → Bool; -==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2); +==Int i1 i2 := from-backend-bool (eqInt i1 i2); infixl 6 -; axiom - : Int -> Int -> Int; @@ -139,7 +139,7 @@ compile eqString { infix 4 ==String; ==String : String → String → Bool; -==String s1 s2 ≔ from-backend-bool (eqString s1 s2); +==String s1 s2 := from-backend-bool (eqString s1 s2); -------------------------------------------------------------------------------- -- Lists @@ -152,12 +152,12 @@ inductive List (A : Type) { }; elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil ≔ false; -elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs; +elem _ _ nil := false; +elem eq s (x ∷ xs) := eq s x || elem eq s xs; foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil ≔ z; -foldl f z (h ∷ hs) ≔ foldl f (f z h) hs; +foldl f z nil := z; +foldl f z (h ∷ hs) := foldl f (f z h) hs; -------------------------------------------------------------------------------- -- Pair @@ -179,17 +179,17 @@ inductive Maybe (A : Type) { }; from-int : Int → Maybe Int; -from-int i ≔ if (i < Int_0) nothing (just i); +from-int i := if (i < Int_0) nothing (just i); maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; -maybe b _ nothing ≔ b; -maybe _ f (just x) ≔ f x; +maybe b _ nothing := b; +maybe _ f (just x) := f x; from-string : String → Maybe String; -from-string s ≔ if (s ==String "") nothing (just s); +from-string s := if (s ==String "") nothing (just s); pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString ≔ maybe (Int_0, false); +pair-from-optionString := maybe (Int_0, false); -------------------------------------------------------------------------------- -- Anoma @@ -211,26 +211,26 @@ compile isBalanceKey { }; read-pre : String → Maybe Int; -read-pre s ≔ from-int (readPre s); +read-pre s := from-int (readPre s); read-post : String → Maybe Int; -read-post s ≔ from-int (readPost s); +read-post s := from-int (readPost s); is-balance-key : String → String → Maybe String; -is-balance-key token key ≔ from-string (isBalanceKey token key); +is-balance-key token key := from-string (isBalanceKey token key); unwrap-default : Maybe Int → Int; -unwrap-default ≔ maybe Int_0 id; +unwrap-default := maybe Int_0 id; -------------------------------------------------------------------------------- -- Validity Predicate -------------------------------------------------------------------------------- change-from-key : String → Int; -change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key); +change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner ≔ +check-vp verifiers key change owner := if (change-from-key key < Int_0) -- make sure the spender approved the transaction @@ -238,17 +238,17 @@ check-vp verifiers key change owner ≔ (change + (change-from-key key), true); check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change, is-success) key ≔ +check-keys token verifiers (change, is-success) key := if is-success (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) (Int_0, false); check-result : Int × Bool → Bool; -check-result (change, all-checked) ≔ (change ==Int Int_0) && all-checked; +check-result (change, all-checked) := (change ==Int Int_0) && all-checked; vp : String → List String → List String → Bool; -vp token keys-changed verifiers ≔ +vp token keys-changed verifiers := check-result (foldl (check-keys token verifiers) @@ -281,33 +281,33 @@ compile >> { }; show-result : Bool → String; -show-result true ≔ "OK"; -show-result false ≔ "FAIL"; +show-result true := "OK"; +show-result false := "FAIL"; -------------------------------------------------------------------------------- -- Testing VP -------------------------------------------------------------------------------- token : String; -token ≔ "owner-token"; +token := "owner-token"; owner-address : String; -owner-address ≔ "owner-address"; +owner-address := "owner-address"; change1-key : String; -change1-key ≔ "change1-key"; +change1-key := "change1-key"; change2-key : String; -change2-key ≔ "change2-key"; +change2-key := "change2-key"; verifiers : List String; -verifiers ≔ owner-address ∷ nil; +verifiers := owner-address ∷ nil; keys-changed : List String; -keys-changed ≔ change1-key ∷ change2-key ∷ nil; +keys-changed := change1-key ∷ change2-key ∷ nil; main : Action; -main ≔ +main := (putStr "VP Status: ") >> (putStrLn (show-result (vp token keys-changed verifiers))); diff --git a/tests/positive/Imports/A.juvix b/tests/positive/Imports/A.juvix index 9f8c44266..9d33b702d 100644 --- a/tests/positive/Imports/A.juvix +++ b/tests/positive/Imports/A.juvix @@ -11,5 +11,5 @@ module A; end ; import M; f : M.N.T; - f (_ M.N.t _) ≔ Type M.+ Type; + f (_ M.N.t _) := Type M.+ Type; end; diff --git a/tests/positive/Internal/Box.juvix b/tests/positive/Internal/Box.juvix index e92e2a47a..235da4f55 100644 --- a/tests/positive/Internal/Box.juvix +++ b/tests/positive/Internal/Box.juvix @@ -9,12 +9,12 @@ module Box; }; b : Box _; -b ≔ box t; +b := box t; id : {A : Type} → A → A; -id x ≔ x; +id x := x; tt : _; -tt ≔ id t +tt := id t end; diff --git a/tests/positive/Internal/HoleInSignature.juvix b/tests/positive/Internal/HoleInSignature.juvix index f225dfc25..93992efca 100644 --- a/tests/positive/Internal/HoleInSignature.juvix +++ b/tests/positive/Internal/HoleInSignature.juvix @@ -12,6 +12,6 @@ p : Pair _ _; p := mkPair true false; p2 : (A : Type) → (B : Type) → _ → B → Pair A _; -p2 _ _ a b ≔ mkPair a b; +p2 _ _ a b := mkPair a b; end; diff --git a/tests/positive/Internal/Implicit.juvix b/tests/positive/Internal/Implicit.juvix index 88c5a34dd..2929de6fb 100644 --- a/tests/positive/Internal/Implicit.juvix +++ b/tests/positive/Internal/Implicit.juvix @@ -2,7 +2,7 @@ module Implicit; infixr 9 ∘; ∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C; -∘ f g x ≔ f (g x); +∘ f g x := f (g x); inductive Nat { zero : Nat; @@ -16,25 +16,25 @@ inductive × (A : Type) (B : Type) { }; uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → C; -uncurry f (a, b) ≔ f a b; +uncurry f (a, b) := f a b; fst : {A : Type} → {B : Type} → A × B → A; -fst (a, _) ≔ a; +fst (a, _) := a; snd : {A : Type} → {B : Type} → A × B → B; -snd (_, b) ≔ b; +snd (_, b) := b; swap : {A : Type} → {B : Type} → A × B → B × A; -swap (a, b) ≔ b, a; +swap (a, b) := b, a; first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B; -first f (a, b) ≔ f a, b; +first f (a, b) := f a, b; second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B'; -second f (a, b) ≔ a, f b; +second f (a, b) := a, f b; both : {A : Type} → {B : Type} → (A → B) → A × A → B × B; -both f (a, b) ≔ f a, f b; +both f (a, b) := f a, f b; inductive Bool { true : Bool; @@ -42,8 +42,8 @@ inductive Bool { }; if : {A : Type} → Bool → A → A → A; -if true a _ ≔ a; -if false _ b ≔ b; +if true a _ := a; +if false _ b := b; infixr 5 ∷; inductive List (A : Type) { @@ -52,71 +52,71 @@ inductive List (A : Type) { }; upToTwo : _; -upToTwo ≔ zero ∷ suc zero ∷ suc (suc zero) ∷ nil; +upToTwo := zero ∷ suc zero ∷ suc (suc zero) ∷ nil; p1 : Nat → Nat → Nat × Nat; -p1 a b ≔ a, b ; +p1 a b := a, b ; inductive Proxy (A : Type) { proxy : Proxy A; }; t2' : {A : Type} → Proxy A; -t2' ≔ proxy; +t2' := proxy; t2 : {A : Type} → Proxy A; -t2 ≔ proxy; +t2 := proxy; t3 : ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B; -t3 _ _ ≔ proxy; +t3 _ _ := proxy; t4 : {B : Type} → Proxy B; -t4 {_} ≔ t3 proxy proxy; +t4 {_} := t3 proxy proxy; t4' : {B : Type} → Proxy B; -t4' ≔ t3 proxy proxy ; +t4' := t3 proxy proxy ; map : {A : Type} → {B : Type} → (A → B) → List A → List B; -map f nil ≔ nil; -map f (x ∷ xs) ≔ f x ∷ map f xs; +map f nil := nil; +map f (x ∷ xs) := f x ∷ map f xs; t : {A : Type} → Proxy A; -t {_} ≔ proxy; +t {_} := proxy; t' : {A : Type} → Proxy A; -t' ≔ proxy; +t' := proxy; t5 : {A : Type} → Proxy A → Proxy A; -t5 p ≔ p; +t5 p := p; t5' : {A : Type} → Proxy A → Proxy A; -t5' proxy ≔ proxy; +t5' proxy := proxy; f : {A : Type} → {B : Type} → A → B → _; -f a b ≔ a; +f a b := a; pairEval : {A : Type} → {B : Type} → (A → B) × A → B; -pairEval (f, x) ≔ f x; +pairEval (f, x) := f x; pairEval' : {A : Type} → {B : Type} → ({C : Type} → A → B) × A → B; -pairEval' (f, x) ≔ f {Nat} x; +pairEval' (f, x) := f {Nat} x; foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B; -foldr _ z nil ≔ z; -foldr f z (h ∷ hs) ≔ f h (foldr f z hs); +foldr _ z nil := z; +foldr f z (h ∷ hs) := f h (foldr f z hs); foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil ≔ z ; -foldl f z (h ∷ hs) ≔ foldl f (f z h) hs; +foldl f z nil := z ; +foldl f z (h ∷ hs) := foldl f (f z h) hs; filter : {A : Type} → (A → Bool) → List A → List A; -filter _ nil ≔ nil; -filter f (h ∷ hs) ≔ if (f h) +filter _ nil := nil; +filter f (h ∷ hs) := if (f h) (h ∷ filter f hs) (filter f hs); partition : {A : Type} → (A → Bool) → List A → List A × List A; -partition _ nil ≔ nil, nil; -partition f (x ∷ xs) ≔ (if (f x) first second) ((∷) x) (partition f xs); +partition _ nil := nil, nil; +partition f (x ∷ xs) := (if (f x) first second) ((∷) x) (partition f xs); end; diff --git a/tests/positive/Internal/Lambda.juvix b/tests/positive/Internal/Lambda.juvix index 35dcb734d..182736181 100644 --- a/tests/positive/Internal/Lambda.juvix +++ b/tests/positive/Internal/Lambda.juvix @@ -31,10 +31,10 @@ uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × uncurry := λ {f (a, b) := f a b}; idB : {A : Type} → A → A; -idB a ≔ λ { a := a} a; +idB a := λ { a := a} a; mapB : {A : Type} → (A → A) → A → A; -mapB ≔ λ { f a := f a}; +mapB := λ { f a := f a}; add : Nat → Nat → Nat; add := λ {zero n := n; (suc n) := λ {m := suc (add n m) }}; diff --git a/tests/positive/Internal/LiteralInt.juvix b/tests/positive/Internal/LiteralInt.juvix index 7d22b82c5..0ccc415c3 100644 --- a/tests/positive/Internal/LiteralInt.juvix +++ b/tests/positive/Internal/LiteralInt.juvix @@ -8,6 +8,6 @@ module LiteralInt; b : B; }; - f : ℕ; - f ≔ 1; + f : Nat; + f := 1; end; diff --git a/tests/positive/Internal/LiteralString.juvix b/tests/positive/Internal/LiteralString.juvix index 5269f33e6..9df3e4ce5 100644 --- a/tests/positive/Internal/LiteralString.juvix +++ b/tests/positive/Internal/LiteralString.juvix @@ -8,5 +8,5 @@ module LiteralString; }; f : A; - f ≔ "a"; + f := "a"; end; diff --git a/tests/positive/Internal/Mutual.juvix b/tests/positive/Internal/Mutual.juvix index af1bb2cc5..1d064cb70 100644 --- a/tests/positive/Internal/Mutual.juvix +++ b/tests/positive/Internal/Mutual.juvix @@ -11,16 +11,16 @@ inductive Nat { }; not : _; -not false ≔ true; -not true ≔ false; +not false := true; +not true := false; odd : _; even : _; -odd zero ≔ false; -odd (suc n) ≔ even n; +odd zero := false; +odd (suc n) := even n; -even zero ≔ true; -even (suc n) ≔ odd n; +even zero := true; +even (suc n) := odd n; end; diff --git a/tests/positive/Internal/Simple.juvix b/tests/positive/Internal/Simple.juvix index 16a5d4e6f..d6a1e1d57 100644 --- a/tests/positive/Internal/Simple.juvix +++ b/tests/positive/Internal/Simple.juvix @@ -4,7 +4,7 @@ module Simple; }; someT : T; - someT ≔ tt; + someT := tt; inductive Bool { false : Bool; @@ -19,14 +19,14 @@ module Simple; infix 3 ==; == : Nat → Nat → Bool; - == zero zero ≔ true; - == (suc a) (suc b) ≔ a == b; - == _ _ ≔ false; + == zero zero := true; + == (suc a) (suc b) := a == b; + == _ _ := false; infixl 4 +; + : Nat → Nat → Nat; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); infixr 5 ∷; inductive List { @@ -35,10 +35,10 @@ module Simple; }; foldr : (Nat → Nat → Nat) → Nat → List → Nat; - foldr _ v nil ≔ v; - foldr f v (a ∷ as) ≔ f a (foldr f v as); + foldr _ v nil := v; + foldr f v (a ∷ as) := f a (foldr f v as); sum : List → Nat; - sum ≔ foldr (+) zero; + sum := foldr (+) zero; end; diff --git a/tests/positive/Judoc.juvix b/tests/positive/Judoc.juvix index 1b7924f87..005e4fcfa 100644 --- a/tests/positive/Judoc.juvix +++ b/tests/positive/Judoc.juvix @@ -11,11 +11,11 @@ inductive T { --- hahahah --- and another one ;T; id : {A : Type} → A → A; -id a ≔ a; +id a := a; --- hellowww id2 : {A : Type} → A → A; -id2 a ≔ a; +id2 a := a; end; diff --git a/tests/positive/MiniC/AlwaysValidVP/Input.juvix b/tests/positive/MiniC/AlwaysValidVP/Input.juvix index f24b951aa..6058778ba 100644 --- a/tests/positive/MiniC/AlwaysValidVP/Input.juvix +++ b/tests/positive/MiniC/AlwaysValidVP/Input.juvix @@ -28,11 +28,11 @@ compile AnomaBool_false { }; encodeBool : Bool → AnomaBool; -encodeBool true ≔ AnomaBool_true; -encodeBool false ≔ AnomaBool_false; +encodeBool true := AnomaBool_true; +encodeBool false := AnomaBool_false; --- The module entrypoint callable by wasm runtime _validate_tx : AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaBool; -_validate_tx _ _ _ _ _ _ _ _ ≔ encodeBool true; +_validate_tx _ _ _ _ _ _ _ _ := encodeBool true; end; diff --git a/tests/positive/MiniC/AxiomNoCompile/Input.juvix b/tests/positive/MiniC/AxiomNoCompile/Input.juvix index 587ae8bf3..0b1092a17 100644 --- a/tests/positive/MiniC/AxiomNoCompile/Input.juvix +++ b/tests/positive/MiniC/AxiomNoCompile/Input.juvix @@ -9,6 +9,6 @@ inductive Unit { axiom ignore : Unit -> Unit; main : IO; -main ≔ putStrLn "Hello"; +main := putStrLn "Hello"; end; diff --git a/tests/positive/MiniC/Builtins/Input.juvix b/tests/positive/MiniC/Builtins/Input.juvix index 78f6f8883..aef30a98b 100644 --- a/tests/positive/MiniC/Builtins/Input.juvix +++ b/tests/positive/MiniC/Builtins/Input.juvix @@ -9,18 +9,18 @@ inductive ℕ { infixl 4 +; builtin natural-plus + : ℕ → ℕ → ℕ; -+ zero x ≔ x; -+ (suc a) b ≔ suc (a + b); ++ zero x := x; ++ (suc a) b := suc (a + b); mult : ℕ → ℕ → ℕ; -mult zero _ ≔ zero; -mult (suc n) m ≔ m + (mult n m); +mult zero _ := zero; +mult (suc n) m := m + (mult n m); plusOne : ℕ → ℕ; -plusOne ≔ suc; +plusOne := suc; someLiteral : _; -someLiteral ≔ 123; +someLiteral := 123; builtin IO axiom IO : Type; @@ -29,6 +29,6 @@ builtin IO-sequence axiom >> : IO → IO → IO; builtin natural-print axiom printNat : ℕ → IO; main : IO; -main ≔ printNat (mult 3 (2 + 2)) >> printNat 2; +main := printNat (mult 3 (2 + 2)) >> printNat 2; end; diff --git a/tests/positive/MiniC/ClosureEnv/Input.juvix b/tests/positive/MiniC/ClosureEnv/Input.juvix index 92e3c476a..a406c8b76 100644 --- a/tests/positive/MiniC/ClosureEnv/Input.juvix +++ b/tests/positive/MiniC/ClosureEnv/Input.juvix @@ -42,60 +42,60 @@ inductive Nat { }; nplus : Nat → Nat → Nat; -nplus zero n ≔ n; -nplus (suc m) n ≔ suc (nplus m n); +nplus zero n := n; +nplus (suc m) n := suc (nplus m n); nplus-to-int : Nat → Int; -nplus-to-int zero ≔ Int_0; -nplus-to-int (suc n) ≔ plus Int_1 (nplus-to-int n); +nplus-to-int zero := Int_0; +nplus-to-int (suc n) := plus Int_1 (nplus-to-int n); nOne : Nat; -nOne ≔ suc zero; +nOne := suc zero; nplusOne : Nat → Nat → Nat; -nplusOne n ≔ nplus nOne; +nplusOne n := nplus nOne; plusOneInt : Int → Int; -plusOneInt ≔ plus Int_1; +plusOneInt := plus Int_1; one : Int; -one ≔ Int_1; +one := Int_1; two : Int; -two ≔ plusOneInt one; +two := plusOneInt one; three : Int; -three ≔ plusOneInt two; +three := plusOneInt two; plusXIgnore2 : Int → Int → Int → Int → Int; -plusXIgnore2 _ _ ≔ plus; +plusXIgnore2 _ _ := plus; plusXIgnore : Int → Int → Int → Int; -plusXIgnore _ ≔ plus; +plusXIgnore _ := plus; plusXIgnore22 : Int → Int → Int → Int → Int; -plusXIgnore22 _ ≔ plusXIgnore; +plusXIgnore22 _ := plusXIgnore; plusX : Int → Int → Int; -plusX ≔ plus; +plusX := plus; plusXThree : Int → Int; -plusXThree ≔ plusX three; +plusXThree := plusX three; plusOne : Int → Int; -plusOne ≔ plus one; +plusOne := plus one; plusOneThenTwo : Int; -plusOneThenTwo ≔ plusOne two; +plusOneThenTwo := plusOne two; plusOneThenX : Int → Int; -plusOneThenX x ≔ plusOne x; +plusOneThenX x := plusOne x; plusOneTwo : Int; -plusOneTwo ≔ plus one two; +plusOneTwo := plus one two; main : Action; -main ≔ put-str "plusOne one: " >> put-str-ln (to-str (plusOne one)) +main := put-str "plusOne one: " >> put-str-ln (to-str (plusOne one)) >> put-str "plusOneThenTwo: " >> put-str-ln (to-str (plusOneThenTwo)) >> put-str "plusOneThenX three: " >> put-str-ln (to-str (plusOneThenX three)) >> put-str "plusOneTwo: " >> put-str-ln (to-str (plusOneTwo)) diff --git a/tests/positive/MiniC/ClosureNoEnv/Input.juvix b/tests/positive/MiniC/ClosureNoEnv/Input.juvix index 09ad15d26..1c7379292 100644 --- a/tests/positive/MiniC/ClosureNoEnv/Input.juvix +++ b/tests/positive/MiniC/ClosureNoEnv/Input.juvix @@ -42,7 +42,7 @@ compile plus { }; apply : (Int → Int → Int) → Int → Int → Int; -apply f a b ≔ f a b; +apply f a b := f a b; inductive Nat { zero : Nat; @@ -50,30 +50,30 @@ inductive Nat { }; plus-nat : Nat → Nat → Nat; -plus-nat zero n ≔ n; -plus-nat (suc m) n ≔ suc (plus-nat m n); +plus-nat zero n := n; +plus-nat (suc m) n := suc (plus-nat m n); apply-nat : (Nat → Nat) → Nat → Nat; -apply-nat f a ≔ f a; +apply-nat f a := f a; apply-nat2 : (Nat → Nat → Nat) → Nat → Nat → Nat; -apply-nat2 f a b ≔ f a b; +apply-nat2 f a b := f a b; nat-to-int : Nat → Int; -nat-to-int zero ≔ Int_0; -nat-to-int (suc n) ≔ plus Int_1 (nat-to-int n); +nat-to-int zero := Int_0; +nat-to-int (suc n) := plus Int_1 (nat-to-int n); one : Nat; -one ≔ suc zero; +one := suc zero; nest-apply : ((Nat → Nat) → Nat → Nat) → (Nat → Nat) → Nat → Nat; -nest-apply f g x ≔ f g x; +nest-apply f g x := f g x; two : Nat; -two ≔ suc one; +two := suc one; main : Action; -main ≔ put-str "plus 1 2: " +main := put-str "plus 1 2: " >> put-str-ln (to-str (apply plus Int_1 Int_2)) >> put-str "suc one: " >> put-str-ln (to-str (nat-to-int (apply-nat suc one))) diff --git a/tests/positive/MiniC/ExportName/Input.juvix b/tests/positive/MiniC/ExportName/Input.juvix index dbbbba4f2..f6a2c96bc 100644 --- a/tests/positive/MiniC/ExportName/Input.juvix +++ b/tests/positive/MiniC/ExportName/Input.juvix @@ -2,7 +2,7 @@ module Input; open import Stdlib.Prelude; -fun : ℕ; -fun ≔ six; +fun : Nat; +fun := six; end; diff --git a/tests/positive/MiniC/ExportNameArgs/Input.juvix b/tests/positive/MiniC/ExportNameArgs/Input.juvix index 27591bb6d..d3e4fdc90 100644 --- a/tests/positive/MiniC/ExportNameArgs/Input.juvix +++ b/tests/positive/MiniC/ExportNameArgs/Input.juvix @@ -2,7 +2,7 @@ module Input; open import Stdlib.Prelude; -fun : ℕ → ℕ; -fun _ ≔ three; +fun : Nat → Nat; +fun _ := three; end; diff --git a/tests/positive/MiniC/HelloWorld/Input.juvix b/tests/positive/MiniC/HelloWorld/Input.juvix index 6e927eb90..145750293 100644 --- a/tests/positive/MiniC/HelloWorld/Input.juvix +++ b/tests/positive/MiniC/HelloWorld/Input.juvix @@ -20,6 +20,6 @@ compile put-str-ln { }; main : Action; -main ≔ put-str-ln "hello world!"; +main := put-str-ln "hello world!"; end; diff --git a/tests/positive/MiniC/HigherOrder/Input.juvix b/tests/positive/MiniC/HigherOrder/Input.juvix index 893724791..83bff1752 100644 --- a/tests/positive/MiniC/HigherOrder/Input.juvix +++ b/tests/positive/MiniC/HigherOrder/Input.juvix @@ -96,24 +96,24 @@ inductive Nat { infixl 6 +; + : Nat → Nat → Nat; -+ zero n ≔ n; -+ (suc m) n ≔ suc (m + n); ++ zero n := n; ++ (suc m) n := suc (m + n); to-int : Nat → Int; -to-int zero ≔ Int_0; -to-int (suc n) ≔ Int_1 +int (to-int n); +to-int zero := Int_0; +to-int (suc n) := Int_1 +int (to-int n); nat-to-str : Nat → String; -nat-to-str n ≔ to-str (to-int n); +nat-to-str n := to-str (to-int n); one : Nat; -one ≔ suc zero; +one := suc zero; two : Nat; -two ≔ suc one; +two := suc one; three : Nat; -three ≔ suc two; +three := suc two; -------------------------------------------------------------------------------- -- Lists @@ -125,20 +125,20 @@ inductive ListNat { }; foldl : (Nat → Nat → Nat) → Nat → ListNat → Nat; -foldl _ z null ≔ z; -foldl f z (cons n hs) ≔ foldl f (f z n) hs; +foldl _ z null := z; +foldl f z (cons n hs) := foldl f (f z n) hs; l : ListNat; -l ≔ cons one (cons two null); +l := cons one (cons two null); sum : ListNat → Nat; -sum l ≔ foldl (+) zero l; +sum l := foldl (+) zero l; sum-is-three : Action; -sum-is-three ≔ put-str "list sum is: " +sum-is-three := put-str "list sum is: " >> put-str-ln (nat-to-str (sum l)); main : Action; -main ≔ sum-is-three +main := sum-is-three end; diff --git a/tests/positive/MiniC/ImportExportName/Input.juvix b/tests/positive/MiniC/ImportExportName/Input.juvix index 11707af40..6b5ab0bea 100644 --- a/tests/positive/MiniC/ImportExportName/Input.juvix +++ b/tests/positive/MiniC/ImportExportName/Input.juvix @@ -5,6 +5,6 @@ open import Stdlib.Prelude; axiom hostDisplayString : String → IO; juvixRender : IO; -juvixRender ≔ hostDisplayString "Hello World from Juvix!"; +juvixRender := hostDisplayString "Hello World from Juvix!"; end; diff --git a/tests/positive/MiniC/Lib/Data/Bool.juvix b/tests/positive/MiniC/Lib/Data/Bool.juvix index f4b1314f3..6e278857b 100644 --- a/tests/positive/MiniC/Lib/Data/Bool.juvix +++ b/tests/positive/MiniC/Lib/Data/Bool.juvix @@ -8,11 +8,11 @@ inductive Bool { }; not : Bool → Bool; -not true ≔ false; -not false ≔ true; +not true := false; +not false := true; boolToStr : Bool → String; -boolToStr true ≔ "true"; -boolToStr false ≔ "false"; +boolToStr true := "true"; +boolToStr false := "false"; end; diff --git a/tests/positive/MiniC/Lib/Data/Nat.juvix b/tests/positive/MiniC/Lib/Data/Nat.juvix index 2e2c60183..e6b1f3a19 100644 --- a/tests/positive/MiniC/Lib/Data/Nat.juvix +++ b/tests/positive/MiniC/Lib/Data/Nat.juvix @@ -22,13 +22,13 @@ compile natInd { }; natToInt : Nat → Int; -natToInt zero ≔ 0; -natToInt (suc n) ≔ 1 + (natToInt n); +natToInt zero := 0; +natToInt (suc n) := 1 + (natToInt n); natToStr : Nat → String; -natToStr n ≔ intToStr (natToInt n); +natToStr n := intToStr (natToInt n); intToNat : Int → Nat; -intToNat x ≔ natInd x zero suc; +intToNat x := natInd x zero suc; end; diff --git a/tests/positive/MiniC/Lib/Data/Pair.juvix b/tests/positive/MiniC/Lib/Data/Pair.juvix index 190bb55c8..ea6b70192 100644 --- a/tests/positive/MiniC/Lib/Data/Pair.juvix +++ b/tests/positive/MiniC/Lib/Data/Pair.juvix @@ -5,7 +5,7 @@ inductive Pair (A : Type) (B : Type) { }; fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) ≔ a; +fst _ _ (mkPair a b) := a; end; diff --git a/tests/positive/MiniC/MultiModules/Data/Bool.juvix b/tests/positive/MiniC/MultiModules/Data/Bool.juvix index f4b1314f3..6e278857b 100644 --- a/tests/positive/MiniC/MultiModules/Data/Bool.juvix +++ b/tests/positive/MiniC/MultiModules/Data/Bool.juvix @@ -8,11 +8,11 @@ inductive Bool { }; not : Bool → Bool; -not true ≔ false; -not false ≔ true; +not true := false; +not false := true; boolToStr : Bool → String; -boolToStr true ≔ "true"; -boolToStr false ≔ "false"; +boolToStr true := "true"; +boolToStr false := "false"; end; diff --git a/tests/positive/MiniC/MultiModules/Data/Nat.juvix b/tests/positive/MiniC/MultiModules/Data/Nat.juvix index cb0e5ea1c..b660df69f 100644 --- a/tests/positive/MiniC/MultiModules/Data/Nat.juvix +++ b/tests/positive/MiniC/MultiModules/Data/Nat.juvix @@ -22,13 +22,13 @@ compile natInd { }; natToInt : Nat → Int; -natToInt zero ≔ Int_0; -natToInt (suc n) ≔ Int_1 + (natToInt n); +natToInt zero := Int_0; +natToInt (suc n) := Int_1 + (natToInt n); natToStr : Nat → String; -natToStr n ≔ intToStr (natToInt n); +natToStr n := intToStr (natToInt n); intToNat : Int → Nat; -intToNat x ≔ natInd x zero suc; +intToNat x := natInd x zero suc; end; diff --git a/tests/positive/MiniC/MultiModules/Data/Pair.juvix b/tests/positive/MiniC/MultiModules/Data/Pair.juvix index 190bb55c8..ea6b70192 100644 --- a/tests/positive/MiniC/MultiModules/Data/Pair.juvix +++ b/tests/positive/MiniC/MultiModules/Data/Pair.juvix @@ -5,7 +5,7 @@ inductive Pair (A : Type) (B : Type) { }; fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) ≔ a; +fst _ _ (mkPair a b) := a; end; diff --git a/tests/positive/MiniC/MultiModules/Input.juvix b/tests/positive/MiniC/MultiModules/Input.juvix index ceebfba7b..f6b90c606 100644 --- a/tests/positive/MiniC/MultiModules/Input.juvix +++ b/tests/positive/MiniC/MultiModules/Input.juvix @@ -12,18 +12,18 @@ open import Data.IO; open import Prelude; bool-to-str : Bool → String; -bool-to-str true ≔ "True"; -bool-to-str false ≔ "False"; +bool-to-str true := "True"; +bool-to-str false := "False"; -------------------------------------------------------------------------------- -- Main -------------------------------------------------------------------------------- fst-of-pair : Action; -fst-of-pair ≔ (put-str "fst (True, False) = ") +fst-of-pair := (put-str "fst (True, False) = ") >> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false))); main : Action; -main ≔ fst-of-pair; +main := fst-of-pair; end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix index f4b1314f3..6e278857b 100644 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix +++ b/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix @@ -8,11 +8,11 @@ inductive Bool { }; not : Bool → Bool; -not true ≔ false; -not false ≔ true; +not true := false; +not false := true; boolToStr : Bool → String; -boolToStr true ≔ "true"; -boolToStr false ≔ "false"; +boolToStr true := "true"; +boolToStr false := "false"; end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix index cb0e5ea1c..b660df69f 100644 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix +++ b/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix @@ -22,13 +22,13 @@ compile natInd { }; natToInt : Nat → Int; -natToInt zero ≔ Int_0; -natToInt (suc n) ≔ Int_1 + (natToInt n); +natToInt zero := Int_0; +natToInt (suc n) := Int_1 + (natToInt n); natToStr : Nat → String; -natToStr n ≔ intToStr (natToInt n); +natToStr n := intToStr (natToInt n); intToNat : Int → Nat; -intToNat x ≔ natInd x zero suc; +intToNat x := natInd x zero suc; end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix index 190bb55c8..ea6b70192 100644 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix +++ b/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix @@ -5,7 +5,7 @@ inductive Pair (A : Type) (B : Type) { }; fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) ≔ a; +fst _ _ (mkPair a b) := a; end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Input.juvix b/tests/positive/MiniC/MutuallyRecursive/Input.juvix index 00fc608fa..259861123 100644 --- a/tests/positive/MiniC/MutuallyRecursive/Input.juvix +++ b/tests/positive/MiniC/MutuallyRecursive/Input.juvix @@ -6,23 +6,23 @@ odd : Nat → Bool; even : Nat → Bool; -odd zero ≔ false; -odd (suc n) ≔ even n; +odd zero := false; +odd (suc n) := even n; -even zero ≔ true; -even (suc n) ≔ odd n; +even zero := true; +even (suc n) := odd n; check : (Nat → Bool) → Int → String; -check f x ≔ boolToStr (f (intToNat x)); +check f x := boolToStr (f (intToNat x)); checkEven : Int → String; -checkEven ≔ check even; +checkEven := check even; checkOdd : Int → String; -checkOdd ≔ check odd; +checkOdd := check odd; main : Action; -main ≔ put-str "even 1: " >> put-str-ln (checkEven Int_1) +main := put-str "even 1: " >> put-str-ln (checkEven Int_1) >> put-str "even 4: " >> put-str-ln (checkEven Int_4) >> put-str "even 9: " >> put-str-ln (checkEven Int_9) >> put-str "odd 1: " >> put-str-ln (checkOdd Int_1) diff --git a/tests/positive/MiniC/Nat/Input.juvix b/tests/positive/MiniC/Nat/Input.juvix index 157a34e2b..a0ca312f8 100644 --- a/tests/positive/MiniC/Nat/Input.juvix +++ b/tests/positive/MiniC/Nat/Input.juvix @@ -60,8 +60,8 @@ compile put-str-ln { }; bool-to-str : Bool → String; -bool-to-str true ≔ "True"; -bool-to-str false ≔ "False"; +bool-to-str true := "True"; +bool-to-str false := "False"; -------------------------------------------------------------------------------- -- Integers @@ -115,62 +115,62 @@ inductive Nat { infixl 6 +; + : Nat → Nat → Nat; -+ zero n ≔ n; -+ (suc m) n ≔ suc (m + n); ++ zero n := n; ++ (suc m) n := suc (m + n); is-even : Nat → Bool; -is-even zero ≔ true; -is-even (suc (suc n)) ≔ is-even n; -is-even _ ≔ false; +is-even zero := true; +is-even (suc (suc n)) := is-even n; +is-even _ := false; infix 4 ==Nat; ==Nat : Nat → Nat → Bool; -==Nat zero zero ≔ true; -==Nat (suc n) (suc m) ≔ n ==Nat m; -==Nat _ _ ≔ false; +==Nat zero zero := true; +==Nat (suc n) (suc m) := n ==Nat m; +==Nat _ _ := false; to-int : Nat → Int; -to-int zero ≔ Int_0; -to-int (suc n) ≔ Int_1 +int (to-int n); +to-int zero := Int_0; +to-int (suc n) := Int_1 +int (to-int n); nat-to-str : Nat → String; -nat-to-str n ≔ to-str (to-int n); +nat-to-str n := to-str (to-int n); one : Nat; -one ≔ suc zero; +one := suc zero; two : Nat; -two ≔ suc one; +two := suc one; three : Nat; -three ≔ suc two; +three := suc two; -------------------------------------------------------------------------------- -- Main -------------------------------------------------------------------------------- three-plus-suc-one : Action; -three-plus-suc-one ≔ (put-str "3 + (1 + 1) = ") +three-plus-suc-one := (put-str "3 + (1 + 1) = ") >> put-str-ln (nat-to-str (three + (suc one))); three-eq-suc-two : Action; -three-eq-suc-two ≔ (put-str "3 == 1 + 2 : ") +three-eq-suc-two := (put-str "3 == 1 + 2 : ") >> put-str-ln (bool-to-str (three ==Nat (one + two))); three-neq-two : Action; -three-neq-two ≔ (put-str "3 == 2 : ") +three-neq-two := (put-str "3 == 2 : ") >> put-str-ln (bool-to-str (three ==Nat two)); three-is-not-even : Action; -three-is-not-even ≔ (put-str "is-even 3 : ") +three-is-not-even := (put-str "is-even 3 : ") >> put-str-ln (bool-to-str (is-even three)); four-is-even : Action; -four-is-even ≔ (put-str "is-even 4 : ") +four-is-even := (put-str "is-even 4 : ") >> put-str-ln (bool-to-str (is-even (suc three))); main : Action; -main ≔ three-plus-suc-one +main := three-plus-suc-one >> three-eq-suc-two >> three-neq-two >> three-is-not-even diff --git a/tests/positive/MiniC/NestedList/Input.juvix b/tests/positive/MiniC/NestedList/Input.juvix index 94f7e2717..8be7b1b1d 100644 --- a/tests/positive/MiniC/NestedList/Input.juvix +++ b/tests/positive/MiniC/NestedList/Input.juvix @@ -13,9 +13,9 @@ inductive Foo { }; l : List (List Foo) → List (List Foo); -l ((_ ∷ nil) ∷ nil) ≔ nil ∷ nil; +l ((_ ∷ nil) ∷ nil) := nil ∷ nil; main : Action; -main ≔ put-str-ln "no errors"; +main := put-str-ln "no errors"; end; diff --git a/tests/positive/MiniC/Polymorphism/Input.juvix b/tests/positive/MiniC/Polymorphism/Input.juvix index 920f7edb6..cf151bcd5 100644 --- a/tests/positive/MiniC/Polymorphism/Input.juvix +++ b/tests/positive/MiniC/Polymorphism/Input.juvix @@ -60,8 +60,8 @@ compile put-str-ln { }; bool-to-str : Bool → String; -bool-to-str true ≔ "True"; -bool-to-str false ≔ "False"; +bool-to-str true := "True"; +bool-to-str false := "False"; infixr 2 ×; infixr 4 ,; @@ -70,20 +70,20 @@ inductive × (A : Type) (B : Type) { }; fst : {A : Type} → {B : Type} → A × B → A; -fst (a, b) ≔ a; +fst (a, b) := a; id' : {A : Type} → A → A; -id' a ≔ fst (a, a); +id' a := fst (a, a); -------------------------------------------------------------------------------- -- Main -------------------------------------------------------------------------------- fst-of-pair : Action; -fst-of-pair ≔ (put-str "fst (True, False) = ") +fst-of-pair := (put-str "fst (True, False) = ") >> put-str-ln (bool-to-str (fst (true, false))); main : Action; -main ≔ fst-of-pair >> put-str-ln (bool-to-str (id' false)); +main := fst-of-pair >> put-str-ln (bool-to-str (id' false)); end; diff --git a/tests/positive/MiniC/PolymorphismHoles/Input.juvix b/tests/positive/MiniC/PolymorphismHoles/Input.juvix index ad86454cc..84959c5e2 100644 --- a/tests/positive/MiniC/PolymorphismHoles/Input.juvix +++ b/tests/positive/MiniC/PolymorphismHoles/Input.juvix @@ -60,8 +60,8 @@ compile put-str-ln { }; bool-to-str : Bool → String; -bool-to-str true ≔ "True"; -bool-to-str false ≔ "False"; +bool-to-str true := "True"; +bool-to-str false := "False"; -------------------------------------------------------------------------------- @@ -73,17 +73,17 @@ inductive Pair (A : Type) (B : Type) { }; fst : {A : Type} → {B : Type} → Pair A B → A; -fst (mkPair a b) ≔ a; +fst (mkPair a b) := a; -------------------------------------------------------------------------------- -- Main -------------------------------------------------------------------------------- fst-of-pair : Action; -fst-of-pair ≔ (put-str "fst (True, False) = ") +fst-of-pair := (put-str "fst (True, False) = ") >> put-str-ln (bool-to-str (fst (mkPair true false))); main : Action; -main ≔ fst-of-pair; +main := fst-of-pair; end; diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix b/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix index 1c03b48aa..80f767aaa 100644 --- a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix +++ b/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix @@ -37,17 +37,17 @@ inductive Bool { infixr 2 ||; || : Bool → Bool → Bool; -|| false a ≔ a; -|| true _ ≔ true; +|| false a := a; +|| true _ := true; infixr 3 &&; && : Bool → Bool → Bool; -&& false _ ≔ false; -&& true a ≔ a; +&& false _ := false; +&& true a := a; if : {A : Type} → Bool → A → A → A; -if true a _ ≔ a; -if false _ b ≔ b; +if true a _ := a; +if false _ b := b; -------------------------------------------------------------------------------- -- Backend Booleans @@ -84,14 +84,14 @@ compile bool { }; from-backend-bool : BackendBool → Bool; -from-backend-bool bb ≔ bool bb true false; +from-backend-bool bb := bool bb true false; -------------------------------------------------------------------------------- -- Functions -------------------------------------------------------------------------------- id : {A : Type} → A → A; -id a ≔ a; +id a := a; -------------------------------------------------------------------------------- -- Integers @@ -134,10 +134,10 @@ compile <' { infix 4 <; < : Int → Int → Bool; -< i1 i2 ≔ from-backend-bool (i1 <' i2); +< i1 i2 := from-backend-bool (i1 <' i2); isNegative : Int → Bool; -isNegative n ≔ n < Int_0; +isNegative n := n < Int_0; axiom eqInt : Int → Int → BackendBool; compile eqInt { @@ -146,7 +146,7 @@ compile eqInt { infix 4 ==Int; ==Int : Int → Int → Bool; -==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2); +==Int i1 i2 := from-backend-bool (eqInt i1 i2); infixl 6 -; axiom - : Int -> Int -> Int; @@ -182,7 +182,7 @@ compile eqString { infix 4 ==String; ==String : String → String → Bool; -==String s1 s2 ≔ from-backend-bool (eqString s1 s2); +==String s1 s2 := from-backend-bool (eqString s1 s2); -------------------------------------------------------------------------------- -- Lists @@ -195,12 +195,12 @@ inductive List (A : Type) { }; elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil ≔ false; -elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs; +elem _ _ nil := false; +elem eq s (x ∷ xs) := eq s x || elem eq s xs; foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil ≔ z; -foldl f z (h ∷ hs) ≔ foldl f (f z h) hs; +foldl f z nil := z; +foldl f z (h ∷ hs) := foldl f (f z h) hs; -------------------------------------------------------------------------------- -- Pair @@ -222,17 +222,17 @@ inductive Maybe (A : Type) { }; from-int : Int → Maybe Int; -from-int i ≔ if (isNegative i) nothing (just i); +from-int i := if (isNegative i) nothing (just i); maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; -maybe b _ nothing ≔ b; -maybe _ f (just x) ≔ f x; +maybe b _ nothing := b; +maybe _ f (just x) := f x; from-string : String → Maybe String; -from-string s ≔ if (s ==String "") nothing (just s); +from-string s := if (s ==String "") nothing (just s); pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString ≔ maybe (Int_0, false); +pair-from-optionString := maybe (Int_0, false); -------------------------------------------------------------------------------- -- Anoma @@ -254,26 +254,26 @@ compile isBalanceKey { }; read-pre : String → Maybe Int; -read-pre s ≔ from-int (readPre s); +read-pre s := from-int (readPre s); read-post : String → Maybe Int; -read-post s ≔ from-int (readPost s); +read-post s := from-int (readPost s); is-balance-key : String → String → Maybe String; -is-balance-key token key ≔ from-string (isBalanceKey token key); +is-balance-key token key := from-string (isBalanceKey token key); unwrap-default : Maybe Int → Int; -unwrap-default ≔ maybe Int_0 id; +unwrap-default := maybe Int_0 id; -------------------------------------------------------------------------------- -- Validity Predicate -------------------------------------------------------------------------------- change-from-key : String → Int; -change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key); +change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner ≔ +check-vp verifiers key change owner := if (isNegative (change-from-key key)) -- make sure the spender approved the transaction @@ -281,17 +281,17 @@ check-vp verifiers key change owner ≔ (change + (change-from-key key), true); check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change, is-success) key ≔ +check-keys token verifiers (change, is-success) key := if is-success (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) (Int_0, false); check-result : Int × Bool → Bool; -check-result (change, all-checked) ≔ (change ==Int Int_0) && all-checked; +check-result (change, all-checked) := (change ==Int Int_0) && all-checked; vp : String → List String → List String → Bool; -vp token keys-changed verifiers ≔ +vp token keys-changed verifiers := check-result (foldl (check-keys token verifiers) @@ -330,33 +330,33 @@ compile >> { }; show-result : Bool → String; -show-result true ≔ "OK"; -show-result false ≔ "FAIL"; +show-result true := "OK"; +show-result false := "FAIL"; -------------------------------------------------------------------------------- -- Testing VP -------------------------------------------------------------------------------- token : String; -token ≔ "owner-token"; +token := "owner-token"; owner-address : String; -owner-address ≔ "owner-address"; +owner-address := "owner-address"; change1-key : String; -change1-key ≔ "change1-key"; +change1-key := "change1-key"; change2-key : String; -change2-key ≔ "change2-key"; +change2-key := "change2-key"; verifiers : List String; -verifiers ≔ owner-address ∷ nil; +verifiers := owner-address ∷ nil; keys-changed : List String; -keys-changed ≔ change1-key ∷ change2-key ∷ nil; +keys-changed := change1-key ∷ change2-key ∷ nil; main : Action; -main ≔ +main := (putStr "VP Status: ") >> (putStrLn (show-result (vp token keys-changed verifiers))); diff --git a/tests/positive/MiniC/StdlibImport/Input.juvix b/tests/positive/MiniC/StdlibImport/Input.juvix index e274d8173..ca781dc1e 100644 --- a/tests/positive/MiniC/StdlibImport/Input.juvix +++ b/tests/positive/MiniC/StdlibImport/Input.juvix @@ -7,6 +7,6 @@ open import Stdlib.Data.Nat; open import Stdlib.System.IO; main : IO; -main ≔ putStrLn (natToStr (two + three)); +main := putStrLn (natToStr (two + three)); end; diff --git a/tests/positive/MiniHaskell/HelloWorld.juvix b/tests/positive/MiniHaskell/HelloWorld.juvix index 98a89915e..2973f53c9 100644 --- a/tests/positive/MiniHaskell/HelloWorld.juvix +++ b/tests/positive/MiniHaskell/HelloWorld.juvix @@ -13,13 +13,13 @@ inductive V { infixl 6 +; + : ℕ → ℕ → ℕ; -+ zero b ≔ b; -+ (suc a) b ≔ suc (a + b); ++ zero b := b; ++ (suc a) b := suc (a + b); infixl 7 *; * : ℕ → ℕ → ℕ; -* zero b ≔ zero; -* (suc a) b ≔ b + (a * b); +* zero b := zero; +* (suc a) b := b + (a * b); axiom Action : Type; compile Action { @@ -40,11 +40,11 @@ compile putStr { }; doTimes : ℕ → Action → Action; -doTimes zero _ ≔ putStr "done"; -doTimes (suc n) a ≔ a >> doTimes n a; +doTimes zero _ := putStr "done"; +doTimes (suc n) a := a >> doTimes n a; three : ℕ; -three ≔ suc (suc (suc zero)); +three := suc (suc (suc zero)); main : Action; main := doTimes three (putStr "hello world"); diff --git a/tests/positive/Operators.juvix b/tests/positive/Operators.juvix index 192821c4f..7a141ea0d 100644 --- a/tests/positive/Operators.juvix +++ b/tests/positive/Operators.juvix @@ -4,12 +4,12 @@ module Operators; axiom + : Type → Type → Type; plus : Type → Type → Type; - plus ≔ (+); + plus := (+); plus2 : Type → Type → Type → Type; - plus2 a b c ≔ a + b + c; + plus2 a b c := a + b + c; plus3 : Type → Type → Type → Type → Type; - plus3 a b c d ≔ (+) (a + b) ((+) c d); + plus3 a b c d := (+) (a + b) ((+) c d); end; diff --git a/tests/positive/Parsing.juvix b/tests/positive/Parsing.juvix index 8bf8ae0ce..4b249abc8 100644 --- a/tests/positive/Parsing.juvix +++ b/tests/positive/Parsing.juvix @@ -1,7 +1,7 @@ module Parsing; let' : Type; - let' ≔ Type; + let' := Type; TypeMine : Type; TypeMine := Type; diff --git a/tests/positive/Polymorphism.juvix b/tests/positive/Polymorphism.juvix index 8be9a976c..25140eea9 100644 --- a/tests/positive/Polymorphism.juvix +++ b/tests/positive/Polymorphism.juvix @@ -20,85 +20,85 @@ inductive Bool { }; id : (A : Type) → A → A; -id _ a ≔ a; +id _ a := a; terminating undefined : (A : Type) → A; -undefined A ≔ undefined A; +undefined A := undefined A; add : Nat → Nat → Nat; -add zero b ≔ b; -add (suc a) b ≔ suc (add a b); +add zero b := b; +add (suc a) b := suc (add a b); nil' : (E : Type) → List E; -nil' A ≔ nil; +nil' A := nil; -- currying nil'' : (E : Type) → List E; -nil'' E ≔ nil; +nil'' E := nil; fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) ≔ a; +fst _ _ (mkPair a b) := a; p : Pair Bool Bool; -p ≔ mkPair true false; +p := mkPair true false; swap : (A : Type) → (B : Type) → Pair A B → Pair B A; -swap A B (mkPair a b) ≔ mkPair b a; +swap A B (mkPair a b) := mkPair b a; curry : (A : Type) → (B : Type) → (C : Type) → (Pair A B → C) → A → B → C; -curry A B C f a b ≔ f (mkPair a b) ; +curry A B C f a b := f (mkPair a b) ; ap : (A : Type) → (B : Type) → (A → B) → A → B; -ap A B f a ≔ f a; +ap A B f a := f a; ite : (A : Type) → Bool → A → A → A; -ite _ true tt _ ≔ tt; -ite _ false _ ff ≔ ff; +ite _ true tt _ := tt; +ite _ false _ ff := ff; headDef : (A : Type) → A → List A → A; -headDef _ d nil ≔ d; -headDef A _ (cons h _) ≔ h; +headDef _ d nil := d; +headDef A _ (cons h _) := h; filter : (A : Type) → (A → Bool) → List A → List A; -filter A f nil ≔ nil; -filter A f (cons x xs) ≔ ite (List A) (f x) (cons x (filter A f xs)) (filter A f xs); +filter A f nil := nil; +filter A f (cons x xs) := ite (List A) (f x) (cons x (filter A f xs)) (filter A f xs); map : (A : Type) → (B : Type) → (A → B) → List A → List B; -map A B f nil ≔ nil ; -map A B f (cons x xs) ≔ cons (f x) (map A B f xs); +map A B f nil := nil ; +map A B f (cons x xs) := cons (f x) (map A B f xs); zip : (A : Type) → (B : Type) → List A → List B → List (Pair A B); -zip A B nil _ ≔ nil; -zip A B _ nil ≔ nil; -zip A B (cons a as) (cons b bs) ≔ nil; +zip A B nil _ := nil; +zip A B _ nil := nil; +zip A B (cons a as) (cons b bs) := nil; zipWith : (A : Type) → (B : Type) → (C : Type) → (A → B → C) → List A → List B → List C; -zipWith A B C f nil _ ≔ nil; -zipWith A B C f _ nil ≔ nil; -zipWith A B C f (cons a as) (cons b bs) ≔ cons (f a b) (zipWith A B C f as bs); +zipWith A B C f nil _ := nil; +zipWith A B C f _ nil := nil; +zipWith A B C f (cons a as) (cons b bs) := cons (f a b) (zipWith A B C f as bs); rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat; -rankn f b n ≔ mkPair (f Bool b) (f Nat n); +rankn f b n := mkPair (f Bool b) (f Nat n); -- currying trankn : Pair Bool Nat; -trankn ≔ rankn id false zero; +trankn := rankn id false zero; l1 : List Nat; -l1 ≔ cons zero nil; +l1 := cons zero nil; pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B; -pairEval _ _ (mkPair f x) ≔ f x; +pairEval _ _ (mkPair f x) := f x; main : Nat; -main ≔ headDef Nat (pairEval Nat Nat (mkPair (add zero) zero)) +main := headDef Nat (pairEval Nat Nat (mkPair (add zero) zero)) (zipWith Nat Nat Nat add l1 l1); end; diff --git a/tests/positive/PolymorphismHoles.juvix b/tests/positive/PolymorphismHoles.juvix index 3cc60dcf1..af118f880 100644 --- a/tests/positive/PolymorphismHoles.juvix +++ b/tests/positive/PolymorphismHoles.juvix @@ -20,78 +20,78 @@ inductive Bool { }; id : (A : Type) → A → A; -id _ a ≔ a; +id _ a := a; terminating undefined : (A : Type) → A; -undefined A ≔ undefined A; +undefined A := undefined A; add : Nat → Nat → Nat; -add zero b ≔ b; -add (suc a) b ≔ suc (add a b); +add zero b := b; +add (suc a) b := suc (add a b); fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) ≔ a; +fst _ _ (mkPair a b) := a; p : Pair Bool Bool; -p ≔ mkPair true false; +p := mkPair true false; swap : (A : Type) → (B : Type) → Pair A B → Pair B A; -swap A B (mkPair a b) ≔ mkPair b a; +swap A B (mkPair a b) := mkPair b a; curry : (A : Type) → (B : Type) → (C : Type) → (Pair A B → C) → A → B → C; -curry A B C f a b ≔ f (mkPair a b) ; +curry A B C f a b := f (mkPair a b) ; ap : (A : Type) → (B : Type) → (A → B) → A → B; -ap A B f a ≔ f a; +ap A B f a := f a; headDef : (A : Type) → A → List A → A; -headDef _ d nil ≔ d; -headDef A _ (cons h _) ≔ h; +headDef _ d nil := d; +headDef A _ (cons h _) := h; ite : (A : Type) → Bool → A → A → A; -ite _ true tt _ ≔ tt; -ite _ false _ ff ≔ ff; +ite _ true tt _ := tt; +ite _ false _ ff := ff; filter : (A : Type) → (A → Bool) → List A → List A; -filter _ f nil ≔ nil; -filter _ f (cons x xs) ≔ ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs); +filter _ f nil := nil; +filter _ f (cons x xs) := ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs); map : (A : Type) → (B : Type) → (A → B) → List _ → List _; -map _ _ f nil ≔ nil; -map _ _ f (cons x xs) ≔ cons (f x) (map _ _ f xs); +map _ _ f nil := nil; +map _ _ f (cons x xs) := cons (f x) (map _ _ f xs); zip : (A : Type) → (B : Type) → List A → List B → List (Pair A B); -zip A _ nil _ ≔ nil; -zip _ _ _ nil ≔ nil; -zip _ _ (cons a as) (cons b bs) ≔ nil; +zip A _ nil _ := nil; +zip _ _ _ nil := nil; +zip _ _ (cons a as) (cons b bs) := nil; zipWith : (A : Type) → (B : Type) → (C : Type) → (A → B → C) → List A → List B → List C; -zipWith _ _ C f nil _ ≔ nil; -zipWith _ _ C f _ nil ≔ nil; -zipWith _ _ _ f (cons a as) (cons b bs) ≔ cons (f a b) (zipWith _ _ _ f as bs); +zipWith _ _ C f nil _ := nil; +zipWith _ _ C f _ nil := nil; +zipWith _ _ _ f (cons a as) (cons b bs) := cons (f a b) (zipWith _ _ _ f as bs); rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat; -rankn f b n ≔ mkPair (f _ b) (f _ n); +rankn f b n := mkPair (f _ b) (f _ n); -- currying trankn : Pair Bool Nat; -trankn ≔ rankn id false zero; +trankn := rankn id false zero; l1 : List Nat; -l1 ≔ cons zero nil; +l1 := cons zero nil; pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B; -pairEval _ _ (mkPair f x) ≔ f x; +pairEval _ _ (mkPair f x) := f x; main : Nat; -main ≔ headDef _ (pairEval _ _ (mkPair (add zero) zero)) +main := headDef _ (pairEval _ _ (mkPair (add zero) zero)) (zipWith _ _ _ add l1 l1); end; diff --git a/tests/positive/QualifiedConstructor/M.juvix b/tests/positive/QualifiedConstructor/M.juvix index d747a92b1..e45782fff 100644 --- a/tests/positive/QualifiedConstructor/M.juvix +++ b/tests/positive/QualifiedConstructor/M.juvix @@ -17,5 +17,5 @@ module M; open N.O; fun : T → T; - fun A ≔ T; + fun A := T; end; diff --git a/tests/positive/Reachability/Data/Bool.juvix b/tests/positive/Reachability/Data/Bool.juvix index a10e90af5..c3acdbbde 100644 --- a/tests/positive/Reachability/Data/Bool.juvix +++ b/tests/positive/Reachability/Data/Bool.juvix @@ -5,17 +5,17 @@ module Data.Bool; }; not : Bool → Bool; - not true ≔ false; - not false ≔ true; + not true := false; + not false := true; -- infixr 2 ||; -- || : Bool → Bool → Bool; - -- || false a ≔ a; - -- || true _ ≔ true; + -- || false a := a; + -- || true _ := true; -- infixr 2 &&; -- && : Bool → Bool → Bool; - -- && false _ ≔ false; - -- && true a ≔ a; + -- && false _ := false; + -- && true a := a; end; diff --git a/tests/positive/Reachability/Data/Nat.juvix b/tests/positive/Reachability/Data/Nat.juvix index fd26414ce..ed7202144 100644 --- a/tests/positive/Reachability/Data/Nat.juvix +++ b/tests/positive/Reachability/Data/Nat.juvix @@ -6,12 +6,12 @@ module Data.Nat; infixl 6 +; + : ℕ → ℕ → ℕ; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); infixl 7 *; * : ℕ → ℕ → ℕ; - * zero b ≔ zero; - * (suc a) b ≔ b + a * b; + * zero b := zero; + * (suc a) b := b + a * b; end; diff --git a/tests/positive/StdlibImport/StdlibImport.juvix b/tests/positive/StdlibImport/StdlibImport.juvix index 0eaa3dc9f..b88a78860 100644 --- a/tests/positive/StdlibImport/StdlibImport.juvix +++ b/tests/positive/StdlibImport/StdlibImport.juvix @@ -4,10 +4,10 @@ open import Stdlib.Prelude; import A; -two : ℕ; -two ≔ 1 + 1; +two : Nat; +two := 1 + 1; foo : A.Foo; -foo ≔ A.bar; +foo := A.bar; end; diff --git a/tests/positive/StdlibList/Data/Bool.juvix b/tests/positive/StdlibList/Data/Bool.juvix index a10e90af5..c3acdbbde 100644 --- a/tests/positive/StdlibList/Data/Bool.juvix +++ b/tests/positive/StdlibList/Data/Bool.juvix @@ -5,17 +5,17 @@ module Data.Bool; }; not : Bool → Bool; - not true ≔ false; - not false ≔ true; + not true := false; + not false := true; -- infixr 2 ||; -- || : Bool → Bool → Bool; - -- || false a ≔ a; - -- || true _ ≔ true; + -- || false a := a; + -- || true _ := true; -- infixr 2 &&; -- && : Bool → Bool → Bool; - -- && false _ ≔ false; - -- && true a ≔ a; + -- && false _ := false; + -- && true a := a; end; diff --git a/tests/positive/StdlibList/Data/List.juvix b/tests/positive/StdlibList/Data/List.juvix index 1d8c132ea..833a0fdb4 100644 --- a/tests/positive/StdlibList/Data/List.juvix +++ b/tests/positive/StdlibList/Data/List.juvix @@ -10,23 +10,23 @@ inductive List (a : Type) { }; match : {A : Type} → {B : Type} → A → (A → B) → B; -match x f ≔ f x; +match x f := f x; foldr : (a : Type) → (b : Type) → (a → b → b) → b → List a → b; -foldr _ _ _ z (nil _) ≔ z; -foldr a b f z (∷ _ h hs) ≔ f h (foldr a b f z hs); +foldr _ _ _ z (nil _) := z; +foldr a b f z (∷ _ h hs) := f h (foldr a b f z hs); foldl : (a : Type) → (b : Type) → (b → a → b) → b → List a → b; -foldl a b f z (nil _) ≔ z ; -foldl a b f z (∷ _ h hs) ≔ foldl a b f (f z h) hs; +foldl a b f z (nil _) := z ; +foldl a b f z (∷ _ h hs) := foldl a b f (f z h) hs; map : (a : Type) → (b : Type) → (a → b) → List a → List b; -map _ b f (nil _) ≔ nil b; -map a b f (∷ _ h hs) ≔ ∷ a (f h) (map a b f hs); +map _ b f (nil _) := nil b; +map a b f (∷ _ h hs) := ∷ a (f h) (map a b f hs); filter : (a : Type) → (a → Bool) → List a → List a; -filter a f (nil _) ≔ nil a; -filter a f (∷ _ h hs) ≔ match (f h) λ{ +filter a f (nil _) := nil a; +filter a f (∷ _ h hs) := match (f h) λ{ true := ∷ a h (filter a f hs); false := filter a f hs; }; @@ -35,24 +35,24 @@ import Data.Nat; open Data.Nat; length : (a : Type) → List a → ℕ; -length _ (nil _) ≔ zero; -length a (∷ _ _ l) ≔ suc (length a l); +length _ (nil _) := zero; +length a (∷ _ _ l) := suc (length a l); reverse : (a : Type) → List a → List a; -reverse a l ≔ rev l (nil a) +reverse a l := rev l (nil a) where { rev : List a → List a → List a; - rev (nil _) a ≔ a; - rev (∷ _ x xs) a ≔ rev xs (∷ a x a) + rev (nil _) a := a; + rev (∷ _ x xs) a := rev xs (∷ a x a) }; replicate : (a : Type) → ℕ → a → List a; -replicate a zero _ ≔ nil a; -replicate a (suc n) x ≔ ∷ a x (replicate a n x); +replicate a zero _ := nil a; +replicate a (suc n) x := ∷ a x (replicate a n x); take : (a : Type) → ℕ → List a → List a; -take a (suc n) (∷ _ x xs) ≔ ∷ a x (take a n xs); -take a _ _ ≔ nil a; +take a (suc n) (∷ _ x xs) := ∷ a x (take a n xs); +take a _ _ := nil a; import Data.Ord; open Data.Ord; @@ -61,40 +61,40 @@ import Data.Product; open Data.Product; splitAt : (a : Type) → ℕ → List a → List a; -splitAt a _ (nil _) ≔ nil a, nil a; -splitAt a zero xs ≔ , (List a) (List a) (nil a) xs; -splitAt a (suc zero) (∷ _ x xs) ≔ , (List a) (List a) (∷ a x (nil a)) xs; -splitAt a (suc (suc m)) (∷ _ x xs) ≔ match (splitAt a m xs) λ { +splitAt a _ (nil _) := nil a, nil a; +splitAt a zero xs := , (List a) (List a) (nil a) xs; +splitAt a (suc zero) (∷ _ x xs) := , (List a) (List a) (∷ a x (nil a)) xs; +splitAt a (suc (suc m)) (∷ _ x xs) := match (splitAt a m xs) λ { (, la _ xs' xs'') := , la la (∷ a x xs') xs''; }; merge : (a : Type) → (a → a → Ordering) → List a → List a → List a; -merge a cmp (∷ _ x xs) (∷ _ y ys) ≔ match (cmp x y) λ{ +merge a cmp (∷ _ x xs) (∷ _ y ys) := match (cmp x y) λ{ LT := ∷ a x (merge a cmp xs (∷ a y ys)); _ := ∷ a y (merge a cmp (∷ a x xs) ys); }; -merge _ _ (nil _) ys ≔ ys; -merge _ _ xs (nil _) ≔ xs; +merge _ _ (nil _) ys := ys; +merge _ _ xs (nil _) := xs; -- infixr 5 ++; waiting for implicit arguments ++ : (a : Type) → List a → List a → List a; -++ a (nil _) ys ≔ ys; -++ a (∷ _ x xs) ys ≔ ∷ a x (++ a xs ys); +++ a (nil _) ys := ys; +++ a (∷ _ x xs) ys := ∷ a x (++ a xs ys); quickSort : (a : Type) → (a → a → Ordering) → List a → List a; -quickSort a _ (nil _) ≔ nil a; -quickSort a _ (∷ _ x (nil _)) ≔ ∷ a x (nil a); -quickSort a cmp (∷ _ x ys) ≔ +quickSort a _ (nil _) := nil a; +quickSort a _ (∷ _ x (nil _)) := ∷ a x (nil a); +quickSort a cmp (∷ _ x ys) := ++ a (quickSort a (filter a ltx) ys) (++ a (∷ a x (nil a)) (quickSort a (filter a gex) ys)) where { ltx : a → Bool; - ltx y ≔ match (cmp y x) λ{ + ltx y := match (cmp y x) λ{ LT := true; _ := false; }; gex : a → Bool; - gex y ≔ not (ltx y) + gex y := not (ltx y) }; end; diff --git a/tests/positive/StdlibList/Data/Nat.juvix b/tests/positive/StdlibList/Data/Nat.juvix index fd26414ce..ed7202144 100644 --- a/tests/positive/StdlibList/Data/Nat.juvix +++ b/tests/positive/StdlibList/Data/Nat.juvix @@ -6,12 +6,12 @@ module Data.Nat; infixl 6 +; + : ℕ → ℕ → ℕ; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); infixl 7 *; * : ℕ → ℕ → ℕ; - * zero b ≔ zero; - * (suc a) b ≔ b + a * b; + * zero b := zero; + * (suc a) b := b + a * b; end; diff --git a/tests/positive/Symbols.juvix b/tests/positive/Symbols.juvix index c7539bcd0..9449085c2 100644 --- a/tests/positive/Symbols.juvix +++ b/tests/positive/Symbols.juvix @@ -2,30 +2,30 @@ module Symbols; open import Stdlib.Data.Nat; - ╘⑽╛ : ℕ; - ╘⑽╛ ≔ suc nine; + ╘⑽╛ : Nat; + ╘⑽╛ := suc nine; -- no - function!? - - : ℕ -> ℕ -> ℕ; - - ≔ (+); + - : Nat -> Nat -> Nat; + - := (+); - （-） : ℕ -> ℕ -> ℕ; - （-） ≔ (-); + （-） : Nat -> Nat -> Nat; + （-） := (-); - （*） : ℕ -> ℕ -> ℕ; - （*） ≔ (*); + （*） : Nat -> Nat -> Nat; + （*） := (*); infixl 6 －; - － : ℕ -> ℕ -> ℕ; - － ≔ （-）; + － : Nat -> Nat -> Nat; + － := （-）; infixl 7 ·; - · : ℕ -> ℕ -> ℕ; - · ≔ （*）; + · : Nat -> Nat -> Nat; + · := （*）; - （0） : ℕ; - （0） ≔ ╘⑽╛ － ╘⑽╛ · zero; + （0） : Nat; + （0） := ╘⑽╛ － ╘⑽╛ · zero; - 主功能 : ℕ; - 主功能 ≔ （0）; -end; \ No newline at end of file + 主功能 : Nat; + 主功能 := （0）; +end; diff --git a/tests/positive/Termination/Ack.juvix b/tests/positive/Termination/Ack.juvix index eb496f399..7b19f65b4 100644 --- a/tests/positive/Termination/Ack.juvix +++ b/tests/positive/Termination/Ack.juvix @@ -3,8 +3,8 @@ module Ack; open Data.Nat; ack : ℕ → ℕ → ℕ; - ack zero n ≔ suc n; - ack (suc m) zero ≔ ack m (suc zero); - ack (suc m) (suc n) ≔ ack m (ack (suc m) n); + ack zero n := suc n; + ack (suc m) zero := ack m (suc zero); + ack (suc m) (suc n) := ack m (ack (suc m) n); end; diff --git a/tests/positive/Termination/Data/Bool.juvix b/tests/positive/Termination/Data/Bool.juvix index ee344f54a..914c42b1e 100644 --- a/tests/positive/Termination/Data/Bool.juvix +++ b/tests/positive/Termination/Data/Bool.juvix @@ -5,21 +5,21 @@ module Data.Bool; }; not : Bool → Bool; - not true ≔ false; - not false ≔ true; + not true := false; + not false := true; infixr 2 ||; || : Bool → Bool → Bool; - || false a ≔ a; - || true _ ≔ true; + || false a := a; + || true _ := true; infixr 2 &&; && : Bool → Bool → Bool; - && false _ ≔ false; - && true a ≔ a; + && false _ := false; + && true a := a; ite : {a : Type} → Bool → a → a → a; - ite true a _ ≔ a; - ite false _ b ≔ b; + ite true a _ := a; + ite false _ b := b; end; diff --git a/tests/positive/Termination/Data/List.juvix b/tests/positive/Termination/Data/List.juvix index c40a32e93..ba71c5125 100644 --- a/tests/positive/Termination/Data/List.juvix +++ b/tests/positive/Termination/Data/List.juvix @@ -13,44 +13,44 @@ inductive List (A : Type) { -- Do not remove implicit arguments. Useful for testing. foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B; -foldr _ z nil ≔ z; -foldr f z (cons h hs) ≔ f h (foldr {_} f z hs); +foldr _ z nil := z; +foldr f z (cons h hs) := f h (foldr {_} f z hs); foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil ≔ z ; -foldl {_} {_} f z (cons h hs) ≔ foldl {_} f (f z h) hs; +foldl f z nil := z ; +foldl {_} {_} f z (cons h hs) := foldl {_} f (f z h) hs; map : {A : Type} → {B : Type} → (A → B) → List A → List B; -map f nil ≔ nil; -map f (cons h hs) ≔ cons (f h) (map f hs); +map f nil := nil; +map f (cons h hs) := cons (f h) (map f hs); filter : {A : Type} → (A → Bool) → List A → List A; -filter f nil ≔ nil; -filter f (cons h hs) ≔ ite (f h) +filter f nil := nil; +filter f (cons h hs) := ite (f h) (cons h (filter {_} f hs)) (filter f hs); length : {A : Type} → List A → ℕ; -length nil ≔ zero; -length {_} (cons _ l) ≔ suc (length l); +length nil := zero; +length {_} (cons _ l) := suc (length l); rev : {A : Type} → List A → List A → List A; -rev nil l ≔ l; -rev (cons x xs) l ≔ rev xs (cons {_} x l); +rev nil l := l; +rev (cons x xs) l := rev xs (cons {_} x l); reverse : {A : Type} → List A → List A; -reverse l ≔ rev l nil; +reverse l := rev l nil; replicate : {A : Type} → ℕ → A → List A; -replicate zero _ ≔ nil; -replicate (suc n) x ≔ cons x (replicate n x); +replicate zero _ := nil; +replicate (suc n) x := cons x (replicate n x); take : {A : Type} → ℕ → List A → List A; -take (suc n) (cons x xs) ≔ cons x (take n xs); -take _ _ ≔ nil; +take (suc n) (cons x xs) := cons x (take n xs); +take _ _ := nil; concat : {A : Type} → List A → List A → List A; -concat nil ys ≔ ys; -concat (cons x xs) ys ≔ cons x (concat xs ys); +concat nil ys := ys; +concat (cons x xs) ys := cons x (concat xs ys); end; diff --git a/tests/positive/Termination/Data/Nat.juvix b/tests/positive/Termination/Data/Nat.juvix index ddf832bbf..991df50bd 100644 --- a/tests/positive/Termination/Data/Nat.juvix +++ b/tests/positive/Termination/Data/Nat.juvix @@ -6,13 +6,13 @@ module Data.Nat; infixl 6 +; + : ℕ → ℕ → ℕ; - + zero b ≔ b; - + (suc a) b ≔ suc (a + b); + + zero b := b; + + (suc a) b := suc (a + b); infixl 7 *; * : ℕ → ℕ → ℕ; - * zero b ≔ zero; - * (suc a) b ≔ b + a * b; + * zero b := zero; + * (suc a) b := b + a * b; import Data.Bool; open Data.Bool; @@ -20,9 +20,9 @@ module Data.Nat; even : ℕ → Bool; odd : ℕ → Bool; - even zero ≔ true; - even (suc n) ≔ odd n; + even zero := true; + even (suc n) := odd n; - odd zero ≔ false; - odd (suc n) ≔ even n; + odd zero := false; + odd (suc n) := even n; end; diff --git a/tests/positive/Termination/Fib.juvix b/tests/positive/Termination/Fib.juvix index 7e5cec23b..a05359b94 100644 --- a/tests/positive/Termination/Fib.juvix +++ b/tests/positive/Termination/Fib.juvix @@ -7,8 +7,8 @@ inductive Nat { infixl 6 +; + : Nat → Nat → Nat; -+ zero b ≔ b; -+ (suc a) b ≔ suc (a + b); ++ zero b := b; ++ (suc a) b := suc (a + b); fib : Nat -> Nat; fib zero := zero; diff --git a/tests/positive/TypeAlias.juvix b/tests/positive/TypeAlias.juvix index 78f344ec1..9312aad70 100644 --- a/tests/positive/TypeAlias.juvix +++ b/tests/positive/TypeAlias.juvix @@ -9,32 +9,32 @@ inductive T2 { }; alias : Type; -alias ≔ T; +alias := T; x : alias; -x ≔ t; +x := t; id : Type → Type; -id x ≔ x; +id x := x; infixr 9 ⊙; ⊙ : (Type → Type) → (Type → Type) → Type → Type; -⊙ f g x ≔ f (g x); +⊙ f g x := f (g x); x2 : (id ⊙ id) alias; -x2 ≔ t; +x2 := t; flip : (Type → Type → Type) → id Type → Type → (id ⊙ id) Type; -flip f a b ≔ f b a; +flip f a b := f b a; inductive Pair (A : Type) (B : Type) { mkPair : id T → id (id A) → B → Pair A B; }; p : {A : Type} → A → Pair A A; -p a ≔ mkPair t a a; +p a := mkPair t a a; x' : flip Pair (id _) T2; -x' ≔ mkPair x t2 t; +x' := mkPair x t2 t; end;