Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make comma a delimiter #1525

Merged
merged 1 commit into from
Sep 12, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion examples/milestone/Collatz/Collatz.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ getInitial : ℕ;
getInitial ≔ parsePositiveInt (readline);

output : ℕ → ℕ × IO;
output n ≔ (n , putStrLn (natToStr n));
output n ≔ (n, putStrLn (natToStr n));

terminating
run : (ℕ → ℕ) → ℕ → IO;
Expand Down
6 changes: 3 additions & 3 deletions examples/milestone/TicTacToe/CLI/TicTacToe.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ getMove : Maybe ℕ;
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;
Expand All @@ -37,8 +37,8 @@ prompt x ≔ "\n" ++str (showGameState x) ++str "\nPlayer " ++str showSymbol (pl
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 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;
Expand Down
6 changes: 3 additions & 3 deletions examples/milestone/TicTacToe/Web/TicTacToe.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ 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 (a ∷ as) (b ∷ bs) ≔ (a, b) ∷ zip as bs;
zip _ _ ≔ nil;

rangeAux : ℕ → ℕ → List ℕ;
Expand Down Expand Up @@ -122,10 +122,10 @@ renderSquare row col (empty n) ≔
>> renderNumber n row col;

renderRowAux : ℕ → (ℕ × Square) → IO;
renderRowAux col (row , s) ≔ renderSquare row col s;
renderRowAux col (row, s) ≔ renderSquare row col s;

renderRow : ℕ × (List Square) → IO;
renderRow (n , xs) ≔ mapIO (renderRowAux n) (enumerate xs);
renderRow (n, xs) ≔ mapIO (renderRowAux n) (enumerate xs);

renderBoard : Board → IO;
renderBoard (board squares) ≔ mapIO renderRow (enumerate squares);
Expand Down
10 changes: 5 additions & 5 deletions examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ 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

Expand All @@ -25,20 +25,20 @@ 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);
(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 ≔
check-result
(foldl
(check-keys token verifiers)
(Int_0 , true)
(Int_0, true)
keys-changed);
end;
5 changes: 4 additions & 1 deletion src/Juvix/Parser/Lexer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,10 @@ rawIdentifier allKeywords = do

validTailChar :: Char -> Bool
validTailChar c =
isAlphaNum c || validFirstChar c
isAlphaNum c || (validFirstChar c && notElem c delimiterSymbols)

delimiterSymbols :: [Char]
delimiterSymbols = ","

reservedSymbols :: [Char]
reservedSymbols = "\";(){}[].≔λ\\"
Expand Down
10 changes: 5 additions & 5 deletions tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ from-string : String → Maybe String;
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
Expand Down Expand Up @@ -238,21 +238,21 @@ 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);
(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 ≔
check-result
(foldl
(check-keys token verifiers)
(Int_0 , true)
(Int_0, true)
keys-changed);

--------------------------------------------------------------------------------
Expand Down
22 changes: 11 additions & 11 deletions tests/positive/Internal/Implicit.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -55,7 +55,7 @@ upToTwo : _;
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;
Expand Down Expand Up @@ -96,10 +96,10 @@ f : {A : Type} → {B : Type} → A → B → _;
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;
Expand All @@ -116,7 +116,7 @@ filter f (h ∷ hs) ≔ if (f h)
(filter f hs);

partition : {A : Type} → (A → Bool) → List A → List A × List A;
partition _ nil ≔ nil , nil;
partition _ nil ≔ nil, nil;
partition f (x ∷ xs) ≔ (if (f x) first second) ((∷) x) (partition f xs);

end;
6 changes: 3 additions & 3 deletions tests/positive/MiniC/Polymorphism/Input.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -70,18 +70,18 @@ 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) = ")
>> put-str-ln (bool-to-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));
Expand Down
12 changes: 6 additions & 6 deletions tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ from-string : String → Maybe String;
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
Expand Down Expand Up @@ -278,24 +278,24 @@ check-vp verifiers key change owner ≔
(isNegative (change-from-key key))
-- make sure the spender approved the transaction
(change + (change-from-key key), elem (==String) owner verifiers)
(change + (change-from-key key), true);
(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);
(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 ≔
check-result
(foldl
(check-keys token verifiers)
(Int_0 , true)
(Int_0, true)
keys-changed);

--------------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion tests/positive/StdlibList/Data/List.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ import Data.Product;
open Data.Product;

splitAt : (a : Type) → ℕ → List a → List a;
splitAt a _ (nil _) ≔ nil a , nil 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) λ{
Expand Down