Merge github.com:idris-lang/Idris2 into caseofcase

CHANGELOG.md

@@ -22,6 +22,8 @@ Syntax changes:
 
 Compiler changes:
 
+* Added more optimisations and transformations, particularly on case blocks,
+  and on list-shaped types, so generated code will often be slightly faster.
 * Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in
   order to not block the Racket runtime when `sleep` is called.
 * Added `--profile` flag, which generates profile data if supported by a back

docs/source/tutorial/interfaces.rst

@@ -721,6 +721,25 @@ do this with a ``using`` clause in the implementation as follows:
 The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
 extend ``PlusNatSemi`` specifically.
 
+.. _InterfaceConstructors:
+
+Interface Constructors
+======================
+
+Interfaces, just like records, can be declared with a user-defined constructor.
+
+.. code-block:: idris
+
+    interface A a where
+      getA : a
+
+    interface A t => B t where
+      constructor MkB
+
+      getB : t
+
+Then ``MkB : A t => t -> B t``.
+
 .. _DeterminingParameters:
 
 Determining Parameters

libs/prelude/Builtin.idr

@@ -207,6 +207,7 @@ force x = Force x
 ||| Interface for types that can be constructed from string literals.
 public export
 interface FromString ty where
+  constructor MkFromString
   ||| Conversion from String.
   fromString : String -> ty
 

libs/prelude/Prelude/Cast.idr

@@ -14,6 +14,7 @@ import Prelude.Types
 ||| Interface for transforming an instance of a data type to another type.
 public export
 interface Cast from to where
+  constructor MkCast
   ||| Perform a (potentially lossy!) cast operation.
   ||| @ orig The original type
   cast : (orig : from) -> to

libs/prelude/Prelude/EqOrd.idr

@@ -13,6 +13,7 @@ import Prelude.Ops
 ||| The Eq interface defines inequality and equality.
 public export
 interface Eq ty where
+  constructor MkEq
   (==) : ty -> ty -> Bool
   (/=) : ty -> ty -> Bool
 
@@ -86,6 +87,7 @@ Eq Ordering where
 ||| The Ord interface defines comparison operations on ordered data types.
 public export
 interface Eq ty => Ord ty where
+  constructor MkOrd
   compare : ty -> ty -> Ordering
 
   (<) : ty -> ty -> Bool

libs/prelude/Prelude/IO.idr

@@ -32,10 +32,12 @@ Monad IO where
 
 public export
 interface Monad io => HasIO io where
+  constructor MkHasIO
   liftIO : IO a -> io a
 
 public export
 interface Monad io => HasLinearIO io where
+  constructor MkHasLinearIO
   liftIO1 : (1 _ : IO a) -> io a
 
 public export %inline

libs/prelude/Prelude/Interfaces.idr

@@ -19,6 +19,7 @@ import Prelude.Ops
 |||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
 public export
 interface Semigroup ty where
+  constructor MkSemigroup
   (<+>) : ty -> ty -> ty
 
 ||| Sets equipped with a single binary operation that is associative, along with
@@ -32,6 +33,7 @@ interface Semigroup ty where
 |||     forall a, neutral <+> a == a
 public export
 interface Semigroup ty => Monoid ty where
+  constructor MkMonoid
   neutral : ty
 
 public export
@@ -68,6 +70,7 @@ Monoid b => Monoid (a -> b) where
 ||| @ f a parameterised type
 public export
 interface Functor f where
+  constructor MkFunctor
   ||| Apply a function across everything of type 'a' in a parameterised type
   ||| @ f the parameterised type
   ||| @ func the function to apply
@@ -114,6 +117,7 @@ namespace Functor
 ||| @f The action of the Bifunctor on pairs of objects
 public export
 interface Bifunctor f where
+  constructor MkBifunctor
   ||| The action of the Bifunctor on pairs of morphisms
   |||
   ||| ````idris example
@@ -147,6 +151,7 @@ mapHom f = bimap f f
 
 public export
 interface Functor f => Applicative f where
+  constructor MkApplicative
   pure : a -> f a
   (<*>) : f (a -> b) -> f a -> f b
 
@@ -172,11 +177,13 @@ namespace Applicative
 
 public export
 interface Applicative f => Alternative f where
