4a1324c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Distinguish term syntax and pattern syntax

4a1324cEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+6−2

compare with master

unifiedsplit

@@ -362,7 +362,10 @@ data DSL = DSL { dsl_bind :: Name,

362 dsl_return :: Name }

363 deriving Show

364

365+data SynContext = PatternSyntax | TermSyntax | AnySyntax

366+ deriving Show

367+

365−data Syntax = Rule [SSymbol] PTerm

368+data Syntax = Rule [SSymbol] PTerm SynContext

366 deriving Show

369 deriving Show

367

370

368data SSymbol = Keyword Name

371data SSymbol = Keyword Name

@@ -376,10 +379,11 @@ data SyntaxInfo = Syn { using :: [(Name, PTerm)],

376 syn_params :: [(Name, PTerm)],

379 syn_params :: [(Name, PTerm)],

377 no_imp :: [Name],

380 no_imp :: [Name],

378 decoration :: Name -> Name,

381 decoration :: Name -> Name,

382+ inPattern :: Bool,

379 dsl_info :: DSL }

383 dsl_info :: DSL }

380 deriving Show

384 deriving Show

381

385

382−defaultSyntax = Syn [] [] [] id initDSL

386+defaultSyntax = Syn [] [] [] id False initDSL

383

387

384--- Pretty printing declarations and terms

388--- Pretty printing declarations and terms

385

389

src/Idris/Parser.hs+15−8

@@ -201,13 +201,15 @@ pSyntaxDecl syn

201 fc <- pfc

202 return (PSyntax fc s)

203 where

204− names (Rule syms _) = mapMaybe ename syms

204+ names (Rule syms _ _) = mapMaybe ename syms

205 ename (Keyword n) = Just n

206 ename _ = Nothing

207

208pSyntaxRule :: SyntaxInfo -> IParser Syntax

209pSyntaxRule syn

210+ = do sty <- option AnySyntax (do reserved "term"; return TermSyntax

211+ <|> do reserved "pattern"; return PatternSyntax)

210− = do reserved "syntax"

212+ reserved "syntax"

211 syms <- many1 pSynSym

213 syms <- many1 pSynSym

212 when (all expr syms) $ fail "No keywords in syntax rule"

214 when (all expr syms) $ fail "No keywords in syntax rule"

213 let ns = mapMaybe name syms

215 let ns = mapMaybe name syms

@@ -216,7 +218,7 @@ pSyntaxRule syn

216 lchar '='

218 lchar '='

217 tm <- pExpr syn

219 tm <- pExpr syn

218 lchar ';'

220 lchar ';'

219− return (Rule syms tm)

221+ return (Rule syms tm sty)

220 where

222 where

221 expr (Expr _) = True

223 expr (Expr _) = True

222 expr _ = False

224 expr _ = False

@@ -331,15 +333,19 @@ pExtExpr syn = do i <- getState

331

333

332pSimpleExtExpr :: SyntaxInfo -> IParser PTerm

334pSimpleExtExpr :: SyntaxInfo -> IParser PTerm

333pSimpleExtExpr syn = do i <- getState

335pSimpleExtExpr syn = do i <- getState

334− pExtensions syn (filter simple (syntax_rules i))

336+ pExtensions syn (filter valid (filter simple (syntax_rules i)))

335 where

337 where

336− simple (Rule (Expr x:xs) _) = False

338+ simple (Rule (Expr x:xs) _ _) = False

337− simple (Rule (_:xs) _) = case (last xs) of

339+ simple (Rule (_:xs) _ _) = case (last xs) of

338 Keyword _ -> True

340 Keyword _ -> True

339 Symbol _ -> True

341 Symbol _ -> True

340 _ -> False

342 _ -> False

341 simple _ = False

343 simple _ = False

342

344

345+ valid (Rule _ _ AnySyntax) = True

346+ valid (Rule _ _ PatternSyntax) = inPattern syn

347+ valid (Rule _ _ TermSyntax) = not (inPattern syn)

348+

343pNoExtExpr syn =

349pNoExtExpr syn =

344 try (pApp syn)

350 try (pApp syn)

345 <|> pSimpleExpr syn

351 <|> pSimpleExpr syn

@@ -352,7 +358,7 @@ pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

352pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)

358pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)

353

359

354pExt :: SyntaxInfo -> Syntax -> IParser PTerm

360pExt :: SyntaxInfo -> Syntax -> IParser PTerm

355−pExt syn (Rule (s:ssym) ptm)

361+pExt syn (Rule (s:ssym) ptm _)

356 = do s1 <- pSymbol pSimpleExpr s

362 = do s1 <- pSymbol pSimpleExpr s

357 smap <- mapM (pSymbol pExpr') ssym

363 smap <- mapM (pSymbol pExpr') ssym

358 let ns = mapMaybe id (s1:smap)

364 let ns = mapMaybe id (s1:smap)

@@ -616,7 +622,8 @@ whereSyn n syn args = let ns = concatMap allNamesIn args

616 no_imp = nub (ni ++ ns) }

622 no_imp = nub (ni ++ ns) }

617 where decorate n x = UN [(show n ++ "_" ++ show x)]

623 where decorate n x = UN [(show n ++ "_" ++ show x)]

618

624

625+pArgExpr syn = let syn' = syn { inPattern = True } in

619−pArgExpr syn = try (pHSimpleExpr syn) <|> pSimpleExtExpr syn

626+ try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'

620

627

621pClause :: SyntaxInfo -> IParser PClause

628pClause :: SyntaxInfo -> IParser PClause

622pClause syn

629pClause syn