getArgs 解決

やっぱり「落ち着いてやればできるだろ」と思い直して。

Data.Text.Text とか言ってるので、getArgs が Text (おそらくutf8)を返しているんだろと思ったんだが、実は、

　　grep Text MAlonzo/**/*.hs | more

したら、

　　MAlonzo/Code/Agda/Builtin/String.hs:type T6 = Data.Text.Text

とかやってて、Compiler が Agda の String を Haskell の Data.Text.Text に変換してるわけね。そうといわかれば、

　　open import Codata.Musical.Notation
　　open import Data.Maybe hiding (_>>=_)
　　open import Data.List　
　　open import Data.Char　
　　open import IO.Primitive
　　open import Codata.Musical.Costring

　　postulate
　　　　getArgs : IO (List (List Char))
　　{-# FOREIGN GHC import qualified System.Environment #-}
　　{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

　　main : IO ⊤
　　main = getArgs >>= (λ x →　putStrLn $ toCostring $ sym5solvable $ getNumArg1 x )

という感じで、 IO (List (List Char)) で受ければよいと。

Monomorphic な Agda では Monad の修飾構文はよろしくないらしく、直接、getArgs >>= (λ x → と書くのが残念な感じ。