+  constructor MkAlternative
   empty : f a
   (<|>) : f a -> Lazy (f a) -> f a
 
 public export
 interface Applicative m => Monad m where
+  constructor MkMonad
   ||| Also called `bind`.
   (>>=) : m a -> (a -> m b) -> m b
 
@@ -230,6 +237,7 @@ when False f = pure ()
 ||| @ t The type of the 'Foldable' parameterised type.
 public export
 interface Foldable t where
+  constructor MkFoldable
   ||| Successively combine the elements in a parameterised type using the
   ||| provided function, starting with the element that is in the final position
   ||| i.e. the right-most position.
@@ -385,6 +393,7 @@ namespace Foldable
 ||| Common examples are `Either` and `Pair`.
 public export
 interface Bifoldable p where
+  constructor MkBifoldable
   bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc
 
   bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc
@@ -395,6 +404,7 @@ interface Bifoldable p where
 
 public export
 interface (Functor t, Foldable t) => Traversable t where
+  constructor MkTraversable
   ||| Map each element of a structure to a computation, evaluate those
   ||| computations and combine the results.
   traverse : Applicative f => (a -> f b) -> t a -> f (t b)
@@ -411,6 +421,7 @@ for = flip traverse
 
 public export
 interface (Bifunctor p, Bifoldable p) => Bitraversable p where
+  constructor MkBitraversable
   ||| Map each element of a structure to a computation, evaluate those
   ||| computations and combine the results.
   bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)

libs/prelude/Prelude/Num.idr

@@ -16,6 +16,7 @@ import Prelude.Ops
 ||| The Num interface defines basic numerical arithmetic.
 public export
 interface Num ty where
+  constructor MkNum
   (+) : ty -> ty -> ty
   (*) : ty -> ty -> ty
   ||| Conversion from Integer.
@@ -26,6 +27,7 @@ interface Num ty where
 ||| The `Neg` interface defines operations on numbers which can be negative.
 public export
 interface Num ty => Neg ty where
+  constructor MkNeg
   ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
   negate : ty -> ty
   (-) : ty -> ty -> ty
@@ -33,11 +35,13 @@ interface Num ty => Neg ty where
 ||| Numbers for which the absolute value is defined should implement `Abs`.
 public export
 interface Num ty => Abs ty where
+  constructor MkAbs
   ||| Absolute value.
   abs : ty -> ty
 
 public export
 interface Num ty => Fractional ty where
+  constructor MkFractional
   partial
   (/) : ty -> ty -> ty
   partial
@@ -47,6 +51,7 @@ interface Num ty => Fractional ty where
 
 public export
 interface Num ty => Integral ty where
+  constructor MkIntegral
   partial
   div : ty -> ty -> ty
   partial

libs/prelude/Prelude/Show.idr

@@ -41,6 +41,7 @@ Ord Prec where
 ||| Things that have a canonical `String` representation.
 public export
 interface Show ty where
+  constructor MkShow
   ||| Convert a value to its `String` representation.
   ||| @ x the value to convert
   show : (x : ty) -> String

libs/prelude/Prelude/Types.idr

@@ -781,6 +781,7 @@ takeBefore p (x :: xs)
 
 public export
 interface Range a where
+  constructor MkRange
   rangeFromTo : a -> a -> List a
   rangeFromThenTo : a -> a -> a -> List a
 

libs/prelude/Prelude/Uninhabited.idr

@@ -8,6 +8,7 @@ import Prelude.Basics
 ||| A canonical proof that some type is empty.
 public export
 interface Uninhabited t where
+  constructor MkUninhabited
   ||| If I have a t, I've had a contradiction.
   ||| @ t the uninhabited type
   uninhabited : t -> Void

src/Idris/Doc/HTML.idr

@@ -80,12 +80,23 @@ renderHtml (STAnn ann rest) = do
   pure $ "<!-- ann ignored START -->" ++ resthtml ++ "<!-- ann END -->"
 renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs)
 
