Termination Check!

README.md

@@ -35,11 +35,11 @@ ghci> run "Eaxmple.shitt"
 - [x] REPL
 - [x] Module system (very naive)
 - [x] Mutual recursion
+- [x] Termination checking
 
 ## TODO
 
 - [ ] Operators
-- [ ] Termination checking
 - [ ] Universe polymorphism
 - [ ] Positive checking for data types
 - [ ] Better pretty printing
@@ -301,6 +301,69 @@ fun addComm (x y : N) : Id (add x y) (add y x) where
 
 `traceContext` will print the context definitions and the goal type (if it is not a metavariable) while type checking. Also note that `traceContext[x] = x`
 
+### Termination Check
+
+ShiTT does check termination. You can use `partial` to shut it down.
+
+```haskell
+data Bool : U where 
+| true : ... 
+| false : ...
+
+data N : U where  
+| zero : ...  
+| succ : (pre : N) -> ...  
+
+mutual
+
+  fun even (_ : N) : Bool
+  fun odd  (_ : N) : Bool
+
+begin
+
+  fun even
+  | zero = true
+  | (succ n) = odd n
+
+  fun odd 
+  | zero = false
+  | (succ n) = even n
+
+end
+
+fun add (_ _ : N) : N 
+| zero n = n 
+| (succ m) n = succ (add m n) 
+
+-- Bad
+fun add1 (_ _ : N) : N 
+| m n = add1 m n
+
+-- Good again
+partial fun add1 (_ _ : N) : N 
+| m n = add1 m n
+
+-- This is also good!
+fun add2 (_ _ : N) : N 
+| x zero = x 
+| x (succ y) = succ (add2 y x)
+
+data Vec (A : U) : (_ : N) -> U where 
+| nil : ... zero 
+| cons : {n : N} (_ : A) (_ : Vec A n) -> ... (succ n)
+
+
+
+fun append {A : U} {m n : N} (v : Vec A m) (w : Vec A n) : Vec A (add m n)
+| nil w = w 
+| (cons x xs) w = cons x (append xs w)
+
+-- Bad
+fun append1 {A : U} {m n : N} (v : Vec A m) (w : Vec A n) : Vec A (add m n)
+| nil w = w 
+| (cons x xs) w = (append (cons x xs) w)
+```
+
 ## Example
 
 The following example shows the basic syntax and how to do some simple theorem proof (remember we have no termination check yet).

src/ShiTT/CheckFunction.hs

@@ -10,11 +10,9 @@ import qualified Data.Map as M
 import ShiTT.Syntax
 import Control.Exception
 import Control.Monad (forM, when, join, guard)
-import Data.Maybe (fromJust, isJust, isNothing)
+import Data.Maybe (fromJust, isNothing)
 import ShiTT.Meta
 import Data.IORef (readIORef)
-import Debug.Trace (trace)
-import Control.Applicative (Alternative(empty))
 import Data.List (nub)
 
 

src/ShiTT/Context.hs

@@ -8,7 +8,6 @@ import qualified Data.Map as M
 import Text.Megaparsec (SourcePos)
 import Control.Monad (join)
 import Data.List (nub)
-import Debug.Trace (trace)
 
 -- Value
 ----------------------------------

src/ShiTT/Parser.hs

@@ -22,7 +22,6 @@ import Control.Exception hiding (try)
 import ShiTT.Meta (allSolved, reset, withoutKRef, allUnmatchableTypes)
 import Data.List (dropWhileEnd)
 import System.IO
-import Debug.Trace (trace)
 import ShiTT.Termination.Call (MutualSet)
 import qualified Data.Set as S
 import ShiTT.Termination.Check

src/ShiTT/Termination/Check.hs

@@ -2,7 +2,6 @@ module ShiTT.Termination.Check where
 
 import ShiTT.Termination.Call
 import ShiTT.Context
-import Debug.Trace (trace)
 
 -- | The given context should contain the fake definitions (which means only fun header) of mutual functions.
 checkTermination :: Context -> MutualSet -> Bool

src/Test.hs

@@ -3,19 +3,19 @@
 {-# OPTIONS_GHC -Wno-type-defaults #-}
 -- {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 module Test where 
-import ShiTT.Syntax
-import ShiTT.Eval
-import ShiTT.Context
-
-import qualified ShiTT.Decl as R 
--- import qualified ShiTT.Inductive as I
--- import ShiTT.Decl (Pattern(PVar, PCon))
-import ShiTT.Meta
-import Control.Monad (forM_)
--- import ShiTT.Inductive (splitCase)
-import ShiTT.TermParser as TP
-import ShiTT.TermParser (readTerm)
-import ShiTT.Check (infer)
+-- import ShiTT.Syntax
+-- import ShiTT.Eval
+-- import ShiTT.Context
+
+-- import qualified ShiTT.Decl as R 
+-- -- import qualified ShiTT.Inductive as I
+-- -- import ShiTT.Decl (Pattern(PVar, PCon))
+-- import ShiTT.Meta
+-- import Control.Monad (forM_)
+-- -- import ShiTT.Inductive (splitCase)
+-- import ShiTT.TermParser as TP
+-- import ShiTT.TermParser (readTerm)
+-- import ShiTT.Check (infer)
 
 -- natData :: Data
 -- natData = Data