module DDC.Core.Parser.Witness
( pWitness
, pWitnessApp
, pWitnessAtom)
where
import DDC.Core.Parser.Type
import DDC.Core.Parser.Context
import DDC.Core.Parser.Base
import DDC.Core.Lexer.Tokens
import DDC.Core.Exp
import DDC.Base.Parser ((<?>), SourcePos)
import qualified DDC.Base.Parser as P
import qualified DDC.Type.Compounds as T
import Control.Monad
pWitness
:: Ord n
=> Context -> Parser n (Witness SourcePos n)
pWitness c = pWitnessJoin c
pWitnessJoin
:: Ord n
=> Context -> Parser n (Witness SourcePos n)
pWitnessJoin c
= do w1 <- pWitnessApp c
P.choice
[ do sp <- pTokSP (KOp "&")
w2 <- pWitnessJoin c
return (WJoin sp w1 w2)
, do return w1 ]
pWitnessApp
:: Ord n
=> Context -> Parser n (Witness SourcePos n)
pWitnessApp c
= do (x:xs) <- P.many1 (pWitnessArgSP c)
let x' = fst x
let sp = snd x
let xs' = map fst xs
return $ foldl (WApp sp) x' xs'
<?> "a witness expression or application"
pWitnessArgSP
:: Ord n
=> Context -> Parser n (Witness SourcePos n, SourcePos)
pWitnessArgSP c
= P.choice
[
do sp <- pTokSP KSquareBra
t <- pType c
pTok KSquareKet
return (WType sp t, sp)
, do pWitnessAtomSP c ]
pWitnessAtom
:: Ord n
=> Context -> Parser n (Witness SourcePos n)
pWitnessAtom c
= liftM fst (pWitnessAtomSP c)
pWitnessAtomSP
:: Ord n
=> Context -> Parser n (Witness SourcePos n, SourcePos)
pWitnessAtomSP c
= P.choice
[ do sp <- pTokSP KRoundBra
w <- pWitness c
pTok KRoundKet
return (w, sp)
, do (con, sp) <- pConSP
return (WCon sp (WiConBound (UName con) (T.tBot T.kWitness)), sp)
, do (wb, sp) <- pWbConSP
return (WCon sp (WiConBuiltin wb), sp)
, do (i, sp) <- pIndexSP
return (WVar sp (UIx i), sp)
, do (var, sp) <- pVarSP
return (WVar sp (UName var), sp) ]
<?> "a witness"