@@ -595,18 +595,12 @@ fnDecl' syn = checkFixity $
595595 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
596596 pushIndent
597597 (doc, argDocs) <- docstring syn
598− ist <- get
599− let initOpts = if default_total ist
600− then [TotalFn]
601− else []
602− opts <- fnOpts initOpts
603− acc <- accessibility
604− opts' <- fnOpts opts
598+ (opts, acc) <- fnOpts
605599 (n_in, nfc) <- fnName
606600 let n = expandNS syn n_in
607601 fc <- getFC
608602 lchar ':'
609− return (doc, argDocs, fc, opts', n, nfc, acc))
603+ return (doc, argDocs, fc, opts, n, nfc, acc))
610604 ty <- typeExpr (allowImp syn)
611605 terminator
612606 -- If it's a top level function, note the accessibility
@@ -634,10 +628,40 @@ fnDecl' syn = checkFixity $
634628 | otherwise = return True
635629 fixityOK _ = return True
636630
637−{-| Parses function options given initial options
631+{-| Parses a series of function and accessbility options
638632
639633@
640−FnOpts ::= 'total'
634+FnOpts ::= FnOpt* Accessibility FnOpt*
635+@
636+ -}
637+fnOpts :: IdrisParser ([FnOpt], Accessibility)
638+fnOpts = do
639+ opts <- many fnOpt
640+ acc <- accessibility
641+ opts' <- many fnOpt
642+ let allOpts = opts ++ opts'
643+ let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
644+ opts'' <- addDefaultTotality (nub existingTotality) allOpts
645+ return (opts'', acc)
646+ where prettyTot TotalFn = "total"
647+ prettyTot PartialFn = "partial"
648+ prettyTot CoveringFn = "covering"
649+ addDefaultTotality [] opts = do
650+ ist <- get
651+ case default_total ist of
652+ DefaultCheckingTotal -> return (TotalFn:opts)
653+ DefaultCheckingCovering -> return (CoveringFn:opts)
654+ DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
655+ addDefaultTotality [tot] opts = return opts
656+ -- Should really be a semantics error instead of a parser error
657+ addDefaultTotality (tot1:tot2:tots) opts =
658+ fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
659+
660+
661+{-| Parses a function option
662+
663+@
664+FnOpt ::= 'total'
641665 | 'partial'
642666 | 'covering'
643667 | 'implicit'
@@ -660,37 +684,31 @@ NameTimesList ::=
660684 ;
661685@
662686-}
663−-- FIXME: Check compatability for function options (i.e. partal/total)
664−--
665−-- Issue #1574 on the issue tracker.
666−-- https://github.com/idris-lang/Idris-dev/issues/1574
667−fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
668−fnOpts opts
669− = do reservedHL "total"; fnOpts (TotalFn : opts)
670− <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
671− <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
672− <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
673− fnOpts (CExport c : opts)
674− <|> do try (lchar '%' *> reserved "no_implicit");
675− fnOpts (NoImplicit : opts)
676− <|> do try (lchar '%' *> reserved "inline");
677− fnOpts (Inlinable : opts)
678− <|> do try (lchar '%' *> reserved "assert_total");
679− fnOpts (AssertTotal : opts)
680− <|> do try (lchar '%' *> reserved "error_handler");
681− fnOpts (ErrorHandler : opts)
682− <|> do try (lchar '%' *> reserved "error_reverse");
683− fnOpts (ErrorReverse : opts)
684− <|> do try (lchar '%' *> reserved "reflection");
685− fnOpts (Reflection : opts)
686− <|> do try (lchar '%' *> reserved "hint");
687− fnOpts (AutoHint : opts)
688− <|> do lchar '%'; reserved "specialise";
689− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
690− fnOpts (Specialise ns : opts)
691− <|> do reservedHL "implicit"; fnOpts (Implicit : opts)
692− <|> return opts
693− <?> "function modifier"
687+fnOpt :: IdrisParser FnOpt
688+fnOpt = do reservedHL "total"; return TotalFn
689+ <|> do reservedHL "partial"; return PartialFn
690+ <|> do reservedHL "covering"; return CoveringFn
691+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
692+ return $ CExport c
693+ <|> do try (lchar '%' *> reserved "no_implicit");
694+ return NoImplicit
695+ <|> do try (lchar '%' *> reserved "inline");
696+ return Inlinable
697+ <|> do try (lchar '%' *> reserved "assert_total");
698+ return AssertTotal
699+ <|> do try (lchar '%' *> reserved "error_handler");
700+ return ErrorHandler
701+ <|> do try (lchar '%' *> reserved "error_reverse");
702+ return ErrorReverse
703+ <|> do try (lchar '%' *> reserved "reflection");
704+ return Reflection
705+ <|> do try (lchar '%' *> reserved "hint");
706+ return AutoHint
707+ <|> do lchar '%'; reserved "specialise";
708+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';
709+ return $ Specialise ns
710+ <|> do reservedHL "implicit"; return Implicit
711+ <?> "function modifier"
694712 where nameTimes :: IdrisParser (Name, Maybe Int)
695713 nameTimes = do n <- fst <$> fnName
696714 t <- option Nothing (do reds <- fmap fst natural
@@ -712,12 +730,7 @@ postulate syn = do (doc, ext)
712730 ext <- ppostDecl
713731 return (doc, ext)
714732 ist <- get
715− let initOpts = if default_total ist
716− then [TotalFn]
717− else []
718− opts <- fnOpts initOpts
719− acc <- accessibility
720− opts' <- fnOpts opts
733+ (opts, acc) <- fnOpts
721734 (n_in, nfc) <- fnName
722735 let n = expandNS syn n_in
723736 lchar ':'
@@ -725,7 +738,7 @@ postulate syn = do (doc, ext)
725738 fc <- getFC
726739 terminator
727740 addAcc n acc
728− return (PPostulate ext doc syn fc nfc opts' n ty)
741+ return (PPostulate ext doc syn fc nfc opts n ty)
729742 <?> "postulate"
730743 where ppostDecl = do fc <- reservedHL "postulate"; return False
731744 <|> do lchar '%'; reserved "extern"; return True
@@ -940,15 +953,8 @@ InstanceName ::= '[' Name ']';
940953instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
941954instance_ kwopt syn
942955 = do ist <- get
943− let initOpts = if default_total ist
944− then [TotalFn]
945− else []
946−
947956 (doc, argDocs) <- docstring syn
948− opts <- fnOpts initOpts
949− acc <- accessibility
950− opts' <- fnOpts opts
951−
957+ (opts, acc) <- fnOpts
952958 if kwopt then optional instanceKeyword
953959 else do instanceKeyword
954960 return (Just ())
@@ -963,7 +969,7 @@ instance_ kwopt syn
963969 let t = bindList (PPi constraint) cs sc
964970 pnames <- instanceUsing
965971 ds <- instanceBlock syn
966− return [PInstance doc argDocs syn fc cs' pnames acc opts' cn cnfc args [] t en ds]
972+ return [PInstance doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
967973 <?> "implementation declaration"
968974 where instanceName :: IdrisParser Name
969975 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
@@ -1424,14 +1430,15 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)
14241430{- | Parses a totality
14251431
14261432@
1427−Totality ::= 'partial' | 'total'
1433+Totality ::= 'partial' | 'total' | 'covering'
14281434@
14291435
14301436-}
1431−totality :: IdrisParser Bool
1437+totality :: IdrisParser DefaultTotality
14321438totality
1433− = do reservedHL "total"; return True
1434− <|> do reservedHL "partial"; return False
1439+ = do reservedHL "total"; return DefaultCheckingTotal
1440+ <|> do reservedHL "partial"; return DefaultCheckingPartial
1441+ <|> do reservedHL "covering"; return DefaultCheckingCovering
14351442
14361443{- | Parses a type provider
14371444