Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical

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?
 ==========================

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

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
 

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

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
+

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
 

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

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

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

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

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

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

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"