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

git.iko.soy/Idris-dev

on master help sign in

Parsing and elaboration of alternatives

94d888bEdwin Brady15 years ago

src/Core/Elaborate.hs+16−11

compare with master

unifiedsplit

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

351 _ -> do put s; t2

352

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

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

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

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

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

356 where

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

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

358+ Elab a -> -- last failure

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

360+ Elab a

358− tryAll' 1 res [] = res

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

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

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

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

364+ tryAll' [] f [] = f

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

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

361− case runStateT x s of

366+ case runStateT x s of

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

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

363− return v) xs

368+ return v):cs) f xs

364− _ -> do put s

369+ Error err -> do put s

365− tryAll' c res xs

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

366

371

367

372

368

373

src/Idris/AbsSyntax.hs+1−1

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

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

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

522 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) ++ "|)"

524 se p PSet = "Set"

525 se p (PConstant c) = show c

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

src/Idris/ElabTerm.hs+2

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

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

97 pimp (MN 0 "P") Placeholder,

98 pexp l, pexp r])

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

100+

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

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

100 = do ctxt <- get_context

102 = do ctxt <- get_context

101 let sc = case lookupTy n ctxt of

103 let sc = case lookupTy n ctxt of

src/Idris/Parser.hs+10−1

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

339 pExtensions syn (filter simple (syntax_rules i))

340 where

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

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

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

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

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

343 Keyword _ -> True

345 Keyword _ -> True

344 Symbol _ -> True

346 Symbol _ -> True

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

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

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

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

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

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

391 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)

390 update ns (PHidden t) = PHidden (update ns t)

393 update ns (PHidden t) = PHidden (update ns t)

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

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

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

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

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

421 return (PTactics ts)

424 return (PTactics ts)

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

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

423 <|> try (pPair syn)

426 <|> try (pPair syn)

427+ <|> try (pAlt syn)

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

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

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

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

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

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

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

448 where

452 where

449 pairOp = do lchar ','; return PPair

453 pairOp = do lchar ','; return PPair

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

454 <|> 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)

452

460

453pHSimpleExpr syn

461pHSimpleExpr syn

454 = do lchar '.'

462 = do lchar '.'

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

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

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

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

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

794 (expandDo dsl r)

802 (expandDo dsl r)

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

795expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

804expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

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

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

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

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