mirror of
https://github.com/anoma/juvix.git
synced 2025-01-05 22:46:08 +03:00
Make comma a delimiter (#1525)
This commit is contained in:
parent
e3dbb308d3
commit
2eb51ce1c3
@ -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;
|
||||
|
@ -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;
|
||||
@ -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;
|
||||
|
@ -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 ℕ;
|
||||
@ -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);
|
||||
|
@ -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
|
||||
|
||||
@ -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;
|
||||
|
@ -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 = "\";(){}[].≔λ\\"
|
||||
|
@ -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
|
||||
@ -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);
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
@ -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;
|
||||
@ -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;
|
||||
@ -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;
|
||||
@ -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;
|
||||
|
@ -70,10 +70,10 @@ 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
|
||||
@ -81,7 +81,7 @@ id' a ≔ fst (a , a);
|
||||
|
||||
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));
|
||||
|
@ -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
|
||||
@ -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);
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
@ -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) λ{
|
||||
|
Loading…
Reference in New Issue
Block a user