module DDC.Core.Parser.Witness
( pWitness
, pWitnessApp
, pWitnessAtom)
where
import DDC.Core.Parser.Type
import DDC.Core.Parser.Base
import DDC.Core.Lexer.Tokens
import DDC.Core.Exp
import DDC.Base.Parser ((<?>))
import qualified DDC.Base.Parser as P
import qualified DDC.Type.Compounds as T
pWitness :: Ord n => Parser n (Witness n)
pWitness = pWitnessJoin
pWitnessJoin :: Ord n => Parser n (Witness n)
pWitnessJoin
= do w1 <- pWitnessApp
P.choice
[ do pTok KAmpersand
w2 <- pWitnessJoin
return (WJoin w1 w2)
, do return w1 ]
pWitnessApp :: Ord n => Parser n (Witness n)
pWitnessApp
= do (x:xs) <- P.many1 pWitnessArg
return $ foldl WApp x xs
<?> "a witness expression or application"
pWitnessArg :: Ord n => Parser n (Witness n)
pWitnessArg
= P.choice
[
do pTok KSquareBra
t <- pType
pTok KSquareKet
return $ WType t
, do pWitnessAtom ]
pWitnessAtom :: Ord n => Parser n (Witness n)
pWitnessAtom
= P.choice
[ do pTok KRoundBra
w <- pWitness
pTok KRoundKet
return $ w
, do con <- pCon
return $ WCon (WiConBound (UName con) (T.tBot T.kWitness))
, do wb <- pWbCon
return $ WCon (WiConBuiltin wb)
, do i <- pIndex
return $ WVar (UIx i)
, do var <- pVar
return $ WVar (UName var) ]
<?> "a witness"