c5f2052 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fixed the way default totality modifiers are added, and checked for conflicting totality modifiers.

c5f2052Ahmad Salim Al-Sibahi10 years ago

libs/prelude/Prelude/File.idr+2−2

compare with master

unifiedsplit

@@ -233,7 +233,7 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

233 return (p > 0)

234

235||| Read the contents of a file into a string

236−partial -- might be reading something infinitely long like /dev/null ...

236+-- might be reading something infinitely long like /dev/null ...

237covering export

238readFile : String -> IO (Either FileError String)

239readFile fn = do Right h <- openFile fn Read

@@ -242,7 +242,7 @@ readFile fn = do Right h <- openFile fn Read

242 closeFile h

243 return c

244 where

245− partial

245+ covering

246 readFile' : File -> String -> IO (Either FileError String)

247 readFile' h contents =

248 do x <- fEOF h

src/Idris/Parser.hs+63−60

@@ -594,19 +594,12 @@ fnDecl' syn = checkFixity $

594 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

595 pushIndent

596 (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

605 (n_in, nfc) <- fnName

598 (n_in, nfc) <- fnName

606 let n = expandNS syn n_in

599 let n = expandNS syn n_in

607 fc <- getFC

600 fc <- getFC

608 lchar ':'

601 lchar ':'

609− return (doc, argDocs, fc, opts', n, nfc, acc))

602+ return (doc, argDocs, fc, opts, n, nfc, acc))

610 ty <- typeExpr (allowImp syn)

603 ty <- typeExpr (allowImp syn)

611 terminator

604 terminator

612 -- If it's a top level function, note the accessibility

605 -- If it's a top level function, note the accessibility

@@ -634,10 +627,40 @@ fnDecl' syn = checkFixity $

634 | otherwise = return True

627 | otherwise = return True

635 fixityOK _ = return True

628 fixityOK _ = return True

636

629

637−{-| Parses function options given initial options

630+{-| Parses a series of function and accessbility options

638

631

639@

632@

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+@

640−FnOpts ::= 'total'

663+FnOpt ::= 'total'

641 | 'partial'

664 | 'partial'

642 | 'covering'

665 | 'covering'

643 | 'implicit'

666 | 'implicit'

@@ -660,37 +683,31 @@ NameTimesList ::=

660 ;

683 ;

661@

684@

662-}

685-}

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]

686+fnOpt :: IdrisParser FnOpt

668−fnOpts opts

669− = do reservedHL "total"; fnOpts (TotalFn : opts)

687+fnOpt = do reservedHL "total"; return TotalFn

670− <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))

688+ <|> do reservedHL "partial"; return PartialFn

671− <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

689+ <|> do reservedHL "covering"; return CoveringFn

672− <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

690+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

673− fnOpts (CExport c : opts)

691+ return $ CExport c

674− <|> do try (lchar '%' *> reserved "no_implicit");

692+ <|> do try (lchar '%' *> reserved "no_implicit");

675− fnOpts (NoImplicit : opts)

693+ return NoImplicit

676− <|> do try (lchar '%' *> reserved "inline");

694+ <|> do try (lchar '%' *> reserved "inline");

677− fnOpts (Inlinable : opts)

695+ return Inlinable

678− <|> do try (lchar '%' *> reserved "assert_total");

696+ <|> do try (lchar '%' *> reserved "assert_total");

679− fnOpts (AssertTotal : opts)

697+ return AssertTotal

680− <|> do try (lchar '%' *> reserved "error_handler");

698+ <|> do try (lchar '%' *> reserved "error_handler");

681− fnOpts (ErrorHandler : opts)

699+ return ErrorHandler

682− <|> do try (lchar '%' *> reserved "error_reverse");

700+ <|> do try (lchar '%' *> reserved "error_reverse");

683− fnOpts (ErrorReverse : opts)

701+ return ErrorReverse

684− <|> do try (lchar '%' *> reserved "reflection");

702+ <|> do try (lchar '%' *> reserved "reflection");

685− fnOpts (Reflection : opts)

703+ return Reflection

686− <|> do try (lchar '%' *> reserved "hint");

704+ <|> do try (lchar '%' *> reserved "hint");

687− fnOpts (AutoHint : opts)

705+ return AutoHint

688− <|> do lchar '%'; reserved "specialise";

706+ <|> do lchar '%'; reserved "specialise";

689− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

707+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

690− fnOpts (Specialise ns : opts)

708+ return $ Specialise ns

691− <|> do reservedHL "implicit"; fnOpts (Implicit : opts)

709+ <|> do reservedHL "implicit"; return Implicit

692− <|> return opts

693− <?> "function modifier"

710+ <?> "function modifier"

694 where nameTimes :: IdrisParser (Name, Maybe Int)

711 where nameTimes :: IdrisParser (Name, Maybe Int)

695 nameTimes = do n <- fst <$> fnName

712 nameTimes = do n <- fst <$> fnName

696 t <- option Nothing (do reds <- fmap fst natural

713 t <- option Nothing (do reds <- fmap fst natural

@@ -712,13 +729,7 @@ postulate syn = do (doc, ext)

712 ext <- ppostDecl

729 ext <- ppostDecl

713 return (doc, ext)

730 return (doc, ext)

714 ist <- get

731 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

722 (n_in, nfc) <- fnName

733 (n_in, nfc) <- fnName

723 let n = expandNS syn n_in

734 let n = expandNS syn n_in

724 lchar ':'

735 lchar ':'

@@ -726,7 +737,7 @@ postulate syn = do (doc, ext)

726 fc <- getFC

737 fc <- getFC

727 terminator

738 terminator

728 addAcc n acc

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

730 <?> "postulate"

741 <?> "postulate"

731 where ppostDecl = do fc <- reservedHL "postulate"; return False

742 where ppostDecl = do fc <- reservedHL "postulate"; return False

732 <|> do lchar '%'; reserved "extern"; return True

743 <|> do lchar '%'; reserved "extern"; return True

@@ -921,16 +932,8 @@ InstanceName ::= '[' Name ']';

921instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

932instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

922instance_ kwopt syn

933instance_ kwopt syn

923 = do ist <- get

934 = do ist <- get

924− let initOpts = case default_total ist of

925− DefaultCheckingTotal -> [TotalFn]

926− DefaultCheckingCovering -> [CoveringFn]

927− _ -> []

928−

929 (doc, argDocs) <- docstring syn

935 (doc, argDocs) <- docstring syn

930− opts <- fnOpts initOpts

931− acc <- accessibility

932− opts' <- fnOpts opts

936+ (opts, acc) <- fnOpts

933−

934 if kwopt then optional instanceKeyword

937 if kwopt then optional instanceKeyword

935 else do instanceKeyword

938 else do instanceKeyword

936 return (Just ())

939 return (Just ())

@@ -944,7 +947,7 @@ instance_ kwopt syn

944 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

947 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

945 let t = bindList (PPi constraint) cs sc

948 let t = bindList (PPi constraint) cs sc

946 ds <- instanceBlock syn

949 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]

948 <?> "implementation declaration"

951 <?> "implementation declaration"

949 where instanceName :: IdrisParser Name

952 where instanceName :: IdrisParser Name

950 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

953 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'