GrParsec.gr

module GrParsec where

import List

-- # A mini parsec like library for Granule

-- ## Parser monad
-- Defines a type like `StateT []` from Haskell
data Parser a = Parser (String -> List (a, String))

runParser : forall {a : Type} . Parser a -> (String -> List (a, String))
runParser (Parser p) = p

-- List concat (used in the monad definition below)
concat : forall {a : Type} . List (List a) -> List a
concat Empty = Empty;
concat (Next xs xss) = append_list xs (concat xss)

-- Monadic bind for the Parser monad
andThen : forall {a : Type, b : Type} .
          Parser a -> (a -> Parser b) [] -> Parser b
andThen (Parser p) [f] = Parser (\s ->
 concat (lmap [\(a, s') -> let Parser p' = f a in p' s'] (p s)))

return : forall {a : Type} . a -> Parser a
return x = Parser (\s -> Next (x, s) Empty)

-- ## Combinators

-- Choice between two parsers (not the second may not get used)
alt : forall {a : Type} . Parser a -> (Parser a) [0..1] -> Parser a
alt p1 [p2] = Parser (\s -> let [s'] : String [] = moveString s in
  case runParser p1 s' of
    Empty -> runParser p2 s';
    x      -> x)

-- Apply a repeatable parser many times (note the result of the
-- parameter parser must be something that can be used arbitrarily)
many : forall {a : Type} . (Parser (a [])) [] -> Parser (List a)
many [p] = alt (many1 [p]) [return Empty]

-- Apply a repeatable parser one or more times
many1 : forall {a : Type} . (Parser (a [])) [] -> Parser (List a)
many1 [p] =
  p `andThen` [\x ->
    let [x'] : (a []) = x
    in  many [p] `andThen` [\xs -> return (Next x' xs)]]

-- Makes a character parser into one whose results are unrestricted
mkMoveable : Parser Char -> Parser (Char [])
mkMoveable p = p `andThen` [\x -> return (moveChar x)]

-- ## Simple primitive parsers

-- Parses any character
anyChar : Parser Char
anyChar =
  Parser (\s ->
    case stringUncons s of
      None           -> Empty;
      Some (c, rest) -> Next (c, rest) Empty)

-- Parses a particular character
char : Char [0..2] -> Parser Char
char [c] =
 Parser (\s ->
  case stringUncons s of
   None -> Empty;
   Some (c', rest) ->
     if charToInt c == charToInt c'
      then Next (c, rest) Empty
      else let () = drop @String rest in Empty)