Merge pull request #1073 from david-christiansen/docs

More docstrings

libs/base/Data/BoundedList.idr

@@ -3,10 +3,12 @@ module Data.BoundedList
 %access public
 %default total
 
+||| A list with an upper bound on its length.
 data BoundedList : Type -> Nat -> Type where
   Nil : BoundedList a n
   (::) : a -> BoundedList a n -> BoundedList a (S n)
 
+||| Compute the length of a list.
 length : BoundedList a n -> Fin (S n)
 length [] = fZ
 length (x :: xs) = fS (length xs)
@@ -24,6 +26,7 @@ index (fS f) (_ :: xs) = index f xs
 -- Adjusting bounds
 --------------------------------------------------------------------------------
 
+||| Loosen the bounds on a list's length.
 weaken : BoundedList a n -> BoundedList a (n + m)
 weaken []        = []
 weaken (x :: xs) = x :: weaken xs
@@ -77,6 +80,7 @@ map f (x :: xs) = f x :: map f xs
 -- Misc
 --------------------------------------------------------------------------------
 
+||| Extend a bounded list to the maximum size by padding on the left.
 pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
 pad {n=Z}    []        _       = []
 pad {n=S n'} []        padding = padding :: (pad {n=n'} [] padding)

libs/base/Data/HVect.idr

@@ -6,7 +6,8 @@ import Data.Vect
 %default total
 
 using (k : Nat, ts : Vect k Type)
-  ||| Heterogeneous vectors where the type index gives, element-wise, the types of the contents
+  ||| Heterogeneous vectors where the type index gives, element-wise,
+  ||| the types of the contents.
   data HVect : Vect k Type -> Type where
     Nil : HVect []
     (::) : t -> HVect ts -> HVect (t::ts)
@@ -30,6 +31,7 @@ using (k : Nat, ts : Vect k Type)
   updateAt fZ f (x::xs) = f x :: xs
   updateAt (fS j) f (x::xs) = x :: updateAt j f xs
 
