8a48c26 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' into repl-definitions

8a48c26Alyssa Carter12 years ago

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -8,6 +8,7 @@ Michael R. Bernstein

8Nicola Botta

9Edwin Brady

10David Raymond Christiansen

11+Carter Charbonneau

11Jason Dagit

12Jason Dagit

12Simon Fowler

13Simon Fowler

13Google

14Google

libs/prelude/Prelude/Applicative.idr+4

@@ -13,6 +13,10 @@ class Functor f => Applicative (f : Type -> Type) where

13 pure : a -> f a

14 (<$>) : f (a -> b) -> f a -> f b

16+instance Applicative id where

17+ pure a = a

18+ f <$> a = f a

19+

16infixl 2 <$

20infixl 2 <$

17(<$) : Applicative f => f a -> f b -> f a

21(<$) : Applicative f => f a -> f b -> f a

18a <$ b = map const a <$> b

22a <$ b = map const a <$> b

libs/prelude/Prelude/Functor.idr+5

@@ -1,5 +1,7 @@

1module Prelude.Functor

3+import Prelude.Basics

3||| Functors

5||| Functors

4||| @ f the action of the functor on objects

6||| @ f the action of the functor on objects

5class Functor (f : Type -> Type) where

7class Functor (f : Type -> Type) where

@@ -7,3 +9,6 @@ class Functor (f : Type -> Type) where

7 ||| @ f the functor

9 ||| @ f the functor

8 ||| @ m the morphism

10 ||| @ m the morphism

9 map : (m : a -> b) -> f a -> f b

11 map : (m : a -> b) -> f a -> f b

12+

13+instance Functor id where

14+ map f a = f a

libs/prelude/Prelude/Monad.idr+4

@@ -5,6 +5,7 @@ module Prelude.Monad

5import Builtins

6import Prelude.List

7import Prelude.Applicative

8+import Prelude.Basics

9%access public

10%access public

@@ -13,6 +14,9 @@ infixl 5 >>=

13class Applicative m => Monad (m : Type -> Type) where

14class Applicative m => Monad (m : Type -> Type) where

14 (>>=) : m a -> (a -> m b) -> m b

15 (>>=) : m a -> (a -> m b) -> m b

17+instance Monad id where

18+ a >>= f = f a

19+

16||| Also called `join` or mu

20||| Also called `join` or mu

17flatten : Monad m => m (m a) -> m a

21flatten : Monad m => m (m a) -> m a

18flatten a = a >>= id

22flatten a = a >>= id

src/Idris/REPLParser.hs+97−96

@@ -27,106 +27,107 @@ parseCmd :: IState -> String -> String -> Result Command

27parseCmd i inputname = P.runparser pCmd i inputname

29cmd :: [String] -> P.IdrisParser ()

30−cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

30+cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs))

31 where docmd [] = fail "No such command"

32− docmd (x:xs) = try (discard (P.symbol x)) <|> docmd xs

32+ docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs

34pCmd :: P.IdrisParser Command

35+

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

36+pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

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

37+ <|> do cmd ["h", "?", "help"]; eof; return Help

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

38+ <|> do cmd ["w", "warranty"]; eof; return Warranty

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

39+ <|> do cmd ["r", "reload"]; eof; return Reload

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

40+ <|> do cmd ["module"]; f <- P.identifier; eof;

40− return (ModImport (toPath f)))

41+ return (ModImport (toPath f))

41− <|> try (do cmd ["e", "edit"]; eof; return Edit)

42+ <|> do cmd ["e", "edit"]; eof; return Edit

42− <|> try (do cmd ["exec", "execute"]; eof; return Execute)

43+ <|> do cmd ["exec", "execute"]; eof; return Execute

43− <|> try (do cmd ["c", "compile"]

44+ <|> do cmd ["c", "compile"]

44− i <- get

45+ i <- get

45− c <- option (opt_codegen $ idris_options i) codegenOption

46+ c <- option (opt_codegen $ idris_options i) codegenOption

46− f <- P.identifier

47+ f <- P.identifier

47− eof

48+ eof

48− return (Compile c f))

49+ return (Compile c f)

49− <|> try (do cmd ["proofs"]; eof; return Proofs)

50+ <|> do cmd ["proofs"]; eof; return Proofs

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

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

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

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

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

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

53− <|> try (do cmd ["let"]

54+ <|> do cmd ["let"]

54− defn <- concat <$> many (P.decl defaultSyntax)

55+ defn <- concat <$> many (P.decl defaultSyntax)

55− return (NewDefn defn))

56+ return (NewDefn defn)

56− <|> try (do cmd ["unlet","undefine"]

57+ <|> do cmd ["unlet","undefine"]

57− Undefine `fmap` many P.name)

