94d888b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parsing and elaboration of alternatives

commit94d888ba61bd99cafec8d8cd8d281bd200cd169b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 25 Nov 2011, 17:53 (15 years ago) parentada02de

4 files changed+29−13

compare with master

unifiedsplit

src/Core/Elaborate.hs+16−11 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabTerm.hs+2 src/Idris/Parser.hs+10−1

src/Core/Elaborate.hs+16−11

@@ -351,18 +351,23 @@ try t1 t2 = do s <- get

351351 _ -> do put s; t2

352352

353353-- Try a selection of tactics. Exactly one must work, all others must fail

354−tryAll :: [Elab a] -> Elab a

355−tryAll xs = tryAll' 0 (fail "Nothing to try") xs

354+tryAll :: [(Elab a, String)] -> Elab a

355+tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

356356 where

357− tryAll' :: Int -> Elab a -> [Elab a] -> Elab a

358− tryAll' 1 res [] = res

359− tryAll' _ res [] = fail "Couldn't resolve alternative"

360− tryAll' c res (x:xs) = do s <- get

361− case runStateT x s of

362− OK (v, s') -> tryAll' (c+1) (do put s'

363− return v) xs

364− _ -> do put s

365− tryAll' c res xs

357+ tryAll' :: [Elab a] -> -- successes

358+ Elab a -> -- last failure

359+ [Elab a] -> -- still to try

360+ Elab a

361+ tryAll' [res] _ [] = res

362+ tryAll' (_:_) _ [] = fail $ "Couldn't resolve alternative: "

363+ ++ showSep ", " (map snd xs)

364+ tryAll' [] f [] = f

365+ tryAll' cs f (x:xs) = do s <- get

366+ case runStateT x s of

367+ OK (v, s') -> tryAll' ((do put s'

368+ return v):cs) f xs

369+ Error err -> do put s

370+ tryAll' cs (lift (tfail err)) xs

366371

367372

368373

src/Idris/AbsSyntax.hs+1−1

@@ -520,7 +520,7 @@ showImp impl tm = se 10 tm where

520520 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

521521 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

522522 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

523− se p (PAlternative as) = "(" ++ showSep " ||| " (map (se 10) as) ++ ")"

523+ se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"

524524 se p PSet = "Set"

525525 se p (PConstant c) = show c

526526 se p (PProof ts) = "proof { " ++ show ts ++ "}"

src/Idris/ElabTerm.hs+2

@@ -96,6 +96,8 @@ elab ist info pattern tm

9696 [pimp (MN 0 "a") t,

9797 pimp (MN 0 "P") Placeholder,

9898 pexp l, pexp r])

99+ elab' (PAlternative as) = tryAll (zip (map elab' as) (map show as))

100+

99101 elab' (PRef fc n) | pattern && not (inparamBlock n)

100102 = do ctxt <- get_context

101103 let sc = case lookupTy n ctxt of

src/Idris/Parser.hs+10−1

@@ -339,6 +339,8 @@ pSimpleExtExpr syn = do i <- getState

339339 pExtensions syn (filter simple (syntax_rules i))

340340 where

341341 simple (Rule (Expr x:xs) _ _) = False

342+ simple (Rule [Keyword _] _ _) = True

343+ simple (Rule [Symbol _] _ _) = True

342344 simple (Rule (_:xs) _ _) = case (last xs) of

343345 Keyword _ -> True

344346 Symbol _ -> True

@@ -387,6 +389,7 @@ pExt syn (Rule (s:ssym) ptm _)

387389 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

388390 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

389391 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

392+ update ns (PAlternative as) = PAlternative (map (update ns) as)

390393 update ns (PHidden t) = PHidden (update ns t)

391394 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

392395 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

@@ -421,6 +424,7 @@ pSimpleExpr syn =

421424 return (PTactics ts)

422425 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

423426 <|> try (pPair syn)

427+ <|> try (pAlt syn)

424428 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

425429 <|> try (do c <- pConstant; fc <- pfc

426430 return (modifyConst syn fc (PConstant c)))

@@ -448,7 +452,11 @@ pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp

448452 where

449453 pairOp = do lchar ','; return PPair

450454 <|> do reservedOp "**"; return (\f x y -> PDPair f x Placeholder y)

451−

455+

456+pAlt syn = do symbol "(|";

457+ alts <- sepBy1 (pExpr' syn) (lchar ',')

458+ symbol "|)"

459+ return (PAlternative alts)

452460

453461pHSimpleExpr syn

454462 = do lchar '.'

@@ -792,6 +800,7 @@ expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

792800expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

793801expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

794802 (expandDo dsl r)

803+expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)

795804expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

796805expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)

797806expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds