fdb79e6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added warranty information to the Idris Repl.

Added REPL command: `:w`, `:warranty`. This command displays the warranty information governing the use of `Idris`. This information comes from the last paragraph of the software license that `Idris` is licensed under.

commitfdb79e633c5f5c984a7f79092110c73f04c408fb authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateMon 2 Jun 2014, 16:41 (12 years ago) parentdcd9568

4 files changed+37−20

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+5−6 src/Idris/Help.hs+2−1 src/Idris/REPL.hs+25−9 src/Idris/REPLParser.hs+5−4

src/Idris/AbsSyntaxTree.hs+5−6

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

339339 | WhoCalls Name

340340 | CallsWho Name

341341 | MakeDoc String -- IdrisDoc

342−

342+ | Warranty

343343

344344data Opt = Filename String

345345 | Quiet

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

11591159 colour ItalicText = IdrisColour Nothing True False False True

11601160

11611161-- | 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

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

11641164 -> Doc OutputAnnotation

11651165prettyImp impl = pprintPTerm impl [] [] []

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

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

11701170

11711171-- | 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

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

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

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

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

14221422 getFixity = flip M.lookup fixities

14231423

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

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

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

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

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

14281428

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

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

14441444 | otherwise = strName n

14451445 strName n | n == falseTy = "_|_"

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

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

14471447 strName other = show other

14481448

14491449

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

17021702

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

17041704 niTacImp _ _ = []

1705−

src/Idris/Help.hs+2−1

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

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

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

6060 ([":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")

6263 ]

6364

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

src/Idris/REPL.hs+25−9

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

110110 return ()

111111 Just input -> -- H.catch

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

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

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

114114 case ms of

115115 Just mods -> repl orig mods

116116 Nothing -> return ()

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

121121 act -- repl orig mods

122122

123123 showMVs c thm [] = ""

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

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

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

126126

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

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

129129 ++ " other"

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

131131 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 ++ ", " ++

133133 show' (n - 1) c thm ms

134134

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

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

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

389389

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

391+ideslaveProcess fn Warranty = process stdout fn Warranty

391392ideslaveProcess fn Help = process stdout fn Help

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

393394 iPrintResult "changed directory to"

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

564565

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

566567process h fn Help = iPrintResult displayHelp

568+process h fn Warranty = iPrintResult warranty

567569process h fn (ChangeDirectory f)

568570 = do runIO $ setCurrentDirectory f

569571 return ()

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

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

710712 iputStrLn (show cg')

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

712−process h fn (CaseSplitAt updatefile l n)

714+process h fn (CaseSplitAt updatefile l n)

713715 = caseSplitAt h fn updatefile l n

714716process h fn (AddClauseFrom updatefile l n)

715717 = addClauseFrom h fn updatefile l n

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

10221024 let ifiles = getModuleFiles modTree

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

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

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

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

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

10271029 -- return the files that need rechecking

1028− return ifiles)

1030+ return ifiles)

10291031 ninputs

10301032 inew <- getIState

10311033 let tidata = idris_tyinfodata inew

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

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

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

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

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

1399−

1400−

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

1401+ "\n" ++

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

3333pCmd :: P.IdrisParser Command

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

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

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

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

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

3839 return (ModImport (toPath f)))

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

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

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

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

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

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

5253 toline <- P.natural

53− f <- many anyChar;

54+ f <- many anyChar;

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

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

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

5657 return (Load f Nothing))

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

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

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

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

7374 <|> 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;

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

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

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