58+ Undefine `fmap` many P.name

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

59+ <|> do cmd ["lto", "loadto"];

59− toline <- P.natural

60+ toline <- P.natural

60− f <- many anyChar;

61+ f <- many anyChar;

61− return (Load f (Just (fromInteger toline))))

62+ return (Load f (Just (fromInteger toline)))

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

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

63− return (Load f Nothing))

64+ return (Load f Nothing)

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

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

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

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

66− <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

67+ <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)

67− <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

68+ <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)

68− <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))

69+ <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))

69− <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))

70+ <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))

70− <|> try (do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n))

71+ <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)

71− <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

72+ <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)

72− <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

73+ <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)

73− <|> try (do cmd ["u", "universes"]; eof; return Universes)

74+ <|> do cmd ["u", "universes"]; eof; return Universes

74− <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))

75+ <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)

75− <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

76+ <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)

76 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

77 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

77− <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

78+ <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)

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

79+ <|> do cmd ["color", "colour"]; pSetColourCmd

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

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

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

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

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

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

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

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

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

84+ <|> do cmd ["cs", "casesplit"]; P.whiteSpace;

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

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

85− l <- P.natural; n <- P.name;

86+ l <- P.natural; n <- P.name;

86− return (CaseSplitAt upd (fromInteger l) n))

87+ return (CaseSplitAt upd (fromInteger l) n)

87− <|> try (do cmd ["apc", "addproofclause"]; P.whiteSpace;

88+ <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;

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

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

89− l <- P.natural; n <- P.name;

90+ l <- P.natural; n <- P.name;

90− return (AddProofClauseFrom upd (fromInteger l) n))

91+ return (AddProofClauseFrom upd (fromInteger l) n)

91− <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;

92+ <|> do cmd ["ac", "addclause"]; P.whiteSpace;

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

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

93− l <- P.natural; n <- P.name;

94+ l <- P.natural; n <- P.name;

94− return (AddClauseFrom upd (fromInteger l) n))

95+ return (AddClauseFrom upd (fromInteger l) n)

95− <|> try (do cmd ["am", "addmissing"]; P.whiteSpace;

96+ <|> do cmd ["am", "addmissing"]; P.whiteSpace;

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

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

97− l <- P.natural; n <- P.name;

98+ l <- P.natural; n <- P.name;

98− return (AddMissing upd (fromInteger l) n))

99+ return (AddMissing upd (fromInteger l) n)

99− <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;

100+ <|> do cmd ["mw", "makewith"]; P.whiteSpace;

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

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

101− l <- P.natural; n <- P.name;

102+ l <- P.natural; n <- P.name;

102− return (MakeWith upd (fromInteger l) n))

103+ return (MakeWith upd (fromInteger l) n)

103− <|> try (do cmd ["ml", "makelemma"]; P.whiteSpace;

104+ <|> do cmd ["ml", "makelemma"]; P.whiteSpace;

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

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

105− l <- P.natural; n <- P.name;

106+ l <- P.natural; n <- P.name;

106− return (MakeLemma upd (fromInteger l) n))

107+ return (MakeLemma upd (fromInteger l) n)

107− <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

108+ <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;

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

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

109− l <- P.natural; n <- P.name;

110+ l <- P.natural; n <- P.name;

110− hints <- many P.fnName

111+ hints <- many P.fnName

111− return (DoProofSearch upd True (fromInteger l) n hints))

112+ return (DoProofSearch upd True (fromInteger l) n hints)

112− <|> try (do cmd ["ref", "refine"]; P.whiteSpace;

113+ <|> do cmd ["ref", "refine"]; P.whiteSpace;

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

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

114− l <- P.natural; n <- P.name;

115+ l <- P.natural; n <- P.name;

115− hint <- P.fnName

116+ hint <- P.fnName

116− return (DoProofSearch upd False (fromInteger l) n [hint]))

117+ return (DoProofSearch upd False (fromInteger l) n [hint])

117− <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

118+ <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)

118− <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

119+ <|> do cmd ["m", "metavars"]; eof; return Metavars

119− <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

120+ <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

120− return (Just x))

121+ return (Just x))

121− eof; return (AddProof n))

122+ eof; return (AddProof n)

122− <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

123+ <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)

123− <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

124+ <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)

124− <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

125+ <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers

125− <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))

126+ <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)

126− <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))

127+ <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)

127− <|> try (do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n))

128+ <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)

128− <|> try (do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n))

129+ <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)

129− <|> try (do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str))

130+ <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)

130 <|> do P.whiteSpace; do eof; return NOP

131 <|> do P.whiteSpace; do eof; return NOP

131 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

132 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

132

133