89d0f5d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #557 from ahmadsalim/feature/fixindent

89d0f5dEdwin Brady13 years ago

src/Idris/ParseExpr.hs+17−17

compare with master

unifiedsplit

@@ -976,49 +976,49 @@ TacticSeq ::=

976-}

977

978tactic :: SyntaxInfo -> IdrisParser PTactic

979−tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')

979+tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')

980 return $ Intro ns

981 <|> do reserved "intros"; return Intros

982− <|> try (do reserved "refine"; n <- name

982+ <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> name)

983 imps <- some imp

984 return $ Refine n imps)

985− <|> do reserved "refine"; n <- name

985+ <|> do reserved "refine"; n <- (indentPropHolds gtProp *> name)

986 i <- get

987 return $ Refine n []

988− <|> do reserved "mrefine"; n <- name

988+ <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> name)

989 i <- get

990 return $ MatchRefine n

991− <|> do reserved "rewrite"; t <- expr syn;

991+ <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);

992 i <- get

993 return $ Rewrite (desugar syn i t)

994− <|> do reserved "equiv"; t <- expr syn;

994+ <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);

995 i <- get

996 return $ Equiv (desugar syn i t)

997− <|> try (do reserved "let"; n <- name; lchar ':';

997+ <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar ':');

998− ty <- expr' syn; lchar '='; t <- expr syn;

998+ ty <- (indentPropHolds gtProp *> expr' syn); (indentPropHolds gtProp *> lchar '='); t <- (indentPropHolds gtProp *> expr syn);

999 i <- get

1000 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))

1001− <|> try (do reserved "let"; n <- name; lchar '=';

1001+ <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar '=');

1002− t <- expr syn;

1002+ t <- (indentPropHolds gtProp *> expr syn);

1003 i <- get

1004 return $ LetTac n (desugar syn i t))

1005− <|> do reserved "focus"; n <- name

1005+ <|> do reserved "focus"; n <- (indentPropHolds gtProp *> name)

1006 return $ Focus n

1007− <|> do reserved "exact"; t <- expr syn;

1007+ <|> do reserved "exact"; t <- (indentPropHolds gtProp *> expr syn);

1008 i <- get

1009 return $ Exact (desugar syn i t)

1010− <|> do reserved "applyTactic"; t <- expr syn;

1010+ <|> do reserved "applyTactic"; t <- (indentPropHolds gtProp *> expr syn);

1011 i <- get

1012 return $ ApplyTactic (desugar syn i t)

1013− <|> do reserved "reflect"; t <- expr syn;

1013+ <|> do reserved "reflect"; t <- (indentPropHolds gtProp *> expr syn);

1014 i <- get

1015 return $ Reflect (desugar syn i t)

1016− <|> do reserved "fill"; t <- expr syn;

1016+ <|> do reserved "fill"; t <- (indentPropHolds gtProp *> expr syn);

1017 i <- get

1018 return $ Fill (desugar syn i t)

1019− <|> do reserved "try"; t <- tactic syn;

1019+ <|> do reserved "try"; t <- (indentPropHolds gtProp *> tactic syn);

1020 lchar '|';

1021− t1 <- tactic syn

1021+ t1 <- (indentPropHolds gtProp *> tactic syn)

1022 return $ Try t t1

1023 <|> do lchar '{'

1024 t <- tactic syn;

src/Idris/ParseHelpers.hs+32

@@ -403,6 +403,38 @@ notEndBlock = do ist <- get

403 when (i < lvl || isParen) (fail "end of block")

404 _ -> return ()

405

406+-- | Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails

407+data IndentProperty = IndentProperty (Int -> Int -> Bool) String

408+

409+-- | Allows comparison of indent, and fails if property doesn't hold

410+indentPropHolds :: IndentProperty -> IdrisParser()

411+indentPropHolds (IndentProperty op msg) = do

412+ li <- lastIndent

413+ i <- indent

414+ when (not $ op i li) $ fail ("Wrong indention: " ++ msg)

415+

416+-- | Greater-than indent property

417+gtProp :: IndentProperty

418+gtProp = IndentProperty (>) "should be greater than context indentation"

419+

420+-- | Greater-than or equal to indent property

421+gteProp :: IndentProperty

422+gteProp = IndentProperty (>=) "should be greater than or equal context indentation"

423+

424+-- | Equal indent property

425+eqProp :: IndentProperty

426+eqProp = IndentProperty (==) "should be equal to context indentation"

427+

428+-- | Less-than indent property

429+ltProp :: IndentProperty

430+ltProp = IndentProperty (<) "should be less than context indentation"

431+

432+-- | Less-than or equal to indent property

433+lteProp :: IndentProperty

434+lteProp = IndentProperty (<=) "should be less than or equal to context indentation"

435+

436+

437+-- | Checks that there are no braces that are not closed

406notOpenBraces :: IdrisParser ()

438notOpenBraces :: IdrisParser ()

407notOpenBraces = do ist <- get

439notOpenBraces = do ist <- get

408 when (hasNothing $ brace_stack ist) $ fail "end of input"

440 when (hasNothing $ brace_stack ist) $ fail "end of input"