+removeNewlinesFromDeclarations : SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
+removeNewlinesFromDeclarations = go False
+  where
+    go : Bool -> SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
+    go False l@(STLine i) = l
+    go True l@(STLine i) = STEmpty
+    go ignoring (STConcat docs) = STConcat $ map (go ignoring) docs
+    go _ (STAnn Declarations rest) = STAnn Declarations $ go True rest
+    go _ (STAnn ann rest) = STAnn ann $ go False rest
+    go _ doc = doc
+
 docDocToHtml : {auto c : Ref Ctxt Defs} ->
                Doc IdrisDocAnn ->
                Core String
 docDocToHtml doc =
   let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in
-      renderHtml dt
+      renderHtml $ removeNewlinesFromDeclarations dt
 
 htmlPreamble : String -> String -> String -> String
 htmlPreamble title root class = "<!DOCTYPE html><html lang=\"en\"><head><meta charset=\"utf-8\">"

src/Idris/DocString.idr

@@ -145,18 +145,21 @@ getDocsForName fc n
       let root = nameRoot n in
       if isOpName n then parens (pretty root) else pretty root
 
-    getDConDoc : Name -> Core (List (Doc IdrisDocAnn))
+    getDConDoc : Name -> Core (Doc IdrisDocAnn)
     getDConDoc con
         = do defs <- get Ctxt
              Just def <- lookupCtxtExact con (gamma defs)
-                  | Nothing => pure []
+                  -- should never happen, since we know that the DCon exists:
+                  | Nothing => pure Empty
              syn <- get Syn
-             let [(n, str)] = lookupName con (docstrings syn)
-                  | _ => pure []
              ty <- resugar [] =<< normaliseHoles defs [] (type def)
-             pure $ pure $ vcat $
-               annotate (Decl con) (hsep [dCon (prettyName n), colon, prettyTerm ty])
-               :: reflowDoc str
+             let conWithTypeDoc = annotate (Decl con) (hsep [dCon (prettyName con), colon, prettyTerm ty])
+             let [(n, str)] = lookupName con (docstrings syn)
+                  | _ => pure conWithTypeDoc
+             pure $ vcat
+               [ conWithTypeDoc
+               , annotate DocStringBody $ vcat $ reflowDoc str
+               ]
 
     getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
     getImplDoc n
@@ -242,7 +245,7 @@ getDocsForName fc n
                TCon _ _ _ _ _ _ cons _
                    => do let tot = [showTotal n (totality d)]
                          cdocs <- traverse (getDConDoc <=< toFullNames) cons
