{- A parser for a subset of formulas not containing | (or)
   It is composed of two phases:
   1. The scanner or tokenizer parses a string into a list of tokens.
   2. The actual parser parses a token list into a formula.
   Both phases are defined by parser combinators.
-}

module FormParser2 (formSP) where

import Data.Char
import Form
import Parser

-- The tokens of the syntax for formulas
data Token = AndT | NotT | LPT | RPT | TT | FT | IdT String
             deriving (Eq,Show)

-- The 'scanner' or 'tokenizer'
formS :: Parser Char [Token]
formS = list (spaces *** formS' >>> snd) *** spaces >>> fst
  where
  spaces = list (item ' ')
  formS' =
    item '&' >>> const AndT |||
    item '~' >>> const NotT |||
    item '(' >>> const LPT |||
    item ')' >>> const RPT |||
    item 'T' >>> const TT |||
    item 'F' >>> const FT |||
    identifier >>> IdT

-- The actual parsers

formP :: Parser Token Form
formP  =
  form1P *** optional (item AndT *** formP >>> snd) >>> andF
  where andF(f1, Just f2) = f1 :&: f2
        andF(f1, Nothing) = f1

-- form1P does not allow &
form1P :: Parser Token Form
form1P  =
  item NotT *** form1P >>> (Not . snd) |||
  item TT >>> const T |||
  item FT >>> const F |||
  one isIdT >>> var |||
  enclose LPT RPT formP
    where
    var(IdT s) = Var s

    isIdT(IdT _) = True
    isIdT _ = False

-- Composing scanner and parser
formSP :: String -> Maybe (Form, [Token])
formSP s = case formS s of
             Just(ss,[]) -> formP ss
             _ -> Nothing

test = formSP " (x1 & ~ T)& ~a &~ ( (  F  & d2)&~d2&d1 ) "