-- | Parsers for CSyntax import Data.List(nub) import Parse import BinParse import FString(getFString, StrTable) import PreStrings(fsStar, fsComma, fsRArrow, fsBRArrow,fsImpl) import Position import Error import CSyntax import Id import Lex import Literal import AgdaTrace import Monads(Error,raise) import MetaVars(preMetaVar) import PluginType (Plugin(..)) import MiscId(commaId) --import AgdaPretty -- just for debugging --import PPrint -- just for debugging infix 6 >>>> , >>>>> type CParser a = Parser [Token] a pProgram :: CParser CProgram pProgram = many pModule >>- CProgram pLetDefs = --trace "LDs" $ block (pLetDef pBindId) pModule :: CParser CModule pModule = l L_module ..+ pModId +.+ pPArgs +.+ pPackageBody >>>> CModule -- pNativeLine = l L_native ..+ string' +.. sm --pInterface :: CParser (CInterface, StrTable) --pInterface = (l L_interface ..+ l L_use ..+ sepBy pModId cm +.+ l L_in ..+ -- pSign pModId +.. sm >>> CInterface) +.+ eof pType = pExpr pExpr :: CParser CExpr pExpr = --trace "E" $ exp0 +.+ many comment >>> foldr (Ccomment False) {- pExprStart :: CParser CExpr pExprStart = --trace "S" $ exp9 +.+ many comment >>> foldr (Ccomment False) -} exp0 :: CParser CExpr exp0 = --trace "0" $ binop getFixity mkBin pOper exp10 mkBin e1 op e2 = if isRArrow op then CArrow False e1 e2 else if isBRArrow op then CArrow True e1 e2 else CBinOp e1 op e2 pB p = p `into` \ (xs,a)-> rarrow .> CArg (map ((,) False) xs) a |!! brarrow .> CArg (map ((,) True) xs) a pB' p = p `into` \ xsas -> rarrow .> (False,xsas) |!! brarrow .> (True,xsas) exp10 :: CParser CExpr exp10 = --trace "A" $ l L_lam ..+ pB' pPBind +.+ pExpr >>> (\(h,CBind xs a) e -> cLam [(h,CBind [x] a) | x<- xs] e) |!! l L_let ..+ block (pLetDef pBindId) +.+ l L_in ..+ pExpr >>> Clet |!! l L_case ..+ pExpr +.+ l L_of ..+ block pCaseArm >>> Ccase #ifdef NEWSYNTAX #else |!! l L_open ..+ pExpr +.+ pOpenArgs +.+ l L_in ..+ pExpr >>>> Copen |!! l L_data ..+ pSummands >>- CSum |!! l L_idata ..+ pIndSummands >>- (CIndSum []) #endif |!! l L_sig +.+ block (pSign pBindId) >>> CProduct |!! l L_external +.+ (many1 string') +.+ (many aexp) >>>> (\p -> \(name:opts) -> \es -> (CExternal (Plugin p name (concat opts) es ()))) -- Should only be one or two strings |!! l L_do +.+ pDoBlock >>> CDo |!! l L_if ..+ exp0 +.+ l L_then ..+ exp0 +.+ l L_else ..+ exp0 >>>> Cif ||! pB pPArgsT +.+ pExpr >>> CUniv ||! aexp +.+ many abexp >>> cApply pOpenArgs :: CParser COpenArgs pOpenArgs = l L_use ..+ pOArgs >>- COpenArgs pOArgs :: CParser [COArg] pOArgs = sepBy pOArg cm pOArg :: CParser COArg pOArg = ( many pProp +.+ pBindId ) `into` \ (ps,i) -> (eq ..+ pBindId >>- (\i' -> COArgAs ps i' i) ||! (dc ..+ pExpr) `into` (\a -> eq ..+ pBindId >>- (\i' -> COArgAsT ps i' a i) ||! succeed (COArgT ps i a)) ||! succeed (COArg ps i)) {- \ (ps,i) -> (eq ..+ pBindId >>- (\i' -> COArgAs ps i' i) ||! (dc ..+ pExpr +.+ eq ..+ pBindId >>- (\(a,i') -> COArgAsT ps i' a i)) -} -- Is this a problem? MT says that it conflicts with Ilya syntax??? abexp = l L_bar ..+ aexp >>- (\x->(True,x)) |!! aexp >>- (\x->(False,x)) aexp :: CParser CExpr aexp = --trace "a" $ aexp' +.+ many (l L_dot ..+ pBindId) >>> foldl CSelect aexp' :: CParser CExpr aexp' = --trace "a'" $ -- "'" comment +.+ aexp' >>> (Ccomment True) #ifdef NEWSYNTAX ||! pId >>- CVar #else ||! pId `into` (\ i -> l L_at ..+ l L_uscore .> (CCConS i) ||! l L_at ..+ aexp >>- CCCon i ||! succeed (CVar i)) #endif ||! lp ..+ pCmId +.. rp >>- CVar ||! lp ..+ sepBy1 pExpr cm +.. rp >>- cBinOp commaId ||! lb +.+ sepBy pExpr cm +.. rb >>> CList ||! pTYPE +.+ oNum >>>> CStar ||! l L_Type >>- cType ||! l L_Set >>- cSet ||! pMeta False ||! many pProp +.+ l L_struct +.+ block (pLetDef pBindId) >>>> CRecord ||! integer ||! string ||! char --pDoBlock :: CParser [CBind] --pDoBlock = testp "" okBlk (block pDoBind) -- where okBlk [] = False -- okBlk bs = case last bs of CBind_ _ -> True; _ -> False --pDoBind :: CParser CBind --pDoBind = pPArg +.+ l L_larrow ..+ pExpr >>> CBind -- ||! l L_let ..+ block (pLetDef pBindId) >>- CBLet -- ||! pExpr >>- CBind_ pDoBlock :: CParser [CDoBind] pDoBlock = block pDoBind pDoBind :: CParser CDoBind pDoBind = pBindId +.+ l L_larrow ..+ pExpr >>> CDoBind ||! l L_let ..+ block (pLetDef pBindId) >>- CDoLet ||! pExpr >>- CDoBind_ block :: CParser a -> CParser [a] block p = --trace "bl" $ startBlock ..+ hBlock p hBlock :: CParser a -> CParser [a] hBlock p = --trace "hB" $ lc ..+ sepBy p dsm +.. osm +.. rc block1 :: CParser a -> CParser [a] block1 p = --trace "bl1" $ startBlock ..+ hBlock p hBlock1 :: CParser a -> CParser [a] hBlock1 p = --trace "hB1" $ lc ..+ sepBy1 p dsm +.. osm +.. rc pTYPE = l L_star pCaseArm :: CParser (CPat, CExpr) pCaseArm = pAPat +.+ rarrow ..+ pExpr pSummands :: CParser [(Id, [CArg])] pSummands = sepBy pSummand (l L_bar) pSummand :: CParser (Id, [CArg]) pSummand = pBindId +.+ ( many (pPArgsBT False)) >>> (,) pSummand' :: CParser (Id, [CArg]) pSummand' = pBindId +.+ (pPArgsBT False) >>> \i -> \a -> (i,[a]) pIndSummands :: CParser CIndSummands pIndSummands = sepBy pIndSummand (l L_bar) pExplInds :: CParser CIndSummands pExplInds = sepBy pExplInd (l L_bar) pIndSummand :: CParser CIndSummand pIndSummand = pSummand `into` \ (c,cas1) -> pIndSummandTyp `into` \ es -> succeed (CIndImpl (c,cas1) (map ((,) False) es)) pExplInd :: CParser CIndSummand pExplInd = pSummand `into` \ (c,cas1) -> pExplTyp `into` \ (n,es) -> succeed (CIndExpl (c,cas1) n es) pIndSummandTyp :: CParser [CExpr] pIndSummandTyp = (l L_over ..+ block aexp ) ||! dc ..+ (l L_uscore ..+ many aexp) ||! succeed [] pExplTyp :: CParser (Id,[(Bool,CExpr)]) pExplTyp = dc ..+ pId +.+ many abexp pPackageBody :: CParser CPackageBody pPackageBody = --trace "PBd" $ eq ..+ pExpr >>- CPackageInstance ||! many pProp +.+ l L_where +.+ block (pLetDef pBindId) >>>> CPackageDef --pOpenArgs :: CParser COpenArgs --pOpenArgs pSign :: CParser Id -> CParser CSign --sepBy1 pBindId cm +.+ dc ..+ pType +.. rp >>- (\ (is, t) -> [CArg i t | i <- is]) pSign pi = pDefn pi >>- CSignDef ||! sepBy1 pi cm +.+ dc ..+ pType >>> CSign -- ||! l L_type ..+ pi +.+ many pPArg >>> CSignType pLetDef :: CParser Id -> CParser CLetDef pLetDef p = --trace "LD" $ l L_mutual ..+ block1 (pDef p) >>- CMutual ||! comment >>- CLetDefComment ||! pDef p >>- CSimple pDef :: CParser Id -> CParser CDef pDef pi = --trace "Def" $ comment >>- CDefComment |!! l L_class ..+ pPClassArg pi +.+ pClassRhs >>> (\as -> \ (export,sds) -> CDef [] (CClass as export sds)) ||! many pProp +.+ osm ..+ pDefn pi >>> CDef pProp :: CParser CProp pProp = l L_public .> Cpublic |!! l L_private .> Cprivate |!! l L_abstract .> Cabstract |!! l L_concrete .> Cconcrete pDefn :: CParser Id -> CParser CDefn pDefn pi = --trace "Defn" $ l L_data ..+ pi +.+ pPArgs +.+ pPMaybeExpr +.+ eq ..+ pSummands >>>>> Cdata |!! l L_idata ..+ pi +.+ pPArgs' +.+ dc ..+ pExpr +.+ l L_where ..+ block (pExplInd) >>>>> Cidata |!! l L_newtype ..+ pi +.+ pPArgs +.+ dc ..+ pType +.+ eq ..+ pSummand' >>>>> Cnewtype |!! l L_type ..+ pi +.+ pPArgs +.+ eq ..+ pExpr >>>> Ctype |!! l L_native ..+ pi +.+ dc ..+ pType >>> CNative |!! l L_axiom ..+ pi +.+ pPArgs +.+ dc ..+ pType >>>> CAxiom |!! l L_package ..+ pi +.+ pPArgs +.+ pPackageBody >>>> CPackage |!! l L_open ..+ pExpr +.+ pOpenArgs >>> COpen |!! l L_instance ..+ pi +.+ pPArgs +.+ dc ..+ pPInstanceArg +.+ l L_where ..+ block (pLetDef pBindId) >>>>> CInstance ||! pi +.+ pPArgs' +.+ dc ..+ pType `into` (\ (i,(as,e)) -> eq ..+ pExpr >>- CValueT i as e ||! dsm ..+ pClause1 i pi >>- CValueS i as e ) {- allows for a def like foo(n::N)::N -> N; foo x = n -} #ifdef NEWSYNTAX #else ||! pi +.+ eq ..+ pExpr >>> CValue #endif --pClauses :: Id -> CParser Id -> CParser [CClause] --pClauses i pi = many (dsm ..+ pClause i pi) --pClauses1 :: Id -> CParser Id -> CParser [CClause] --pClauses1 i pi = sepBy1 (pClause i pi) dsm pClause1 :: Id -> CParser Id -> CParser CClause pClause1 i pi = pClause i pi -- --pClauses :: Id -> CParser Id -> CParser [CClause] --pClauses i pi = pClause i pi pClause :: Id -> CParser Id -> CParser CClause pClause i pi = piEq i pi ..+ many pBAPat +.+ eq ..+ pExpr >>> CClause ||! pAPat +.+ piEq i pOper ..+ pAPat +.+ eq ..+ pExpr >>>> (\a1 -> \a2 -> \e -> CClause [(False,a1),(False,a2)] e) piEq :: Id -> CParser Id -> CParser Id piEq i pi = testp (getIdString i) (\i'->i==i') pi pPatArg :: CParser CPatArg pPatArg = lp ..+ pBindId +.+ dc ..+ pExpr +.. rp >>> CPatT ||! pBindId >>- CPatId pPatApply :: CParser CPat pPatApply = pBindId +.+ many pPatArg >>> (\i -> \l -> (CPCon i (map CPVar l))) pPatOp :: CParser CPat pPatOp = binop getFixity mkBinP (pOper |!! pCmId) pAPat where mkBinP p1 op p2 = CPCon op [p1, p2] pBAPat :: CParser (Bool, CPat) pBAPat = l L_bar ..+ pAPat >>- (\x->(True,x)) |!! pAPat >>- (\x->(False,x)) pAPat :: CParser CPat pAPat = -- pBindId `into` (\ i -> -- -- l L_at ..+ pAPat >>- CPAs (CArg i) -- succeed (CPVar (CArg i))) pPatArg >>- CPVar ||! lp ..+ pPatApply +.. rp ||! lp ..+ pPatOp +.. rp -- ||! char >>- (\ (CLit p l) -> CPLit p l) pPArgsT :: CParser ([Id],CExpr) pPArgsT = lp ..+ sepBy1 pBindId cm +.+ dc ..+ pType +.. rp pPBind :: CParser CBind pPBind = many1 pBindId >>- (\xs -> CBind xs Nothing ) ||! pPArgsT >>- (\(xs,t) -> CBind xs (Just t)) pPArgsBT :: Bool -> CParser CArg pPArgsBT def = lp ..+ sepBy1 (pBBindId def) cm +.+ dc ..+ pType +.. rp >>> CArg pPArgs :: CParser CArgs pPArgs = many (pPArgsBT False) #ifdef NEWSYNTAX pPArgs' :: CParser CArgs pPArgs' = many (pPArgsBT True) #else pPArgs' :: CParser CArgs pPArgs' = many (pPArgsBT False) #endif pPClassArg :: CParser Id -> CParser CClassArg pPClassArg pi = pi +.+ pPArgs +.+ dc ..+ pExpr `into` (\(c,(as,t)) -> l L_extends ..+ pPArgs >>- CClassArg c as t |!! succeed (CClassArg c as t [])) pClassRhs :: CParser (Bool, [CSign]) pClassRhs = l L_where ..+ block (pSign pBindId) >>- (\sds -> (False,sds)) |!! l L_exports ..+ block (pSign pBindId) >>- (\sds -> (True,sds)) pPMaybeExpr :: CParser (Maybe CExpr) pPMaybeExpr = dc ..+ pExpr >>- Just ||! succeed Nothing pPInstanceArg :: CParser CInstanceArg pPInstanceArg = pType >>- CInstanceArg --pMeta :: Bool -> CParser CExpr --pMeta b = l L_bar ..+ (pMeta' b True) -- ||! pMeta' b False pMeta :: Bool -> CParser CExpr pMeta b = l L_uscore >>- (\p -> CMeta p b (Just True) preMetaVar) ||! l L_meta >>- (\p -> CMeta p b (Just False) preMetaVar) pOper :: CParser Id pOper = pOpId ||! l L_bquote ..+ pVarId +.. l L_bquote pModId, pVarId,pConId, pBindId, pOpId, pCmId :: CParser Id pModId = lcp "" (\p x->case x of L_modid fs -> Just (mkId p fs); _ -> Nothing) pBindId = pVarId ||! lp ..+ pOpId +.. rp pBindIds = many pBindId pBBindId def = l L_bar ..+ pBindId >>- (,) True |!! l L_excl ..+ pBindId >>- (,) False |!! pBindId >>- (,) def pVarId = lcp "" (\p x->case x of L_varid fs -> Just (mkId p fs); _ -> Nothing) pOpId = lcp "" (\p x->case x of L_varsym fs -> Just (mkId p fs); _ -> Nothing) pCmId = lcp "" (\p x->case x of L_comma -> Just (mkId p fsComma); _ -> Nothing) pConId = lcp "" (\p x->case x of L_conid fs -> Just (mkId p fs); _ -> Nothing) pId :: CParser Id pId = pBindId ||! pModId -- Utilities p >>>> f = p >>- \ (x,(y,z)) -> f x y z p >>>>> f = p >>- \ (x,(y,(z,w))) -> f x y z w eq = l L_eq lp = l L_lpar rp = l L_rpar lb = l L_lsquare rb = l L_rsquare cm = l L_comma lc = l L_lcurl rc = l L_rcurl sm = l L_semi dc = l L_dcolon osm = sm ||! succeed noPosition dsm = sm +.. osm eof = lcp "" (\p x->case x of L_eof x -> Just x; _ -> Nothing) l :: LexItem -> CParser Position l li = token ( \ls-> case ls of Token p li' : ls' -> if li==li' then Right (p, ls') else Left (prLexItem li) ) getPos :: CParser Position getPos = token ( \ls-> case ls of Token p _ : _ -> Right (p, ls)) lcp :: String -> (Position -> LexItem -> Maybe a) -> CParser a lcp s f = token $ \ls-> case ls of Token p li : ls' -> case f p li of Just x -> Right (x, ls') Nothing -> Left s startBlock :: CParser () startBlock = --trace "sB" $ token $ \ ts -> case ts of t@(Token p@(Position _ _ c) li) : ts' | li /= L_lcurl -> Right ((), Token p L_lcurl : t : col c ts') _ -> Right ((), ts) where col c (t@(Token p@(Position _ _ c') _) : ts) | c' == c = Token p L_semi : t : col c ts col c (t@(Token p@(Position _ _ c') _) : ts) | c' > c = t : col c ts -- col c (t@(Token p@(Position _ _ c') (L_comment _)) : ts) | c' < c = t : col c ts col c (t@(Token p@(Position _ _ c') _) : ts) | c' < c = Token p L_rcurl : t : ts col c [] = [Token noPosition L_rcurl] -- XXX bad position errSyntax :: [String] -> [Token] -> EMsg errSyntax ss ts = case ts of Token p (L_error em) : _ -> (p, em) Token p li : _ -> (p, ESyntax (showt (prLexItem li)) (map showt (nub ss))) where showt t = case show t of "\"\\\\\"" -> "\"\\\"" s -> s oNum :: CParser (Int, Int) oNum = integer' `into` (\ n -> l L_dot ..+ integer' >>- (\m -> (n,m)) ||! succeed (n,n)) ||! succeed (0,0) comment :: CParser Comment comment = lcp "" (\p x->case x of L_comment s -> Just s; _ -> Nothing) integer' :: CParser Int integer' = lcp "" (\p x->case x of L_integer i-> Just (fromInteger i); _ -> Nothing) string' :: CParser String string' = lcp "" (\p x->case x of L_string s-> Just s; _ -> Nothing) integer = lcp "" (\p x->case x of L_integer i-> Just (CLit p (LInteger i)); _ -> Nothing) string = lcp "" (\p x->case x of L_string s-> Just (CLit p (LString s)); _ -> Nothing) char = lcp "" (\p x->case x of L_char c-> Just (CLit p (LChar c)); _ -> Nothing) rational = lcp "" (\p x->case x of L_rational c-> Just (CLit p (LRational c)); _ -> Nothing) --string' = string >>- \ (CLit _ (LString s)) -> s star = lcp "*" (\p x->case x of L_varsym fs | fs == fsStar -> Just p; _ -> Nothing) --cm = lcp "," (\p x->case x of L_varsym fs | fs == fsComma -> Just p; _ -> Nothing) rarrow = lcp "->" (\p x->case x of L_varsym fs | fs == fsRArrow -> Just p; _ -> Nothing) brarrow = lcp "|->" (\p x->case x of L_varsym fs | fs == fsBRArrow -> Just p; _ -> Nothing) rimpl = lcp "=>" (\p x->case x of L_varsym fs | fs == fsImpl -> Just p; _ -> Nothing) idP :: String -> CParser () idP str = token f where f ((Token _ (L_varid x) :ts))|getFString x==str = Right ((),ts) f _ = Left str finalP :: CParser a -> [Token] -> Error (a,StrTable) finalP p ts = chkParse (p +.+ eof ) ts {- do --traceM$"finalP:enter" tmp@(e,_) <- chkParse (p +.+ eof) ts --traceM$"finalP:exit" return tmp -} chkParse :: (CParser (a, StrTable)) -> [Token] -> Error (a, StrTable) chkParse p ts = case parse p ts of Right ((m,_):_) -> return m Left (ss,ts) -> let (Token _ (L_eof tbl)) = last ts in raise (errSyntax (filter (not . null ) ss) ts)