fdb79e6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added warranty information to the Idris Repl.

fdb79e6Jan de Muijnck-Hughes12 years ago

src/Idris/AbsSyntaxTree.hs+5−6

compare with master

unifiedsplit

@@ -339,7 +339,7 @@ data Command = Quit

339 | WhoCalls Name

340 | CallsWho Name

341 | MakeDoc String -- IdrisDoc

342−

342+ | Warranty

343

344data Opt = Filename String

345 | Quiet

@@ -1159,7 +1159,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1159 colour ItalicText = IdrisColour Nothing True False False True

1160

1161-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1162−prettyImp :: PPOption -- ^^ pretty printing options

1162+prettyImp :: PPOption -- ^^ pretty printing options

1163 -> PTerm -- ^^ the term to pretty-print

1164 -> Doc OutputAnnotation

1165prettyImp impl = pprintPTerm impl [] [] []

@@ -1169,7 +1169,7 @@ prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1169prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1170

1171-- | Pretty-print a high-level Idris term in some bindings context with infix info

1172−pprintPTerm :: PPOption -- ^^ pretty printing options

1172+pprintPTerm :: PPOption -- ^^ pretty printing options

1173 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1174 -> [Name] -- ^^ names to always show in pi, even if not used

1175 -> [FixDecl] -- ^^ Fixity declarations

@@ -1422,7 +1422,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1422 getFixity = flip M.lookup fixities

1423

1424prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1425−prettyDocumentedIst ist (name, ty, docs) =

1425+prettyDocumentedIst ist (name, ty, docs) =

1426 prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1427 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1428

@@ -1443,7 +1443,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

1443 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1444 | otherwise = strName n

1445 strName n | n == falseTy = "_|_"

1446− strName (MN i s) = T.unpack s

1446+ strName (MN i s) = T.unpack s

1447 strName other = show other

1448

1449

@@ -1702,4 +1702,3 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1702

1703 niTacImp env (TacImp _ _ scr) = ni env scr

1704 niTacImp _ _ = []

1705−

src/Idris/Help.hs+2−1

@@ -58,7 +58,8 @@ help =

58 ([":unset"], OptionArg, "Unset an option"),

59 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

60 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

61− ([":q",":quit"], NoArg, "Exit the Idris system")

61+ ([":q",":quit"], NoArg, "Exit the Idris system"),

62+ ([":w", ":warranty"], NoArg, "Displays warranty information")

62 ]

63 ]

64-- | Use these for completion, but don't show them in :help

65-- | Use these for completion, but don't show them in :help

src/Idris/REPL.hs+25−9

@@ -110,7 +110,7 @@ repl orig mods

110 return ()

111 Just input -> -- H.catch

112 do ms <- H.catch (lift $ processInput input orig mods)

113− (ctrlC (return (Just mods)))

113+ (ctrlC (return (Just mods)))

114 case ms of

115 Just mods -> repl orig mods

116 Nothing -> return ()

@@ -121,7 +121,7 @@ repl orig mods

121 act -- repl orig mods

122

123 showMVs c thm [] = ""

124− showMVs c thm ms = "Metavariables: " ++

124+ showMVs c thm ms = "Metavariables: " ++

125 show' 4 c thm (map fst ms) ++ "\n"

126

127 show' 0 c thm ms = let l = length ms in

@@ -129,7 +129,7 @@ repl orig mods

129 ++ " other"

130 ++ if l == 1 then ")" else "s)"

131 show' n c thm [m] = showM c thm m

132− show' n c thm (m : ms) = showM c thm m ++ ", " ++

132+ show' n c thm (m : ms) = showM c thm m ++ ", " ++

133 show' (n - 1) c thm ms

134

135 showM c thm n = if c then colouriseFun thm (show n)

@@ -388,6 +388,7 @@ splitName s = case reverse $ splitOn "." s of

388 (n:ns) -> Right $ sNS (sUN n) ns

389

390ideslaveProcess :: FilePath -> Command -> Idris ()

391+ideslaveProcess fn Warranty = process stdout fn Warranty

391ideslaveProcess fn Help = process stdout fn Help

392ideslaveProcess fn Help = process stdout fn Help

392ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

393ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

393 iPrintResult "changed directory to"

394 iPrintResult "changed directory to"

@@ -564,6 +565,7 @@ insertScript prf (x : xs) = x : insertScript prf xs

564

565

565process :: Handle -> FilePath -> Command -> Idris ()

566process :: Handle -> FilePath -> Command -> Idris ()

566process h fn Help = iPrintResult displayHelp

567process h fn Help = iPrintResult displayHelp

568+process h fn Warranty = iPrintResult warranty