+  ||| Append two `HVect`s.
   (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
   (++) [] ys = ys
   (++) (x::xs) ys = x :: (xs ++ ys)
@@ -52,16 +54,18 @@ using (k : Nat, ts : Vect k Type)
   instance (Shows k ts) => Show (HVect ts) where
     show xs = show (shows xs)
 
-  ||| Extract an arbitrary element of the correct type
+  ||| Extract an arbitrary element of the correct type.
   ||| @ t the goal type
   get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
   get {p = Here} (x::xs) = x
   get {p = There p'} (x::xs) = get {p = p'} xs
 
+  ||| Replace an element with the correct type.
   put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
   put {p = Here} y (x::xs) = y :: xs
   put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
 
+  ||| Replace an element with the correct type.
   update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
   update {p = Here} f (x::xs) = f x :: xs
   update {p = There p'} f (x::xs) = x :: update {p = p'} f xs

libs/effects/Effect/StdIO.idr

@@ -3,12 +3,22 @@ module Effect.StdIO
 import Effects
 import Control.IOExcept
 
+-------------------------------------------------------------
+-- IO effects internals
+-------------------------------------------------------------
+
+||| The internal representation of StdIO effects
 data StdIO : Effect where
      PutStr : String -> { () } StdIO () 
      GetStr : { () } StdIO String 
      PutCh : Char -> { () } StdIO ()
      GetCh : { () } StdIO Char
 
+
+-------------------------------------------------------------
+-- IO effects handlers
+-------------------------------------------------------------
+
 instance Handler StdIO IO where
     handle () (PutStr s) k = do putStr s; k () ()
     handle () GetStr     k = do x <- getLine; k x ()
@@ -21,23 +31,30 @@ instance Handler StdIO (IOExcept a) where
     handle () (PutCh c)  k = do ioe_lift $ putChar c; k () () 
     handle () GetCh      k = do x <- ioe_lift $ getChar; k x ()
 
+-------------------------------------------------------------
 --- The Effect and associated functions
+-------------------------------------------------------------
 
 STDIO : EFFECT
 STDIO = MkEff () StdIO
 
+||| Write a string to standard output.
 putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
 putStr s = PutStr s
 
+||| Write a character to standard output.
 putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
 putChar c = PutCh c
 
+||| Write a string to standard output, terminating with a newline.
 putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
 putStrLn s = putStr (s ++ "\n")
 
+||| Read a string from standard input.
 getStr : Handler StdIO e => { [STDIO] } Eff e String
 getStr = GetStr
 
+||| Read a character from standard input.
 getChar : Handler StdIO e => { [STDIO] } Eff e Char
 getChar = GetCh
 

libs/prelude/Builtins.idr

@@ -17,6 +17,7 @@ getWitness (a ** v) = a
 getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
 getProof (a ** v) = v
 
+||| The eliminator for the empty type.
 FalseElim : _|_ -> a
 
 ||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
@@ -43,17 +44,35 @@ lazy x = x -- compiled specially
 force : a -> a
 force x = x -- compiled specially
 
+||| There are two types of laziness: that arising from lazy functions, and that
+||| arising from codata. They differ in their totality condition.
 data LazyType = LazyCodata | LazyEval
 
+||| The underlying implementation of Lazy and Inf.
 data Lazy' : LazyType -> Type -> Type where
+     ||| A delayed computation.
+     |||
+     |||Delay is inserted automatically by the elaborator where necessary.
+     |||
+     ||| Note that compiled code gives `Delay` special semantics.
+     ||| @ t   whether this is laziness from codata or normal lazy evaluation
+     ||| @ a   the type of the eventual value
+     ||| @ val a computation that will produce a value
      Delay : {t, a : _} -> (val : a) -> Lazy' t a
 
+||| Compute a value from a delayed computation.
+|||
+||| Inserted by the elaborator where necessary.
 Force : {t, a : _} -> Lazy' t a -> a
 Force (Delay x) = x
 
+||| Lazily evaluated values. This has special evaluation semantics.
 Lazy : Type -> Type
 Lazy t = Lazy' LazyEval t
 
+||| Recursive parameters to codata. Inserted automatically by the elaborator
+||| on a "codata" definition but is necessary by hand if mixing inductive and
+||| coinductive parameters.
 Inf : Type -> Type
 Inf t = Lazy' LazyCodata t
 

libs/prelude/Prelude/Fin.idr

@@ -6,7 +6,10 @@ import Prelude.Uninhabited
 
 %default total
 
-||| Numbers strictly less than some bound.  The name comes from "finite sets"
+||| Numbers strictly less than some bound.  The name comes from "finite sets".
+|||
+||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
+||| exceedingly inefficient at run time.
 ||| @ n the upper bound
 data Fin : (n : Nat) -> Type where
     fZ : Fin (S k)
@@ -24,16 +27,19 @@ instance Eq (Fin n) where
     (==) (fS k) (fS k') = k == k'
     (==) _ _ = False
 
+||| There are no elements of `Fin Z`
 FinZAbsurd : Fin Z -> _|_
 FinZAbsurd fZ impossible
 
 FinZElim : Fin Z -> a
 FinZElim x = FalseElim (FinZAbsurd x)
 
+||| Convert a Fin to a Nat
 finToNat : Fin n -> Nat
 finToNat fZ = Z
 finToNat (fS k) = S (finToNat k)
 
+||| `finToNat` is injective
 finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
 finToNatInjective fZ     fZ     refl = refl
 finToNatInjective (fS m) fZ     refl impossible
@@ -44,6 +50,7 @@ finToNatInjective (fS m) (fS n) prf  =
 instance Cast (Fin n) Nat where
     cast x = finToNat x
 
+||| Convert a Fin to an Integer
 finToInteger : Fin n -> Integer
 finToInteger fZ     = 0
 finToInteger (fS k) = 1 + finToInteger k
@@ -123,9 +130,13 @@ natToFin _ _ = Nothing
 integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
 integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
 
+||| Proof that some `Maybe` is actually `Just`
 data IsJust : Maybe a -> Type where
   ItIsJust : IsJust {a} (Just x)
 
+||| Allow overloading of Integer literals for Fin.
+||| @ x the Integer that the user typed
+||| @ prf an automatically-constructed proof that `x` is in bounds
 fromInteger : (x : Integer) ->
               {default ItIsJust
                prf : (IsJust (integerToFin x n))} ->