From 0922ca11a851a2f511875df31bacd53d1d3892e3 Mon Sep 17 00:00:00 2001 From: Guglielmo Fachini Date: Sat, 13 Jun 2015 15:57:26 +0200 Subject: [PATCH 1/6] Fix #2176 by adding totality status to the REPL :doc command output *) pprintFD receives a boolean argument that allows to show the totality status when needed *) pprintFDWithoutTotality behaves as the old pprintFD *) pprintFDWithTotality behaves as the old pprintFD and add a new line with the totality status of the given function *) the totality status is not considered for data types (and their constructors) and type classes (and their instance constructors and named instances) --- src/Idris/Docs.hs | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/src/Idris/Docs.hs b/src/Idris/Docs.hs index f7080b362..a8e1f403d 100644 --- a/src/Idris/Docs.hs +++ b/src/Idris/Docs.hs @@ -53,17 +53,26 @@ showDoc ist d | otherwise = text " -- " <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d -pprintFD :: IState -> FunDoc -> Doc OutputAnnotation -pprintFD ist (FD n doc args ty f) +pprintFD :: IState -> Bool -> FunDoc -> Doc OutputAnnotation +pprintFD ist totalityFlag (FD n doc args ty f) = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$> + -- show doc renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$> + -- show fixity maybe empty (\f -> text (show f) <> line) f <> + -- show arguments doc let argshow = showArgs args [] in - if not (null argshow) + (if not (null argshow) then nest 4 $ text "Arguments:" <$> vsep argshow - else empty) + else empty) <> + -- show totality status + let totality = getTotality in + (if totalityFlag && not (null totality) then + line <> (vsep . map (\t -> text "The function is" <+> t) $ totality) + else + empty)) where ppo = ppOptionIst ist infixes = idris_infixes ist @@ -87,15 +96,21 @@ pprintFD ist (FD n doc args ty f) showArgs args ((n, True):bnd) showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd) showArgs [] _ = [] + getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist) +pprintFDWithTotality :: IState -> FunDoc -> Doc OutputAnnotation +pprintFDWithTotality ist = pprintFD ist True + +pprintFDWithoutTotality :: IState -> FunDoc -> Doc OutputAnnotation +pprintFDWithoutTotality ist = pprintFD ist False pprintDocs :: IState -> Docs -> Doc OutputAnnotation -pprintDocs ist (FunDoc d) = pprintFD ist d +pprintDocs ist (FunDoc d) = pprintFDWithTotality ist d pprintDocs ist (DataDoc t args) - = text "Data type" <+> pprintFD ist t <$> + = text "Data type" <+> pprintFDWithoutTotality ist t <$> if null args then text "No constructors." else nest 4 (text "Constructors:" <> line <> - vsep (map (pprintFD ist) args)) + vsep (map (pprintFDWithoutTotality ist) args)) pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor) = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <> if nullDocstring doc @@ -105,12 +120,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct nest 4 (text "Parameters:" <$> prettyParameters) <> line <$> nest 4 (text "Methods:" <$> - vsep (map (pprintFD ist) meths)) + vsep (map (pprintFDWithTotality ist) meths)) <$> maybe empty ((<> line) . nest 4 . (text "Instance constructor:" <$>) . - pprintFD ist) + pprintFDWithoutTotality ist) ctor <> nest 4 (text "Instances:" <$> @@ -195,7 +210,7 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct else hsep (punctuate comma (map (prettyName True False params' . fst) params)) pprintDocs ist (NamedInstanceDoc _cls doc) - = nest 4 (text "Named instance:" <$> pprintFD ist doc) + = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist doc) pprintDocs ist (ModDoc mod docs) = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$> From 164c4f6a27b5e7ddd3fba886966f8724f6f7d50b Mon Sep 17 00:00:00 2001 From: Guglielmo Fachini Date: Sat, 13 Jun 2015 16:10:25 +0200 Subject: [PATCH 2/6] Update REPL :doc related tests with totality status --- test/classes001/expected | 2 ++ test/docs001/expected | 1 + test/docs002/expected | 3 +++ test/docs003/expected | 1 + test/docs004/expected | 3 +++ test/interactive005/expected | 3 +++ 6 files changed, 13 insertions(+) diff --git a/test/classes001/expected b/test/classes001/expected index 5e9fb93aa..fd93c1a7b 100644 --- a/test/classes001/expected +++ b/test/classes001/expected @@ -8,6 +8,7 @@ Methods: myShow : MyShow a => (x : a) -> String The shower + The function is Total Instance constructor: MkMyShow : (myShow : a -> String) -> MyShow a Build a MyShow @@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a myShow : a -> String -- The shower + The function is Total diff --git a/test/docs001/expected b/test/docs001/expected index 1490b0db5..1588a6165 100644 --- a/test/docs001/expected +++ b/test/docs001/expected @@ -8,6 +8,7 @@ Methods: m : C t => t member of class + The function is Total Instances: C A instance of class diff --git a/test/docs002/expected b/test/docs002/expected index faa922a90..1ac43e6c1 100644 --- a/test/docs002/expected +++ b/test/docs002/expected @@ -1,9 +1,12 @@ T1 : Type Some documentation + The function is Total T2 : Type Some other documentation + The function is Total T3 : Int Some provided postulate + The function is not yet checked for totality diff --git a/test/docs003/expected b/test/docs003/expected index 66d96cb18..0b94f27cb 100644 --- a/test/docs003/expected +++ b/test/docs003/expected @@ -8,6 +8,7 @@ Methods: map : Functor f => (m : a -> b) -> f a -> f b The action of the functor on morphisms + The function is Total Instances: Functor List Functor Stream diff --git a/test/docs004/expected b/test/docs004/expected index 8d844c7ef..cbdc29aed 100644 --- a/test/docs004/expected +++ b/test/docs004/expected @@ -7,9 +7,12 @@ MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a baz : Bool -- A field baz + The function is Total bar : (rec : Foo a) -> Nat A field bar + The function is Total baz : (rec : Foo a) -> Bool A field baz + The function is Total diff --git a/test/interactive005/expected b/test/interactive005/expected index fd3fca115..aba629e54 100644 --- a/test/interactive005/expected +++ b/test/interactive005/expected @@ -3,6 +3,7 @@ Hello, World main : IO () This is a docstring + The function is Total Main.main is Total Hello, World Prelude.Basics.id : a -> a @@ -26,8 +27,10 @@ main : IO () is a docstring + The function is Total main : IO () This is a docstring + The function is Total Nat2 : Type Invalid filename for compiler output "Test.idr" From 36f37df7ffdd74a4e3bcb41e82065056c99457be Mon Sep 17 00:00:00 2001 From: Thomas Cooper Date: Sat, 13 Jun 2015 17:48:42 +0100 Subject: [PATCH 3/6] Fixed minor inconsistency in function definitions --- docs/tutorial/typesfuns.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/tutorial/typesfuns.rst b/docs/tutorial/typesfuns.rst index 7adee95ea..ed4a653de 100644 --- a/docs/tutorial/typesfuns.rst +++ b/docs/tutorial/typesfuns.rst @@ -268,8 +268,8 @@ can be used to calculate a return type: .. code-block:: idris mkSingle : (x : Bool) -> isSingleton x - mkSingle False = 0 - mkSingle True = [] + mkSingle True = 0 + mkSingle False = [] Or it can be used to have varying input types. The following function calculates 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 .. code-block:: idris sum : (single : Bool) -> isSingleton single -> Nat - sum False x = x - sum True [] = 0 - sum True (x :: xs) = x + sum True xs + sum True x = x + sum False [] = 0 + sum False (x :: xs) = x + sum False xs Vectors ------- From 66870b20396a02ad1c50c77c68cc0ad8224d5e13 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 10 Jun 2015 11:54:36 +0100 Subject: [PATCH 4/6] Export 'lift' from Control.Monad.State --- libs/base/Control/Monad/State.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/base/Control/Monad/State.idr b/libs/base/Control/Monad/State.idr index 02dc1cc07..0b63b9b16 100644 --- a/libs/base/Control/Monad/State.idr +++ b/libs/base/Control/Monad/State.idr @@ -1,7 +1,7 @@ module Control.Monad.State import public Control.Monad.Identity -import Control.Monad.Trans +import public Control.Monad.Trans %access public From f224681a7c560ecd97463bab197b18547ee1b8c9 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 14 Jun 2015 12:04:33 +0100 Subject: [PATCH 5/6] Update FAQ Differences with Agda question was somewhat out of date. --- docs/faq/faq.rst | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/docs/faq/faq.rst b/docs/faq/faq.rst index 18b24dee6..0f63ce56e 100644 --- a/docs/faq/faq.rst +++ b/docs/faq/faq.rst @@ -5,13 +5,17 @@ Frequently Asked Questions What are the differences between Agda and Idris? ================================================ -The main difference is that Idris has been designed from the start to support -verified systems programming through easy interoperability with C and high -level language constructs to support domain specific language implementation. -Idris emphasises general-purpose programming, rather than theorem proving, and -as such includes higher level programming constructs such as type classes and -do notation. Idris also supports tactic based theorem proving, and has a -lightweight Hugs/GHCI style interface. +Like Idris, Agda is a functional language with dependent types, supporting +dependent pattern matching. Both can be used for writing programs and proofs. +However, Idris has been designed from the start to emphasise general purpose +programming rather than theorem proving. As such, it supports interoperability +with systems libraries and C programs, and language constructs for +domain specific language implementation. It also includes higher level +programming constructs such as type classes and do notation. + +Idris supports multiple back ends (C and JavaScript by default, with the +ability to add more via plugins) and has a reference run time system, written +in C, with a garbage collector and built-in message passing concurrency. Is Idris production ready? ========================== From a21064e77efe3993c32ca9a20d0636599a57624f Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 14 Jun 2015 13:54:14 +0100 Subject: [PATCH 6/6] Add Effect.Monad and Effect.Trans These allow Eff programs to be used in monad transformer stacks, either by wrapping them in MonadEff (which is a monad wrapping programs with unchanging effects) or by using the TRANS effect to allow lifting of programs in some inner monad. --- libs/effects/Effect/Monad.idr | 31 +++++++++++++++++++------------ libs/effects/Effect/Trans.idr | 20 ++++++++++++++++++++ libs/effects/effects.ipkg | 4 ++-- 3 files changed, 41 insertions(+), 14 deletions(-) create mode 100644 libs/effects/Effect/Trans.idr diff --git a/libs/effects/Effect/Monad.idr b/libs/effects/Effect/Monad.idr index 8b67c8f95..6160c9e89 100644 --- a/libs/effects/Effect/Monad.idr +++ b/libs/effects/Effect/Monad.idr @@ -2,20 +2,27 @@ module Effect.Monad import Effects --- Eff is a monad too, so we can happily use it in a monad transformer. +data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where + MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a -using (xs : List EFFECT, m : Type -> Type) - instance Functor (\a => EffM m a xs (\v => xs)) where - map f prog = do t <- prog - value (f t) +instance Functor (MonadEffT xs f) where + map f (MkMonadEffT x) = MkMonadEffT (do x' <- x + pure (f x')) - instance Applicative (\a => EffM m a xs (\v => xs)) where - pure = value - (<*>) f a = do f' <- f - a' <- a - value (f' a') +instance Applicative (MonadEffT xs f) where + pure x = MkMonadEffT (pure x) + (<*>) (MkMonadEffT f) (MkMonadEffT x) + = MkMonadEffT (do f' <- f + x' <- x + pure (f' x')) - instance Monad (\a => Eff m a xs (\v => xs)) where - (>>=) = Effects.(>>=) +instance Monad (MonadEffT xs f) where + (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x + let MkMonadEffT fx = f x' + fx) +implicit monadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a +monadEffT = MkMonadEffT +MonadEff : List EFFECT -> Type -> Type +MonadEff xs = MonadEffT xs id diff --git a/libs/effects/Effect/Trans.idr b/libs/effects/Effect/Trans.idr new file mode 100644 index 000000000..eb8ba157d --- /dev/null +++ b/libs/effects/Effect/Trans.idr @@ -0,0 +1,20 @@ +module Effect.Trans + +import Effects + +%access public + +data Trans : (Type -> Type) -> Effect where + Lift : m a -> sig (Trans m) a + +-- using (m : Type -> Type) +instance Monad m => Handler (Trans m) m where + handle st (Lift op) k = do x <- op + k x () + +TRANS : (Type -> Type) -> EFFECT +TRANS m = MkEff () (Trans m) + +lift : m a -> Eff a [TRANS m] +lift op = call $ Lift op + diff --git a/libs/effects/effects.ipkg b/libs/effects/effects.ipkg index de99976c5..4fcc97bbd 100644 --- a/libs/effects/effects.ipkg +++ b/libs/effects/effects.ipkg @@ -1,9 +1,9 @@ package effects opts = "--nobasepkgs -i ../prelude -i ../base" -modules = Effects, Effect.Default, +modules = Effects, Effect.Default, Effect.Monad, Effect.Exception, Effect.File, Effect.State, Effect.Random, Effect.StdIO, Effect.Select, - Effect.Memory, Effect.System + Effect.Memory, Effect.System, Effect.Trans