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

remove ≔ from the language and replace it by := (#1563)

Browse Source 
* 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
This commit is contained in:
janmasrovira 2022-09-30 02:55:32 +02:00 committed by GitHub
parent f0ade4be7c
commit 803d2008d9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
126 changed files with 864 additions and 866 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.org
View File

@ -126,7 +126,7 @@ module HelloWorld;
open import Stdlib.Prelude;
main : IO;
main ≔ putStrLn "hello world!";
main := putStrLn "hello world!";
end;
#+end_src

2
docs/org/examples/backend-specific/minic-hello-world.org
View File

@ -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

76
docs/org/examples/validity-predicates/PolyFungibleToken.org
View File

@ -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)));

4
docs/org/language-reference/builtins.org
View File

@ -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.

2
docs/org/language-reference/foreign-blocks.org
View File

@ -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

8
docs/org/language-reference/functions.org
View File

@ -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

8
docs/org/language-reference/inductive-data-types.org
View File

@ -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

4
docs/org/notes/builtins.org
View File

@ -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:

24
docs/org/notes/monomorphization.org
View File

@ -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ₖ

2
docs/org/tutorials/nodejs-interop.org
View File

@ -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

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

@ -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;

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

@ -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;

30
examples/milestone/Hanoi/Hanoi.juvix
View File

@ -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;

2
examples/milestone/HelloWorld/HelloWorld.juvix
View File

@ -4,6 +4,6 @@ module HelloWorld;
open import Stdlib.Prelude;
main : IO;
main ≔ putStrLn "hello world!";
main := putStrLn "hello world!";
end;

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

@ -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;

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

@ -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;

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

@ -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;

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

@ -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;

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

@ -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;

10
examples/milestone/TicTacToe/Logic/GameState.juvix
View File

@ -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;

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

@ -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;

14
examples/milestone/TicTacToe/Logic/Symbol.juvix
View File

@ -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;

120
examples/milestone/TicTacToe/Web/TicTacToe.juvix
View File

@ -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;

12
examples/milestone/ValidityPredicates/Anoma/Base.juvix
View File

@ -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;

4
examples/milestone/ValidityPredicates/Data/Int/Ops.juvix
View File

@ -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;

12
examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix
View File

@ -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)

18
examples/milestone/ValidityPredicates/Tests.juvix
View File

@ -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)));

2
juvix-stdlib

@ -1 +1 @@
Subproject commit 5228caaf13c55db942a60dba50bce8cbc74d0497
Subproject commit 2c765890271b536f1c6247a4f00ce6f5e688aed0

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

@ -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

2
src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs
View File

@ -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

2
src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
View File

@ -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_

4
src/Juvix/Data/CodeAnn.hs
View File

@ -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

3
src/Juvix/Extra/Strings.hs
View File

@ -122,9 +122,6 @@ using = "using"
where_ :: IsString s => s
where_ = "where"
assignUnicode :: IsString s => s
assignUnicode = "≔"
assignAscii :: IsString s => s
assignAscii = ":="

18
src/Juvix/Parser/Lexer.hs
View File

@ -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

2
tests/CLI/Commands/dev/internal.test
View File

@ -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

2
tests/CLI/Commands/typecheck.test
View File

@ -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

4
tests/Core/positive/lambda-lifting/test1.out
View File

@ -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)

10
tests/Core/positive/lambda-lifting/test2.out
View File

@ -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)

10
tests/Core/positive/lambda-lifting/test3.out
View File

@ -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))

16
tests/negative/230/Foo/Data/Bool.juvix
View File

@ -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;

2
tests/negative/230/Prod.juvix
View File

@ -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;

4
tests/negative/265/M.juvix
View File

@ -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;

2
tests/negative/AmbiguousConstructor.juvix
View File

@ -15,5 +15,5 @@ module AmbiguousConstructor;
open N;
f : T1 -> T2;
f A ≔ N.A;
f A := N.A;
end;

2
tests/negative/AppLeftImplicit.juvix
View File

@ -1,6 +1,6 @@
module AppLeftImplicit;
x : Type;
x ≔ {x};
x := {x};
end;

2
tests/negative/BindGroupConflict/Clause.juvix
View File

@ -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;

2
tests/negative/BindGroupConflict/Lambda.juvix
View File

@ -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;

2
tests/negative/InfixErrorP.juvix
View File

@ -7,6 +7,6 @@ module InfixErrorP;
};
fst : Pair → Type;
fst (x , ) ≔ x;
fst (x , ) := x;
end;

2
tests/negative/Internal/ExpectedExplicitArgument.juvix
View File

@ -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;

2
tests/negative/Internal/ExpectedExplicitPattern.juvix
View File

@ -4,5 +4,5 @@ module ExpectedExplicitPattern;
};
f : {A : Type} → T A → A;
f {_} {c a} ≔ a;
f {_} {c a} := a;
end;

2
tests/negative/Internal/ExpectedFunctionType.juvix
View File

@ -8,5 +8,5 @@ module ExpectedFunctionType;
};
f : Pair B → Pair B;
f (mkPair a b) ≔ a b;
f (mkPair a b) := a b;
end;

2
tests/negative/Internal/FunctionApplied.juvix
View File

@ -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;

2
tests/negative/Internal/FunctionPattern.juvix
View File

@ -4,5 +4,5 @@ module FunctionPattern;
};
f : (T → T) → T;
f A ≔ A;
f A := A;
end;

2
tests/negative/Internal/LhsTooManyPatterns.juvix
View File

@ -4,5 +4,5 @@ module LhsTooManyPatterns;
};
f : T → T;
f A x ≔ A;
f A x := A;
end;

