add Run constructor to GrammarST

This allows a grammar with a different state type to be run
in the current input stream context.

Problematically, this causes the compiler to hang while processing `doParse`.

Author: msmorgan

libs/contrib/Text/Parser/Core.idr

@@ -22,18 +22,25 @@ data GrammarST : (state : Type) -> (tok : Type) -> (consumes : Bool) -> Type ->
      Fail : String -> GrammarST st tok c ty
      Commit : GrammarST st tok False ()
 
-     SeqEat : GrammarST st tok True a -> Inf (a -> GrammarST st tok c2 b) ->
+     SeqEat : GrammarST st tok True a ->
+              Inf (a -> GrammarST st tok c2 b) ->
               GrammarST st tok True b
      SeqEmpty : {c1, c2 : Bool} ->
-                GrammarST st tok c1 a -> (a -> GrammarST st tok c2 b) ->
+                GrammarST st tok c1 a ->
+                (a -> GrammarST st tok c2 b) ->
                 GrammarST st tok (c1 || c2) b
      Alt : {c1, c2 : Bool} ->
-           GrammarST st tok c1 ty -> GrammarST st tok c2 ty ->
+           GrammarST st tok c1 ty ->
+           GrammarST st tok c2 ty ->
            GrammarST st tok (c1 && c2) ty
 
      Get : GrammarST st tok False st
      Put : st -> GrammarST st tok False ()
 
+     Run : GrammarST inner tok c a ->
+           (init : inner) ->
+           GrammarST outer tok c (a, inner)
+
 
 public export
 Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type
@@ -87,10 +94,22 @@ Functor (GrammarST st tok c) where
       = SeqEat act (\val => map f (next val))
   map f (SeqEmpty act next)
       = SeqEmpty act (\val => map f (next val))
-  -- The remaining constructors (NextIs, EOF, Commit, Get, Put) have a fixed type,
+  -- The remaining constructors (NextIs, EOF, Commit, Get, Put, Run) have a fixed type,
   -- so a sequence must be used.
+  map {c = True} f p = SeqEmpty p (Empty . f)
   map {c = False} f p = SeqEmpty p (Empty . f)
 
+export
+run : GrammarST inner tok c a ->
+      inner ->
+      GrammarST outer tok c (a, inner)
+run = Run
+
+export
+lift : Grammar tok c a ->
+       GrammarST st tok c a
+lift g = map fst $ Run g ()
+
 ||| Sequence a grammar with value type `a -> b` and a grammar
 ||| with value type `a`. If both succeed, apply the function
 ||| from the first grammar to the value from the second grammar.
@@ -132,6 +151,7 @@ mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (ne
 mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
 mapToken f Get = Get
 mapToken f (Put x) = Put x
+mapToken f (Run sub init) = Run (mapToken f sub) init
 
 ||| Always succeed with the given value.
 export
@@ -219,11 +239,20 @@ shorter : (more : List tok) -> .(ys : List tok) ->
 shorter more [] = lteRefl
 shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
 
+upgradeRes : {c : Bool} -> {xs : List tok} ->
+             outerST ->
+             ParseResult innerST xs c ty ->
+             ParseResult outerST xs c (ty, innerST)
+upgradeRes state (Failure inner com msg xs) = Failure state com msg xs
+upgradeRes state (EmptyRes inner com val xs) = EmptyRes state com (val, inner) xs
+upgradeRes state (NonEmptyRes inner com val xs) = NonEmptyRes state com (val, inner) xs
+
 doParse : {c : Bool} ->
           (state : st) ->
           (commit : Bool) -> (xs : List tok) -> (act : GrammarST st tok c ty) ->
           ParseResult st xs c ty
 doParse state com xs act with (sizeAccessible xs)
+  doParse state com xs (Run sub init) | sml = upgradeRes state (doParse init com xs sub | sml)
   doParse state com xs Get | sml = EmptyRes state com state xs
   doParse state com xs (Put newState) | sml = EmptyRes newState com () xs
   doParse state com xs (Empty val) | sml = EmptyRes state com val xs