git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical
commit6df52fa9cd1a9d39e5864fe73992a67a1c188c4f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 15 Jun 2015, 09:59 (11 years ago) parenta440a74a21064e
13 files changed+96−37
compare with master
unifiedsplit
docs/faq/faq.rst+11−7 docs/tutorial/typesfuns.rst+5−5 libs/base/Control/Monad/State.idr+1−1 libs/effects/Effect/Monad.idr+19−12 libs/effects/Effect/Trans.idr+20 libs/effects/effects.ipkg+2−2 src/Idris/Docs.hs+25−10 test/classes001/expected+2 test/docs001/expected+1 test/docs002/expected+3 test/docs003/expected+1 test/docs004/expected+3 test/interactive005/expected+3
docs/faq/faq.rst+11−7
@@ -5,13 +5,17 @@ Frequently Asked Questions
55What are the differences between Agda and Idris?
66================================================
77
8−The main difference is that Idris has been designed from the start to support
9−verified systems programming through easy interoperability with C and high
10−level language constructs to support domain specific language implementation.
11−Idris emphasises general-purpose programming, rather than theorem proving, and
12−as such includes higher level programming constructs such as type classes and
13−do notation. Idris also supports tactic based theorem proving, and has a
14−lightweight Hugs/GHCI style interface.
8+Like Idris, Agda is a functional language with dependent types, supporting
9+dependent pattern matching. Both can be used for writing programs and proofs.
10+However, Idris has been designed from the start to emphasise general purpose
11+programming rather than theorem proving. As such, it supports interoperability
12+with systems libraries and C programs, and language constructs for
13+domain specific language implementation. It also includes higher level
14+programming constructs such as type classes and do notation.
15+
16+Idris supports multiple back ends (C and JavaScript by default, with the
17+ability to add more via plugins) and has a reference run time system, written
18+in C, with a garbage collector and built-in message passing concurrency.
1519
1620Is Idris production ready?
1721==========================
docs/tutorial/typesfuns.rst+5−5
@@ -268,8 +268,8 @@ can be used to calculate a return type:
268268.. code-block:: idris
269269
270270 mkSingle : (x : Bool) -> isSingleton x
271− mkSingle False = 0
272− mkSingle True = []
271+ mkSingle True = 0
272+ mkSingle False = []
273273
274274Or it can be used to have varying input types. The following function
275275calculates either the sum of a list of ``Nat``, or returns the given
@@ -278,9 +278,9 @@ calculates either the sum of a list of ``Nat``, or returns the given
278278.. code-block:: idris
279279
280280 sum : (single : Bool) -> isSingleton single -> Nat
281− sum False x = x
282− sum True [] = 0
283− sum True (x :: xs) = x + sum True xs
281+ sum True x = x
282+ sum False [] = 0
283+ sum False (x :: xs) = x + sum False xs
284284
285285Vectors
286286-------
libs/base/Control/Monad/State.idr+1−1
@@ -1,7 +1,7 @@
11module Control.Monad.State
22
33import public Control.Monad.Identity
4−import Control.Monad.Trans
4+import public Control.Monad.Trans
55
66%access public
77
libs/effects/Effect/Monad.idr+19−12
@@ -2,20 +2,27 @@ module Effect.Monad
22
33import Effects
44
5−-- Eff is a monad too, so we can happily use it in a monad transformer.
5+data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where
6+ MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
67
7−using (xs : List EFFECT, m : Type -> Type)
8− instance Functor (\a => EffM m a xs (\v => xs)) where
9− map f prog = do t <- prog
10− value (f t)
8+instance Functor (MonadEffT xs f) where
9+ map f (MkMonadEffT x) = MkMonadEffT (do x' <- x
10+ pure (f x'))
1111
12− instance Applicative (\a => EffM m a xs (\v => xs)) where
13− pure = value
14− (<*>) f a = do f' <- f
15− a' <- a
16− value (f' a')
12+instance Applicative (MonadEffT xs f) where
13+ pure x = MkMonadEffT (pure x)
14+ (<*>) (MkMonadEffT f) (MkMonadEffT x)
15+ = MkMonadEffT (do f' <- f
16+ x' <- x
17+ pure (f' x'))
1718
18− instance Monad (\a => Eff m a xs (\v => xs)) where
19− (>>=) = Effects.(>>=)
19+instance Monad (MonadEffT xs f) where
20+ (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x
21+ let MkMonadEffT fx = f x'
22+ fx)
2023
24+implicit monadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
25+monadEffT = MkMonadEffT
2126
27+MonadEff : List EFFECT -> Type -> Type
28+MonadEff xs = MonadEffT xs id
libs/effects/Effect/Trans.idrnew file+20
@@ -0,0 +1,20 @@
1+module Effect.Trans
2+
3+import Effects
4+
5+%access public
6+
7+data Trans : (Type -> Type) -> Effect where
8+ Lift : m a -> sig (Trans m) a
9+
10+-- using (m : Type -> Type)
11+instance Monad m => Handler (Trans m) m where
12+ handle st (Lift op) k = do x <- op
13+ k x ()
14+
15+TRANS : (Type -> Type) -> EFFECT
16+TRANS m = MkEff () (Trans m)
17+
18+lift : m a -> Eff a [TRANS m]
19+lift op = call $ Lift op
20+
libs/effects/effects.ipkg+2−2
@@ -1,9 +1,9 @@
11package effects
22
33opts = "--nobasepkgs -i ../prelude -i ../base"
4−modules = Effects, Effect.Default,
4+modules = Effects, Effect.Default, Effect.Monad,
55
66 Effect.Exception, Effect.File, Effect.State,
77 Effect.Random, Effect.StdIO, Effect.Select,
8− Effect.Memory, Effect.System
8+ Effect.Memory, Effect.System, Effect.Trans
99
src/Idris/Docs.hs+25−10
@@ -53,17 +53,26 @@ showDoc ist d
5353 | otherwise = text " -- " <>
5454 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
5555
56−pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
57−pprintFD ist (FD n doc args ty f)
56+pprintFD :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
57+pprintFD ist totalityFlag (FD n doc args ty f)
5858 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
5959 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
6060 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
61+ -- show doc
6162 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
63+ -- show fixity
6264 maybe empty (\f -> text (show f) <> line) f <>
65+ -- show arguments doc
6366 let argshow = showArgs args [] in
64− if not (null argshow)
67+ (if not (null argshow)
6568 then nest 4 $ text "Arguments:" <$> vsep argshow
66− else empty)
69+ else empty) <>
70+ -- show totality status
71+ let totality = getTotality in
72+ (if totalityFlag && not (null totality) then
73+ line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
74+ else
75+ empty))
6776
6877 where ppo = ppOptionIst ist
6978 infixes = idris_infixes ist
@@ -87,15 +96,21 @@ pprintFD ist (FD n doc args ty f)
8796 showArgs args ((n, True):bnd)
8897 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
8998 showArgs [] _ = []
99+ getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
90100
101+pprintFDWithTotality :: IState -> FunDoc -> Doc OutputAnnotation
102+pprintFDWithTotality ist = pprintFD ist True
103+
104+pprintFDWithoutTotality :: IState -> FunDoc -> Doc OutputAnnotation
105+pprintFDWithoutTotality ist = pprintFD ist False
91106
92107pprintDocs :: IState -> Docs -> Doc OutputAnnotation
93−pprintDocs ist (FunDoc d) = pprintFD ist d
108+pprintDocs ist (FunDoc d) = pprintFDWithTotality ist d
94109pprintDocs ist (DataDoc t args)
95− = text "Data type" <+> pprintFD ist t <$>
110+ = text "Data type" <+> pprintFDWithoutTotality ist t <$>
96111 if null args then text "No constructors."
97112 else nest 4 (text "Constructors:" <> line <>
98− vsep (map (pprintFD ist) args))
113+ vsep (map (pprintFDWithoutTotality ist) args))
99114pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)
100115 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
101116 if nullDocstring doc
@@ -105,12 +120,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct
105120 nest 4 (text "Parameters:" <$> prettyParameters)
106121 <> line <$>
107122 nest 4 (text "Methods:" <$>
108− vsep (map (pprintFD ist) meths))
123+ vsep (map (pprintFDWithTotality ist) meths))
109124 <$>
110125 maybe empty
111126 ((<> line) . nest 4 .
112127 (text "Instance constructor:" <$>) .
113− pprintFD ist)
128+ pprintFDWithoutTotality ist)
114129 ctor
115130 <>
116131 nest 4 (text "Instances:" <$>
@@ -195,7 +210,7 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct
195210 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
196211
197212pprintDocs ist (NamedInstanceDoc _cls doc)
198− = nest 4 (text "Named instance:" <$> pprintFD ist doc)
213+ = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist doc)
199214
200215pprintDocs ist (ModDoc mod docs)
201216 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
test/classes001/expected+2
@@ -8,6 +8,7 @@ Methods:
88 myShow : MyShow a => (x : a) -> String
99 The shower
1010
11+ The function is Total
1112Instance constructor:
1213 MkMyShow : (myShow : a -> String) -> MyShow a
1314 Build a MyShow
@@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
2526
2627 myShow : a -> String -- The shower
2728
29+ The function is Total
test/docs001/expected+1
@@ -8,6 +8,7 @@ Methods:
88 m : C t => t
99 member of class
1010
11+ The function is Total
1112Instances:
1213 C A
1314 instance of class
test/docs002/expected+3
@@ -1,9 +1,12 @@
11T1 : Type
22 Some documentation
33
4+ The function is Total
45T2 : Type
56 Some other documentation
67
8+ The function is Total
79T3 : Int
810 Some provided postulate
911
12+ The function is not yet checked for totality
test/docs003/expected+1
@@ -8,6 +8,7 @@ Methods:
88 map : Functor f => (m : a -> b) -> f a -> f b
99 The action of the functor on morphisms
1010
11+ The function is Total
1112Instances:
1213 Functor List
1314 Functor Stream
test/docs004/expected+3
@@ -7,9 +7,12 @@ MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
77
88 baz : Bool -- A field baz
99
10+ The function is Total
1011bar : (rec : Foo a) -> Nat
1112 A field bar
1213
14+ The function is Total
1315baz : (rec : Foo a) -> Bool
1416 A field baz
1517
18+ The function is Total
test/interactive005/expected+3
@@ -3,6 +3,7 @@ Hello, World
33main : IO ()
44 This is a docstring
55
6+ The function is Total
67Main.main is Total
78Hello, World
89Prelude.Basics.id : a -> a
@@ -26,8 +27,10 @@ main : IO ()
2627 is a
2728 docstring
2829
30+ The function is Total
2931main : IO ()
3032 This is a docstring
3133
34+ The function is Total
3235Nat2 : Type
3336Invalid filename for compiler output "Test.idr"