4
tests/negative/Internal/MultiWrongType.juvix
View File

@ -8,8 +8,8 @@ module MultiWrongType;
};
f : A;
f ≔ b;
f := b;
g : B;
g ≔ a;
g := a;
end;

2
tests/negative/Internal/PatternConstructor.juvix
View File

@ -8,6 +8,6 @@ inductive B {
};
f : A → B;
f b ≔ b;
f b := b;
end;

2
tests/negative/Internal/TooManyArguments.juvix
View File

@ -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;

2
tests/negative/Internal/UnsolvedMeta.juvix
View File

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

2
tests/negative/Internal/WrongConstructorArity.juvix
View File

@ -4,5 +4,5 @@ module WrongConstructorArity;
};
f : T → T;
f (A i x) ≔ i;
f (A i x) := i;
end;

2
tests/negative/Internal/WrongType.juvix
View File

@ -8,5 +8,5 @@ module WrongType;
};
f : A;
f ≔ b;
f := b;
end;

2
tests/negative/LacksTypeSig.juvix
View File

@ -1,6 +1,6 @@
module LacksTypeSig;
some ≔ Type;
some := Type;
end;

2
tests/negative/NestedPatternBraces.juvix
View File

@ -1,6 +1,6 @@
module NestedPatternBraces;
a : {A : Type} → Type;
a {{A}} ≔ a;
a {{A}} := a;
end;

16
tests/negative/Termination/Data/Bool.juvix
View File

@ -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;

16
tests/negative/Termination/Data/Nat.juvix
View File

@ -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;

18
tests/negative/Termination/Data/QuickSort.juvix
View File

@ -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))

2
tests/negative/issue1344/D.juvix
View File

@ -3,6 +3,6 @@ module D;
import U;
u : Other.Unit;
u ≔ U.t;
u := U.t;
end;

2
tests/negative/issue1344/M.juvix
View File

@ -6,6 +6,6 @@ module M;
};
u : Other.Unit;
u ≔ t;
u := t;
end;

4
tests/positive/265/M.juvix
View File

@ -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;

6
tests/positive/272/M.juvix
View File

@ -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;

84
tests/positive/FullExamples/MonoSimpleFungibleToken.juvix
View File

@ -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)));

76
tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix
View File

@ -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)));

2
tests/positive/Imports/A.juvix
View File

@ -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;

6
tests/positive/Internal/Box.juvix
View File

@ -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;

2
tests/positive/Internal/HoleInSignature.juvix
View File

@ -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;

68
tests/positive/Internal/Implicit.juvix
View File

@ -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;

4
tests/positive/Internal/Lambda.juvix
View File

@ -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) }};

4
tests/positive/Internal/LiteralInt.juvix
View File

@ -8,6 +8,6 @@ module LiteralInt;
b : B;
};
f : ℕ;
f ≔ 1;
f : Nat;
f := 1;
end;

2
tests/positive/Internal/LiteralString.juvix
View File

@ -8,5 +8,5 @@ module LiteralString;
};
f : A;
f ≔ "a";
f := "a";
end;

12
tests/positive/Internal/Mutual.juvix
View File

@ -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;

18
tests/positive/Internal/Simple.juvix
View File

@ -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;

4
tests/positive/Judoc.juvix
View File

@ -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;

6
tests/positive/MiniC/AlwaysValidVP/Input.juvix
View File

@ -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;

2
tests/positive/MiniC/AxiomNoCompile/Input.juvix
View File

@ -9,6 +9,6 @@ inductive Unit {
axiom ignore : Unit -> Unit;
main : IO;
main ≔ putStrLn "Hello";
main := putStrLn "Hello";
end;

14
tests/positive/MiniC/Builtins/Input.juvix
View File

@ -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;

40
tests/positive/MiniC/ClosureEnv/Input.juvix
View File

@ -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))

22
tests/positive/MiniC/ClosureNoEnv/Input.juvix
View File

@ -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)))

4
tests/positive/MiniC/ExportName/Input.juvix
View File

@ -2,7 +2,7 @@ module Input;
open import Stdlib.Prelude;
fun : ℕ;
fun ≔ six;
fun : Nat;
fun := six;
end;

4
tests/positive/MiniC/ExportNameArgs/Input.juvix
View File

@ -2,7 +2,7 @@ module Input;
open import Stdlib.Prelude;
fun : ℕ → ℕ;
fun _ ≔ three;
fun : Nat → Nat;
fun _ := three;
end;

2
tests/positive/MiniC/HelloWorld/Input.juvix
View File

@ -20,6 +20,6 @@ compile put-str-ln {
};
main : Action;
main ≔ put-str-ln "hello world!";
main := put-str-ln "hello world!";
end;

28
tests/positive/MiniC/HigherOrder/Input.juvix
View File

@ -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;

2
tests/positive/MiniC/ImportExportName/Input.juvix
View File

@ -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;

8
tests/positive/MiniC/Lib/Data/Bool.juvix
View File

@ -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;

8
tests/positive/MiniC/Lib/Data/Nat.juvix
View File

@ -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;

2
tests/positive/MiniC/Lib/Data/Pair.juvix
View File

@ -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;

8
tests/positive/MiniC/MultiModules/Data/Bool.juvix
View File

@ -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;

8
tests/positive/MiniC/MultiModules/Data/Nat.juvix
View File

@ -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;

2
tests/positive/MiniC/MultiModules/Data/Pair.juvix
View File

@ -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;

8
tests/positive/MiniC/MultiModules/Input.juvix
View File

@ -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;

8
tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix
View File

@ -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;

8
tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix
View File

@ -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;

2
tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix
View File

@ -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;

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