Mercurial > hg > Members > kono > Proof > galois
changeset 253:b46a3a3f45af
getArgs worked
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 13 Dec 2020 17:31:00 +0900 |
| parents | e937bf565bf8 |
| children | a5b3061f15ee |
| files | sym5n.agda |
| diffstat | 1 files changed, 32 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/sym5n.agda Sat Dec 12 21:35:49 2020 +0900 +++ b/sym5n.agda Sun Dec 13 17:31:00 2020 +0900 @@ -59,39 +59,50 @@ FListtoStr [] = "" FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x)) --- open import IO -- using (IO) +-- open import IO +-- main = run ( putStrLn $ sym5solvable 4) + +open import Codata.Musical.Notation open import Data.Maybe hiding (_>>=_) -open import Data.List -- using (IO) -open import Foreign.Haskell using (Unit) +open import Data.List +open import Data.Char +-- open import Foreign.Haskell using (Unit) open import IO.Primitive open import Codata.Musical.Costring +-- open import Agda.Builtin.IO public postulate - getArgs : IO (List String) -{-# FOREIGN GHC import qualified System.Environment #-} + getArgs : IO (List (List Char)) +{-# FOREIGN GHC import qualified System.Environment #-} {-# COMPILE GHC getArgs = System.Environment.getArgs #-} -charToDigit : String → Maybe ℕ -charToDigit "0" = just ( 0) -charToDigit "1" = just ( 1) -charToDigit "2" = just ( 2) -charToDigit "3" = just ( 3) -charToDigit "4" = just ( 4) -charToDigit "5" = just ( 5) -charToDigit "6" = just ( 6) -charToDigit "7" = just ( 7) -charToDigit "8" = just ( 8) -charToDigit "9" = just ( 9) +charToDigit : Char → Maybe ℕ +charToDigit '0' = just ( 0) +charToDigit '1' = just ( 1) +charToDigit '2' = just ( 2) +charToDigit '3' = just ( 3) +charToDigit '4' = just ( 4) +charToDigit '5' = just ( 5) +charToDigit '6' = just ( 6) +charToDigit '7' = just ( 7) +charToDigit '8' = just ( 8) +charToDigit '9' = just ( 9) charToDigit _ = nothing -getNumArg1 : (List String) → ℕ +getNumArg1 : (List (List Char)) → ℕ getNumArg1 [] = 0 -getNumArg1 (x ∷ y) with charToDigit x +getNumArg1 ([] ∷ y) = 0 +getNumArg1 ((x ∷ _) ∷ y) with charToDigit x ... | just n = n ... | nothing = 0 +--main = run do +-- ♯ putStrLn "A string" +-- ♯ putStrLn "second string" + main : IO ⊤ -main = do - x <- getArgs - putStrLn $ toCostring $ sym5solvable $ getNumArg1 x +main = getArgs >>= (λ x → putStrLn $ toCostring $ sym5solvable $ getNumArg1 x ) +-- x <- getArgs +-- ? --♯ putStrLn $ toCostring $ sym5solvable $ getNumArg1 x +