如何解决有没有更好的方法在 Idris 中编写嵌套案例?
这是 Edwin 书中的一段 Idris 代码:
data DataStore : Type where
MkData : (size : Nat) ->
(items : Vect size String) ->
DataStore
proccessInput : DataStore -> String -> Maybe (String,DataStore)
proccessInput store@(MkData size items) input =
case map trim $ span (/= ' ') input of
("add",item) => Just ("ID " ++ show size ++ "\n",MkData _ (item :: items))
("get",val) => case all isDigit (unpack val) of
False => Just ("Invalid command\n",store)
True => case integerToFin (cast val) size of
Nothing => Just ("Out of range\n",store)
(Just id) => Just (index id items ++ " \n",store)
("quit","") => Nothing
(_,_) => Just ("Invalid command\n",store)
我已经删除了一些我认为多余的代码(一些辅助函数),但我仍然发现代码有些多余。我认为案例拆分真的很难看。
解决方法
模式匹配绑定是一种方便的符号,用于处理可能失败的操作序列,这可能有助于减少嵌套 case 块的某些最近性。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。