@@ -594,19 +594,12 @@ fnDecl' syn = checkFixity $
594594 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
595595 pushIndent
596596 (doc, argDocs) <- docstring syn
597− ist <- get
598− let initOpts = case default_total ist of
599− DefaultCheckingTotal -> [TotalFn]
600− DefaultCheckingCovering -> [CoveringFn]
601− _ -> []
602− opts <- fnOpts initOpts
603− acc <- accessibility
604− opts' <- fnOpts opts
597+ (opts, acc) <- fnOpts
605598 (n_in, nfc) <- fnName
606599 let n = expandNS syn n_in
607600 fc <- getFC
608601 lchar ':'
609− return (doc, argDocs, fc, opts', n, nfc, acc))
602+ return (doc, argDocs, fc, opts, n, nfc, acc))
610603 ty <- typeExpr (allowImp syn)
611604 terminator
612605 -- If it's a top level function, note the accessibility
@@ -634,10 +627,40 @@ fnDecl' syn = checkFixity $
634627 | otherwise = return True
635628 fixityOK _ = return True
636629
637−{-| Parses function options given initial options
630+{-| Parses a series of function and accessbility options
638631
639632@
640−FnOpts ::= 'total'
633+FnOpts ::= FnOpt* Accessibility FnOpt*
634+@
635+ -}
636+fnOpts :: IdrisParser ([FnOpt], Accessibility)
637+fnOpts = do
638+ opts <- many fnOpt
639+ acc <- accessibility
640+ opts' <- many fnOpt
641+ let allOpts = opts ++ opts'
642+ let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
643+ opts'' <- addDefaultTotality (nub existingTotality) allOpts
644+ return (opts'', acc)
645+ where prettyTot TotalFn = "total"
646+ prettyTot PartialFn = "partial"
647+ prettyTot CoveringFn = "covering"
648+ addDefaultTotality [] opts = do
649+ ist <- get
650+ case default_total ist of
651+ DefaultCheckingTotal -> return (TotalFn:opts)
652+ DefaultCheckingCovering -> return (CoveringFn:opts)
653+ DefaultCheckingPartial -> return (PartialFn:opts)
654+ addDefaultTotality [tot] opts = return opts
655+ -- Should really be a semantics error instead of a parser error
656+ addDefaultTotality (tot1:tot2:tots) opts =
657+ fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
658+
659+
660+{-| Parses a function option
661+
662+@
663+FnOpt ::= 'total'
641664 | 'partial'
642665 | 'covering'
643666 | 'implicit'
@@ -660,37 +683,31 @@ NameTimesList ::=
660683 ;
661684@
662685-}
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"
686+fnOpt :: IdrisParser FnOpt
687+fnOpt = do reservedHL "total"; return TotalFn
688+ <|> do reservedHL "partial"; return PartialFn
689+ <|> do reservedHL "covering"; return CoveringFn
690+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
691+ return $ CExport c
692+ <|> do try (lchar '%' *> reserved "no_implicit");
693+ return NoImplicit
694+ <|> do try (lchar '%' *> reserved "inline");
695+ return Inlinable
696+ <|> do try (lchar '%' *> reserved "assert_total");
697+ return AssertTotal
698+ <|> do try (lchar '%' *> reserved "error_handler");
699+ return ErrorHandler
700+ <|> do try (lchar '%' *> reserved "error_reverse");
701+ return ErrorReverse
702+ <|> do try (lchar '%' *> reserved "reflection");
703+ return Reflection
704+ <|> do try (lchar '%' *> reserved "hint");
705+ return AutoHint
706+ <|> do lchar '%'; reserved "specialise";
707+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';
708+ return $ Specialise ns
709+ <|> do reservedHL "implicit"; return Implicit
710+ <?> "function modifier"
694711 where nameTimes :: IdrisParser (Name, Maybe Int)
695712 nameTimes = do n <- fst <$> fnName
696713 t <- option Nothing (do reds <- fmap fst natural
@@ -712,13 +729,7 @@ postulate syn = do (doc, ext)
712729 ext <- ppostDecl
713730 return (doc, ext)
714731 ist <- get
715− let initOpts = case default_total ist of
716− DefaultCheckingTotal -> [TotalFn]
717− DefaultCheckingCovering -> [CoveringFn]
718− _ -> []
719− opts <- fnOpts initOpts
720− acc <- accessibility
721− opts' <- fnOpts opts
732+ (opts, acc) <- fnOpts
722733 (n_in, nfc) <- fnName
723734 let n = expandNS syn n_in
724735 lchar ':'
@@ -726,7 +737,7 @@ postulate syn = do (doc, ext)
726737 fc <- getFC
727738 terminator
728739 addAcc n acc
729− return (PPostulate ext doc syn fc nfc opts' n ty)
740+ return (PPostulate ext doc syn fc nfc opts n ty)
730741 <?> "postulate"
731742 where ppostDecl = do fc <- reservedHL "postulate"; return False
732743 <|> do lchar '%'; reserved "extern"; return True
@@ -921,16 +932,8 @@ InstanceName ::= '[' Name ']';
921932instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
922933instance_ kwopt syn
923934 = do ist <- get
924− let initOpts = case default_total ist of
925− DefaultCheckingTotal -> [TotalFn]
926− DefaultCheckingCovering -> [CoveringFn]
927− _ -> []
928−
929935 (doc, argDocs) <- docstring syn
930− opts <- fnOpts initOpts
931− acc <- accessibility
932− opts' <- fnOpts opts
933−
936+ (opts, acc) <- fnOpts
934937 if kwopt then optional instanceKeyword
935938 else do instanceKeyword
936939 return (Just ())
@@ -944,7 +947,7 @@ instance_ kwopt syn
944947 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
945948 let t = bindList (PPi constraint) cs sc
946949 ds <- instanceBlock syn
947− return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args t en ds]
950+ return [PInstance doc argDocs syn fc cs' acc opts cn cnfc args t en ds]
948951 <?> "implementation declaration"
949952 where instanceName :: IdrisParser Name
950953 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'