Tweaks

StdLib/Char.gr

@@ -1,14 +1,30 @@
-import Bool
+import Either
 
-isDigit : Char -> (Char, Bool)
-isDigit '0' = ('0', True);
-isDigit '1' = ('1', True);
-isDigit '2' = ('2', True);
-isDigit '3' = ('3', True);
-isDigit '4' = ('4', True);
-isDigit '5' = ('5', True);
-isDigit '6' = ('6', True);
-isDigit '7' = ('7', True);
-isDigit '8' = ('8', True);
-isDigit '9' = ('9', True);
-isDigit c = (c, False)
+digitToInt : Char -> Either Char Int
+digitToInt c = case charToInt c - 48 of
+  0 -> Right 0;
+  1 -> Right 1;
+  2 -> Right 2;
+  3 -> Right 3;
+  4 -> Right 4;
+  5 -> Right 5;
+  6 -> Right 6;
+  7 -> Right 7;
+  8 -> Right 8;
+  9 -> Right 9;
+  c -> Left c
+
+
+-- Don't have Char literal patterns
+-- digitToInt : Char -> Maybe Int
+-- digitToInt '0' = Some 0;
+-- digitToInt '1' = Some 1;
+-- digitToInt '2' = Some 2;
+-- digitToInt '3' = Some 3;
+-- digitToInt '4' = Some 4;
+-- digitToInt '5' = Some 5;
+-- digitToInt '6' = Some 6;
+-- digitToInt '7' = Some 7;
+-- digitToInt '8' = Some 8;
+-- digitToInt '9' = Some 9;
+-- digitToInt c = None;

work-in-progress/Parse.gr

@@ -0,0 +1,38 @@
+import Char
+import Maybe
+
+-- takeWhile : (a -> (Bool, a)) -> VecX a -> (VecX a, VecX a)
+
+parseInt : String -> (Maybe Int, String)
+parseInt str = case stringUnsnoc str of
+  None -> (None, ""); -- fail on empty string
+  Some (init,c) -> parseIntInner (stringSnoc init c)
+
+parseIntInner : String -> (Maybe Int, String)
+parseIntInner str = case stringUnsnoc str of
+  None -> (0, "");
+  Some (str,c) -> case digitToInt c of
+    Left c -> (None, stringSnoc str c);
+    Right n -> case parseIntInner str of
+
+
+  parseIntInner init c
+
+
+  case [digitToInt [c]] of
+    [None] -> None;
+    [Some n] -> case parseInt [init] of
+      None -> None;
+      Some m -> Some (n + (m * 10))
+
+parseInt : String [0..1] -> Maybe Int
+parseInt [str] = case [stringUnsnoc str] of
+  [None] -> Some 0;
+  [Some (init,c)] -> case [digitToInt [c]] of
+    [None] -> None;
+    [Some n] -> case parseInt [init] of
+      None -> None;
+      Some m -> Some (n + (m * 10))
+
+-- main : Maybe Int
+-- main = parseInt ["123456"]

work-in-progress/State.gr

@@ -0,0 +1,55 @@
+import Prelude
+
+data State sIn sOut a = State (sIn -> a × sOut)
+
+mapState
+  : forall {a : Type, b : Type, sIn : Type, sOut : Type}
+  . (a -> b) -> State sIn sOut a -> State s b
+mapState f (State ka) = State (\s -> let (a, s) = ka s in (f a, s))
+
+pureState
+  : forall {a : Type, s : Type}
+  . a -> State s a
+pureState a = State (\s -> (a, s))
+
+amapState
+  : forall {a : Type, b : Type, s : Type}
+  . State s (a -> b) -> State s a -> State s b
+amapState (State kf) (State ka) = State
+    (\s ->
+      let (f, s) = kf s;
+          (a, s) = ka s
+      in (f a, s)
+    )
+
+joinState
+  : forall {a : Type, s : Type}
+  . State s (State s a) -> State s a
+joinState (State kka) = State (\s -> let ((State ka), s) = kka s in ka s)
+
+mmapState
+  : forall {a : Type, b : Type, s : Type}
+  . (a -> State s b) -> State s a -> State s b
+mmapState k = joinState ∘ mapState k
+
+
+-- here things get interesitng
+-- `get` duplicates the state, so the usual implementation is not well typed
+-- get
+--   : forall {s : Type}
+--   . State s s
+-- get = State (\s -> (s, s))
+
+
+-- get
+--   : forall {s : Type}
+--   . State (s [2]) s
+-- get = State (\[x] -> (x, x))
+
+get
+  : forall {s : Type}
+  . State (s [2]) s
+get = State foo
+
+foo : forall {s : Type} . s [2] -> (s, s)
+foo = \[s] -> (s, s)