Permalink
Browse files

Fix silly error in termination checker :)

  • Loading branch information...
1 parent 86c2bee commit 98395627b255c0b213f18c8066e32e90f1232dab Edwin Brady committed Feb 1, 2012
Showing with 52 additions and 4 deletions.
  1. +5 −4 CHANGELOG
  2. +1 −0 src/Idris/Coverage.hs
  3. +17 −0 tutorial/examples/theorems.idr
  4. +1 −0 tutorial/starting.tex
  5. +28 −0 tutorial/theorems.tex
View
9 CHANGELOG
@@ -3,15 +3,16 @@ New in 0.9.1:
User visible changes:
-* dsl notation
-* record projection and update
-* auto implicits and default argument values {auto n : T}, {default val n : T}
+* DSL notation
+* Record projection and update
+* Totality checking and 'total' keyword
+* Auto implicits and default argument values {auto n : T}, {default val n : T}
* Additions to prelude, including Nat and List theorems
* New libs: control.monad.identity, control.monad.state
Internal changes:
-* faster compilation (only compiling names which are used)
+* Faster compilation (only compiling names which are used)
0.1.x to 0.9.0:
View
1 src/Idris/Coverage.hs
@@ -253,6 +253,7 @@ calcTotality path fc n pats
Total _ -> return ords
p@(Partial (Mutual x)) -> return ((Left p) : ords)
_ -> return (Left (Partial (Other [fn])) : ords)
+ | null args = return (Left (Partial Itself) : ords)
chkOrd ords args _ = return ords
lexOrd x y | x == y = LexEQ
View
17 tutorial/examples/theorems.idr
@@ -5,6 +5,23 @@ fiveIsFive = refl
twoPlusTwo : 2 + 2 = 4
twoPlusTwo = refl
+total imp : (n : Nat) -> O = S n -> _|_
+imp n p = replace {P = impTy} p ()
+ where
+ impTy : Nat -> Set
+ impTy O = ()
+ impTy (S k) = _|_
+
+empty1 : _|_
+empty1 = let xs : List _|_ = [] in hd xs
+ where
+ hd : List a -> a
+ hd (x :: xs) = x
+
+
+empty2 : _|_
+empty2 = empty2
+
plusReduces : (n:Nat) -> plus O n = n
plusReduces n = refl
View
1 tutorial/starting.tex
@@ -109,6 +109,7 @@ \subsection{The interactive environment}
<expr> Evaluate an expression
:t <expr> Check the type of an expression
+ :total <name> Check the totality of a name
:r :reload Reload current file
:e :edit Edit current file using $EDITOR or $VISUAL
:m :metavars Show remaining proof obligations (metavariables)
View
28 tutorial/theorems.tex
@@ -29,6 +29,34 @@ \subsection{Equality}
\end{SaveVerbatim}
\useverb{eqprf}
+\subsection{The Empty Type}
+
+There is an empty type, \texttt{\_|\_}, which has no constructors. It is
+therefore impossible to construct an element of the empty type, at least
+without using a partially defined or general recursive function (see Section
+\ref{sect:totality} for more details). We can therefore use the empty type
+to prove that something is impossible, for example zero is never equal
+to a successor:
+
+\begin{SaveVerbatim}{natdisjoint}
+
+imp : (n : Nat) -> O = S n -> _|_
+imp n p = replace {P = impTy} p ()
+ where
+ impTy : Nat -> Set
+ impTy O = ()
+ impTy (S k) = _|_
+
+\end{SaveVerbatim}
+\useverb{natdisjoint}
+
+\noindent
+There is no need to worry too much about how this function works --- essentially,
+it applies the library function \texttt{replace}, which uses an equality proof to
+transform a predicate. Here we use it to transform a value of a type which can exist,
+the empty tuple, to a value of a type which can't, by using a proof of something
+which can't exist.
+
\subsection{Simple Theorems}
When type checking dependent types, the type itself gets \emph{normalised}. So imagine

0 comments on commit 9839562

Please sign in to comment.