Initial.

LocalEffect/Exception.lidr

+> module LocalEffect.Exception
+
+
+> import Effects
+> import Effect.Exception
+
+> import Nat.LTProperties
+> import BoundedNat.BoundedNat
+> import Sigma.Sigma
+> import Pairs.Operations
+
+
+> %default total
+
+> %access public export
+
+
+> ||| Parses a string for a Nat
+> parseNat : String -> { [EXCEPTION String] } Eff Nat
+> parseNat str
+>   = if all (\x => isDigit x) (unpack str)
+>     then pure (cast {to = Nat} (cast {to = Int} str))
+>     else raise "Not a Nat!"
+
+
+> ||| Parses a string for a bounded Nat
+> parseLTB : (b : Nat) -> String -> { [EXCEPTION String] } Eff (LTB b)
+> {-
+> parseLTB b str
+>   = if all (\x => isDigit x) (unpack str)
+>     then let n = cast {to = Nat} (cast {to = Int} str) in
+>          case (decLT n b) of
+>            (Yes p) => pure (MkSigma n p)
+>            (No _)  => raise "Out of bound!"
+>     else raise "Not a Nat!"
+> -}
+> parseLTB b str
+>   = if all (\x => isDigit x) (unpack str)
+>     then let m = cast {to = Nat} (cast {to = Int} str) in
+>          case (decLT m b) of
+>            (Yes p) => pure (MkSigma m p)
+>            (No _)  => raise "Out of bound!"
+>     else raise "Not a Nat!"
+
+
+> ||| Parses a string for an Int
+> parseInt : String -> { [EXCEPTION String] } Eff Int
+> parseInt str
+>   = if all (\x => isDigit x || x == '-') (unpack str)
+>     then pure (cast {to = Int} str)
+>     else raise "Not an Int!"

LocalEffect/StdIO.lidr

+> module LocalEffect.StdIO
+
+> import Effects
+> import Effect.StdIO
+> import Effect.Exception
+
+> import LocalEffect.Exception
+> import BoundedNat.BoundedNat
+> import Sigma.Sigma
+> import Pairs.Operations
+
+> -- %default total
+
+> %access public export
+
+
+> |||
+> -- %assert_total -- termination not required
+> -- getNat : { [STDIO] } Eff Nat
+> getNat : Eff Nat [STDIO]
+> getNat =
+>   do putStr (" Nat: " )
+>      case the (Either String Nat) (run (parseNat (trim !getStr))) of
+>           Left err => do putStr (err ++ "\n")
+>                          getNat
+>           Right n  => do putStr "thanks!\n"
+>                          pure n
+
+
+> |||
+> -- %assert_total -- termination not required
+> getLTB : (b : Nat) -> { [STDIO] } Eff (LTB b)
+> getLTB b =
+>   do putStr (" Nat, < " ++ cast {from = Int} (cast b) ++ ": " )
+>      case the (Either String (LTB b)) (run (parseLTB b (trim !getStr))) of
+>           Left err => do putStr (err ++ "\n")
+>                          getLTB b
+>           Right n  => do putStr "thanks!\n"
+>                          pure n