-                         let cdoc = case concat cdocs of
+                         let cdoc = case cdocs of
                               [] => []
                               [doc] => [header "Constructor" <++> annotate Declarations doc]
                               docs => [vcat [header "Constructors"

src/Idris/Package.idr

@@ -655,6 +655,7 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
     optType (DumpVMCode f)   = POpt
     optType DebugElabCheck   = POpt
     optType (SetCG f)        = POpt
+    optType (Directive d)    = POpt
     optType (BuildDir f)     = POpt
     optType (OutputDir f)    = POpt
     optType (ConsoleWidth n) = PIgnore
@@ -682,6 +683,7 @@ errorMsg = unlines
   , "    --dumpvmcode <file>"
   , "    --debug-elab-check"
   , "    --codegen <cg>"
+  , "    --directive <directive>"
   , "    --build-dir <dir>"
   , "    --output-dir <dir>"
   ]

src/Idris/Pretty/Render.idr

@@ -9,6 +9,8 @@ import Libraries.Text.PrettyPrint.Prettyprinter
 import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
 import Libraries.Utils.Term
 
+import System
+
 getPageWidth : {auto o : Ref ROpts REPLOpts} -> Core PageWidth
 getPageWidth = do
   consoleWidth <- getConsoleWidth
@@ -25,11 +27,16 @@ render : {auto o : Ref ROpts REPLOpts} ->
          Doc ann -> Core String
 render stylerAnn doc = do
   color <- getColor
+  isDumb <- (Just "dumb" ==) <$> coreLift (getEnv "TERM")
+  -- ^-- emacs sets the TERM variable to `dumb` and expects the compiler
+  --     to not emit any ANSI escape codes
   pageWidth <- getPageWidth
   let opts = MkLayoutOptions pageWidth
   let layout = layoutPretty opts doc
   pure $ renderString $
-    if color then reAnnotateS stylerAnn layout else unAnnotateS layout
+    if color && not isDumb
+      then reAnnotateS stylerAnn layout
+      else unAnnotateS layout
 
 export
 renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc ann -> Core String

support/docs/styles.css

@@ -94,7 +94,7 @@ p {
 }
 
 .decls {
-  margin-top: 15px;
+  margin-top: 5px;
 }
 
 .decls > dt {
@@ -111,7 +111,7 @@ p {
 }
 
 .decls > dd {
-  margin: 10px 0 10px 20px;
+  margin: 10px 0 20px 20px;
   font-family: Arial, sans-serif;
   font-size: 10pt;
 }

tests/codegen/con001/expected

@@ -2,21 +2,21 @@ Dumping case trees to Main.cases
 prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
 prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
 prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
-Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
+Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.MkFoldable Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con Builtin.MkPair Just 0 [(%con Prelude.Num.MkIntegral Just 0 [(%con Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.MkOrd Just 0 [(%con Prelude.EqOrd.MkEq Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.MkNeg Just 0 [(%con Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
 Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
 Builtin.snd = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
 Builtin.idris_crash = [{ext:N}]: (crash [___, !{ext:N}])
 Builtin.fst = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
 Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
-Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))])])), (%constcase 1 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (%con [nil] Prelude.Types.Nil Just 0 [])]))] Nothing)
-Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
+Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))])])), (%constcase 1 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (%con [nil] Prelude.Types.Nil Just 0 [])]))] Nothing)
+Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
 Prelude.Types.case block in takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (%con [nil] Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [!{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
 Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
-Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
+Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
 Prelude.Types.null = [{arg:N}]: (%case !{arg:N} [(%concase [nil] Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase [cons] Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
 Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase [nil] Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase [cons] Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [!{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
 Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase [nil] Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase [cons] Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [!{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
-Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing))] Nothing), !{ext:N}])
+Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.MkMonad Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case !{arg:N} [(%concase Prelude.Interfaces.MkMonad Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Interfaces.MkApplicative Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing))] Nothing), !{ext:N}])
 Prelude.Types.takeUntil = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [!{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
 Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
 Prelude.Types.countFrom = [{arg:N}, {arg:N}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [(!{arg:N} [!{arg:N}]), !{arg:N}]))])
@@ -39,7 +39,7 @@ Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%co
 Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case (<Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
 Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case (<=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
 Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]) [(%constcase 0 1), (%constcase 1 0)] Nothing)
-Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {eta:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{eta:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
+Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.MkFoldable Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {eta:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{eta:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
 PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
 PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
 PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}

tests/idris2/docs002/Doc.idr

@@ -13,6 +13,16 @@ export
 hello : Int -> Int
 hello x = x*2
 
+public export
+data WrappedInt : Type where
+  MkWrappedInt : Int -> WrappedInt
+
+public export
+record SimpleRec where
+  constructor MkSimpleRec
+  a : Int
+  b : String
+
 namespace NS
 
   namespace NestedNS

tests/idris2/docs002/expected

@@ -1,9 +1,22 @@
 1/1: Building Doc (Doc.idr)
-Doc> hello : Int -> Int
+Doc> MkSimpleRec : Int -> String -> SimpleRec
+MkWrappedInt : Int -> WrappedInt
+SimpleRec : Type
+WrappedInt : Type
+a : SimpleRec -> Int
+b : SimpleRec -> String
+hello : Int -> Int
 	Hello!
 world : Nat -> Nat
 	World!
 Doc> Doc.NS.NestedNS.Foo : Type
   A type of Foo
   
+Doc> Doc.WrappedInt : Type
+  Totality: total
+  Constructor: MkWrappedInt : Int -> WrappedInt
+  
+Doc> Doc.SimpleRec : Type
+  Totality: total
+  Constructor: MkSimpleRec : Int -> String -> SimpleRec
 Doc> Bye for now!

tests/idris2/docs002/input

@@ -1,3 +1,5 @@
 :browse Doc
 :doc Foo
+:doc WrappedInt
+:doc SimpleRec
 :q

tests/idris2/pkg003/expected

@@ -11,6 +11,7 @@ Overridable options are:
     --dumpvmcode <file>
     --debug-elab-check
     --codegen <cg>
+    --directive <directive>
     --build-dir <dir>
     --output-dir <dir>