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

git.iko.soy/Idris-dev

Distinguish term syntax and pattern syntax

commit4a1324c24e382515fe053659fdb0c35b2d93bb87 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 15 Nov 2011, 16:34 (15 years ago) parent31d974b

2 files changed+21−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−2 src/Idris/Parser.hs+15−8

src/Idris/AbsSyntax.hs+6−2

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

362362 dsl_return :: Name }

363363 deriving Show

364364

365−data Syntax = Rule [SSymbol] PTerm

365+data SynContext = PatternSyntax | TermSyntax | AnySyntax

366+ deriving Show

367+

368+data Syntax = Rule [SSymbol] PTerm SynContext

366369 deriving Show

367370

368371data SSymbol = Keyword Name

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

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

377380 no_imp :: [Name],

378381 decoration :: Name -> Name,

382+ inPattern :: Bool,

379383 dsl_info :: DSL }

380384 deriving Show

381385

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

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

383387

384388--- Pretty printing declarations and terms

385389

src/Idris/Parser.hs+15−8

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

201201 fc <- pfc

202202 return (PSyntax fc s)

203203 where

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

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

205205 ename (Keyword n) = Just n

206206 ename _ = Nothing

207207

208208pSyntaxRule :: SyntaxInfo -> IParser Syntax

209209pSyntaxRule syn

210− = do reserved "syntax"

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

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

212+ reserved "syntax"

211213 syms <- many1 pSynSym

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

213215 let ns = mapMaybe name syms

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

216218 lchar '='

217219 tm <- pExpr syn

218220 lchar ';'

219− return (Rule syms tm)

221+ return (Rule syms tm sty)

220222 where

221223 expr (Expr _) = True

222224 expr _ = False

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

331333

332334pSimpleExtExpr :: SyntaxInfo -> IParser PTerm

333335pSimpleExtExpr syn = do i <- getState

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

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

335337 where

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

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

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

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

338340 Keyword _ -> True

339341 Symbol _ -> True

340342 _ -> False

341343 simple _ = False

342344

345+ valid (Rule _ _ AnySyntax) = True

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

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

348+

343349pNoExtExpr syn =

344350 try (pApp syn)

345351 <|> pSimpleExpr syn

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

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

353359

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

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

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

356362 = do s1 <- pSymbol pSimpleExpr s

357363 smap <- mapM (pSymbol pExpr') ssym

358364 let ns = mapMaybe id (s1:smap)

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

616622 no_imp = nub (ni ++ ns) }

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

618624

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

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

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

620627

621628pClause :: SyntaxInfo -> IParser PClause

622629pClause syn