@@ -157,16 +157,27 @@ pSyntaxRule :: SyntaxInfo -> IParser Syntax
157157pSyntaxRule syn
158158 = do reserved "syntax"
159159 syms <- many1 pSynSym
160+ when (all expr syms) $ fail "No keywords in syntax rule"
161+ let ns = mapMaybe name syms
162+ when (length ns /= length (nub ns))
163+ $ fail "Repeated variable in syntax rule"
160164 lchar '='
161165 tm <- pExpr syn
162166 lchar ';'
163167 return (Rule syms tm)
168+ where
169+ expr (Expr _) = True
170+ expr _ = False
171+ name (Expr n) = Just n
172+ name _ = Nothing
164173
165174pSynSym :: IParser SSymbol
166175pSynSym = try (do lchar '['; n <- iName; lchar ']'
167176 return (Expr n))
168177 <|> do n <- iName
169178 return (Keyword n)
179+ <|> do sym <- strlit
180+ return (Symbol sym)
170181
171182pFunDecl' :: SyntaxInfo -> IParser PDecl
172183pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn
@@ -238,11 +249,14 @@ pExtensions syn rules = choice (map (pExt syn) rules)
238249pExt :: SyntaxInfo -> Syntax -> IParser PTerm
239250pExt syn (Rule ssym ptm)
240251 = do smap <- mapM pSymbol ssym
241− return (update (mapMaybe id smap) ptm) -- updated with smap
252+ let ns = mapMaybe id smap
253+ return (update ns ptm) -- updated with smap
242254 where
243255 pSymbol (Keyword n) = do reserved (show n); return Nothing
244256 pSymbol (Expr n) = do tm <- pSimpleExpr syn
245257 return $ Just (n, tm)
258+ pSymbol (Symbol s) = do symbol s
259+ return Nothing
246260 dropn n [] = []
247261 dropn n ((x,t) : xs) | n == x = xs
248262 | otherwise = (x,t):dropn n xs