567process h fn (ChangeDirectory f)

569process h fn (ChangeDirectory f)

568 = do runIO $ setCurrentDirectory f

570 = do runIO $ setCurrentDirectory f

569 return ()

571 return ()

@@ -709,7 +711,7 @@ process h fn (DebugInfo n)

709 when (not (null cg')) $ do iputStrLn "Call graph:\n"

711 when (not (null cg')) $ do iputStrLn "Call graph:\n"

710 iputStrLn (show cg')

712 iputStrLn (show cg')

711process h fn (Search t) = searchByType h t

713process h fn (Search t) = searchByType h t

712−process h fn (CaseSplitAt updatefile l n)

714+process h fn (CaseSplitAt updatefile l n)

713 = caseSplitAt h fn updatefile l n

715 = caseSplitAt h fn updatefile l n

714process h fn (AddClauseFrom updatefile l n)

716process h fn (AddClauseFrom updatefile l n)

715 = addClauseFrom h fn updatefile l n

717 = addClauseFrom h fn updatefile l n

@@ -1022,10 +1024,10 @@ loadInputs h inputs toline -- furthest line to read in input source files

1022 let ifiles = getModuleFiles modTree

1024 let ifiles = getModuleFiles modTree

1023 iLOG ("MODULE TREE : " ++ show modTree)

1025 iLOG ("MODULE TREE : " ++ show modTree)

1024 iLOG ("RELOAD: " ++ show ifiles)

1026 iLOG ("RELOAD: " ++ show ifiles)

1025− when (not (all ibc ifiles) || loadCode) $

1027+ when (not (all ibc ifiles) || loadCode) $

1026 tryLoad False (filter (not . ibc) ifiles)

1028 tryLoad False (filter (not . ibc) ifiles)

1027 -- return the files that need rechecking

1029 -- return the files that need rechecking

1028− return ifiles)

1030+ return ifiles)

1029 ninputs

1031 ninputs

1030 inew <- getIState

1032 inew <- getIState

1031 let tidata = idris_tyinfodata inew

1033 let tidata = idris_tyinfodata inew

@@ -1395,6 +1397,20 @@ banner = " ____ __ _ \n" ++

1395 " / _/___/ /____(_)____ \n" ++

1397 " / _/___/ /____(_)____ \n" ++

1396 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1398 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1397 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

1399 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

1398− " /___/\\__,_/_/ /_/____/ Type :? for help \n"

1400+ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++

1399−

1401+ "\n" ++

1400−

1402+ "Idris is a research tool distributed with ABSOLUTELY NO WARRANTY.\n" ++

1403+ "For details type :warranty."

1404+

1405+warranty = "\n" ++

1406+ "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++

1407+ "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++

1408+ "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++

1409+ "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++

1410+ "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++

1411+ "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++

1412+ "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++

1413+ "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++

1414+ "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++

1415+ "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++

1416+ "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"

src/Idris/REPLParser.hs+5−4

@@ -33,6 +33,7 @@ cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) x

33pCmd :: P.IdrisParser Command

34pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

35 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

36+ <|> try (do cmd ["w", "warranty"]; eof; return Warranty)

36 <|> try (do cmd ["r", "reload"]; eof; return Reload)

37 <|> try (do cmd ["r", "reload"]; eof; return Reload)

37 <|> try (do cmd ["module"]; f <- P.identifier; eof;

38 <|> try (do cmd ["module"]; f <- P.identifier; eof;

38 return (ModImport (toPath f)))

39 return (ModImport (toPath f)))

@@ -48,11 +49,11 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

48 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

49 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

49 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

50 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

50 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

51 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

51− <|> try (do cmd ["lto", "loadto"];

52+ <|> try (do cmd ["lto", "loadto"];

52 toline <- P.natural

53 toline <- P.natural

53− f <- many anyChar;

54+ f <- many anyChar;

54 return (Load f (Just (fromInteger toline))))

55 return (Load f (Just (fromInteger toline))))

55− <|> try (do cmd ["l", "load"]; f <- many anyChar;

56+ <|> try (do cmd ["l", "load"]; f <- many anyChar;

56 return (Load f Nothing))

57 return (Load f Nothing))

57 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

58 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

58 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

59 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

@@ -71,7 +72,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

71 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

72 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

72 <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

73 <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

73 <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

74 <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

74− <|> try (do cmd ["s", "search"]; P.whiteSpace;

75+ <|> try (do cmd ["s", "search"]; P.whiteSpace;

75 t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))

76 t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))

76 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 upd <- option False (do P.lchar '!'; return True)

78 upd <- option False (do P.lchar '!'; return True)