git.iko.soy/Idris-dev
on master help sign in
Addition of indentation property support.
ea39754Ahmad Salim Al-Sibahi
src/Idris/ParseExpr.hs+17−17
compare with master
unifiedsplit
@@ -976,49 +976,49 @@ TacticSeq ::=
976-}
976-}
977
977
978tactic :: SyntaxInfo -> IdrisParser PTactic
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
980 return $ Intro ns
981 <|> do reserved "intros"; return Intros
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
983 imps <- some imp
984 return $ Refine n imps)
984 return $ Refine n imps)
985− <|> do reserved "refine"; n <- name
985+ <|> do reserved "refine"; n <- (indentPropHolds gtProp *> name)
986 i <- get
986 i <- get
987 return $ Refine n []
987 return $ Refine n []
988− <|> do reserved "mrefine"; n <- name
988+ <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> name)
989 i <- get
989 i <- get
990 return $ MatchRefine n
990 return $ MatchRefine n
991− <|> do reserved "rewrite"; t <- expr syn;
991+ <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
992 i <- get
992 i <- get
993 return $ Rewrite (desugar syn i t)
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
995 i <- get
996 return $ Equiv (desugar syn i t)
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
999 i <- get
1000 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
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
1003 i <- get
1004 return $ LetTac n (desugar syn i t))
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
1006 return $ Focus n
1007− <|> do reserved "exact"; t <- expr syn;
1007+ <|> do reserved "exact"; t <- (indentPropHolds gtProp *> expr syn);
1008 i <- get
1008 i <- get
1009 return $ Exact (desugar syn i t)
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
1011 i <- get
1012 return $ ApplyTactic (desugar syn i t)
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
1014 i <- get
1015 return $ Reflect (desugar syn i t)
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
1017 i <- get
1018 return $ Fill (desugar syn i t)
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 '|';
1020 lchar '|';
1021− t1 <- tactic syn
1021+ t1 <- (indentPropHolds gtProp *> tactic syn)
1022 return $ Try t t1
1022 return $ Try t t1
1023 <|> do lchar '{'
1023 <|> do lchar '{'
1024 t <- tactic syn;
1024 t <- tactic syn;
src/Idris/ParseHelpers.hs+32
@@ -397,6 +397,38 @@ notEndBlock = do ist <- get
397 when (i < lvl || isParen) (fail "end of block")
397 when (i < lvl || isParen) (fail "end of block")
398 _ -> return ()
398 _ -> return ()
399
399
400+-- | Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails
401+data IndentProperty = IndentProperty (Int -> Int -> Bool) String
402+
403+-- | Allows comparison of indent, and fails if property doesn't hold
404+indentPropHolds :: IndentProperty -> IdrisParser()
405+indentPropHolds (IndentProperty op msg) = do
406+ li <- lastIndent
407+ i <- indent
408+ when (not $ op i li) $ fail ("Wrong indention: " ++ msg)
409+
410+-- | Greater-than indent property
411+gtProp :: IndentProperty
412+gtProp = IndentProperty (>) "should be greater than context indentation"
413+
414+-- | Greater-than or equal to indent property
415+gteProp :: IndentProperty
416+gteProp = IndentProperty (>=) "should be greater than or equal context indentation"
417+
418+-- | Equal indent property
419+eqProp :: IndentProperty
420+eqProp = IndentProperty (==) "should be equal to context indentation"
421+
422+-- | Less-than indent property
423+ltProp :: IndentProperty
424+ltProp = IndentProperty (<) "should be less than context indentation"
425+
426+-- | Less-than or equal to indent property
427+lteProp :: IndentProperty
428+lteProp = IndentProperty (<=) "should be less than or equal to context indentation"
429+
430+
431+-- | Checks that there are no braces that are not closed
400notOpenBraces :: IdrisParser ()
432notOpenBraces :: IdrisParser ()
401notOpenBraces = do ist <- get
433notOpenBraces = do ist <- get
402 when (hasNothing $ brace_stack ist) $ fail "end of input"
434 when (hasNothing $ brace_stack ist) $ fail "end of input"