From 4a15816e6dc9fb6c48c7d83122ab57eb5a670efe Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Sat, 23 Dec 2017 14:49:31 -0600
Subject: [PATCH] WIP StateT operations for Grammar

---
 libs/contrib/Text/Parser/Core.idr  |  2 +-
 libs/contrib/Text/Parser/State.idr | 68 ++++++++++++++++++++++++++++++
 libs/contrib/contrib.ipkg          |  1 +
 3 files changed, 70 insertions(+), 1 deletion(-)
 create mode 100644 libs/contrib/Text/Parser/State.idr

diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr
index cba92dfd8e..20ec2c35d1 100644
--- a/libs/contrib/Text/Parser/Core.idr
+++ b/libs/contrib/Text/Parser/Core.idr
@@ -88,7 +88,7 @@ Functor (Grammar tok c) where
 ||| from the first grammar to the value from the second grammar.
 ||| Guaranteed to consume if either grammar consumes.
 export
-(<*>) : Grammar tok c1 (a -> b) ->
+(<*>) : Grammar tok c1 (inf c1 (a -> b)) ->
         Grammar tok c2 a ->
         Grammar tok (c1 || c2) b
 (<*>) x y = SeqEmpty x (\f => map f y)
diff --git a/libs/contrib/Text/Parser/State.idr b/libs/contrib/Text/Parser/State.idr
new file mode 100644
index 0000000000..a8e6a20cd4
--- /dev/null
+++ b/libs/contrib/Text/Parser/State.idr
@@ -0,0 +1,68 @@
+module Text.Parser.Stateful
+
+import Control.Monad.State
+import Control.ST
+import Text.Parser
+
+import public Control.Delayed
+
+%access public export
+%default total
+
+get : StateT stateType (Grammar tok False) stateType
+get = ST (\x => pure (x, x))
+
+put : stateType -> StateT stateType (Grammar tok False) ()
+put x = ST (\y => pure ((), x))
+
+modify : (stateType -> stateType) -> StateT stateType (Grammar tok False) ()
+modify f = ST (\x => pure ((), f x))
+
+lemma : (a, stateType) -> Inf (a -> StateT stateType (Grammar tok c2) b) -> Grammar tok c2 (b, stateType)
+lemma (v, st') k = let ST kv = k v in
+                       kv st'
+
+(>>=) : StateT stateType (Grammar tok c1) a ->
+        inf c1 (a -> StateT stateType (Grammar tok c2) b) ->
+        StateT stateType (Grammar tok (c1 || c2)) b
+(>>=) {c1 = False} (ST f) k = ST (\st => do (v, st') <- f st
+                                            let ST kv = k v
+                                            kv st')
+(>>=) {c1 = True} (ST f) k = ST (\st => do x <- f st
+                                           lemma x k)
+
+pure : a -> StateT stateType (Grammar tok False) a
+pure x = ST (\st => pure (x, st))
+
+
+map : (a -> b) -> StateT stateType (Grammar tok c) a ->
+                  StateT stateType (Grammar tok c) b
+map f (ST g) = ST (\st => map (mapFst f) (g st))
+  where mapFst : (a -> x) -> (a, s) -> (x, s)
+        mapFst fn (a, b) = (fn a, b)
+
+-- (>>=) {c1 = True} {c2 = True} (ST f) k = ST (\st => (f st) >>= Delay (\x => ?whatNow3))
+                                           -- kv st')
+
+
+-- gets : (stateType -> a) -> StateT stateType (Grammar tok False) a
+-- gets f = do s <- get
+--             pure (f s)
+
+
+GrammarTrans : Type -> Type -> Bool -> Type -> Type
+GrammarTrans st tok consumes result = st -> Grammar tok consumes (result, st)
+
+identity : Grammar tok True a -> GrammarTrans st tok True a
+identity g state = map (\x => (x, state)) g
+
+comma : Grammar Char True ()
+comma = terminal (\c => if c == ',' then Just () else Nothing)
+
+commaCounter : GrammarTrans Nat Char True ()
+commaCounter n = do comma
+                    commaCounter (S n) <|> pure ((), S n)
+
+countCommas : Grammar Char True Nat
+countCommas = map (\(_, n) => n) (commaCounter Z)
+
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index 849625f598..92b7f7c249 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -90,6 +90,7 @@ modules = CFFI
 
         , Text.Parser
         , Text.Parser.Core
+        , Text.Parser.State
 
         , Text.PrettyPrint.WL.Core
         , Text.PrettyPrint.WL.Combinators