From 405971990d725cf8b6fe9ff746a25727221b65cb Mon Sep 17 00:00:00 2001
From: KonjacSource <1435771606@qq.com>
Date: Sat, 5 Oct 2024 18:54:45 +0800
Subject: [PATCH] Mutual Recursion, Ready to do termination check

---
 Draft.shitt                | 16 +++++++++++++
 README.md                  | 24 +++++++++++++++++++-
 WithoutKTest.shitt         |  2 +-
 src/ShiTT/CheckFunction.hs |  1 -
 src/ShiTT/Parser.hs        | 46 +++++++++++++++++++++++++++++++++-----
 5 files changed, 81 insertions(+), 8 deletions(-)

diff --git a/Draft.shitt b/Draft.shitt
index f10f65a..cae47ff 100644
--- a/Draft.shitt
+++ b/Draft.shitt
@@ -91,3 +91,19 @@ data Void : U where
 
 fun nomatchTest (n : N) (_: Id (succ (succ n)) (succ n)) : N where 
 | n k !@ k
+
+
+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
diff --git a/README.md b/README.md
index a9dc8a2..4791321 100644
--- a/README.md
+++ b/README.md
@@ -34,6 +34,7 @@ ghci> run "Eaxmple.shitt"
 - [x] [Syntax Highlight](https://github.com/KonjacSource/shitt-highlight)
 - [x] REPL
 - [x] Module system (very naive)
+- [x] Mutual recursion
 
 ## TODO
 
@@ -45,7 +46,7 @@ ghci> run "Eaxmple.shitt"
 - [ ] IO
 - [ ] Code generator
 - [ ] Type classes
-- [ ] Mutual recursion
+- [ ] Better Module system
 
 ## Use REPL
 
@@ -175,6 +176,27 @@ fun invf {A B : U} (f : A -> B) (y : B) (_ : Imf f y) : A where
 
 Here `y` is restricted by `imf x`.
 
+### Mutual Recursion
+
+Only mutual functions for now. The syntax is pretty Pascal style.
+
+```haskell
+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
+```
+
 ### ~~HIT~~
 
 ```haskell
diff --git a/WithoutKTest.shitt b/WithoutKTest.shitt
index 0bfde7e..37d2ede 100644
--- a/WithoutKTest.shitt
+++ b/WithoutKTest.shitt
@@ -13,7 +13,7 @@ fun K {A : U} {a : A} (P : Id a a -> U) (p : P (refl _)) (e : Id a a) : P e wher
 
 -- OK
 fun J {A : U} {a : A} (P : (b : A) -> Id a b -> U) (p : P a (refl _)) (b : A) (e : Id a b) : P b e 
-| P p a (refl _) = p 
+| P p b (refl _) = p 
 
 -- not OK
 fun K1 {A : U} {a : A} (P : Id a a -> U) (p : P (refl _)) (e : Id a a) : P e where 
diff --git a/src/ShiTT/CheckFunction.hs b/src/ShiTT/CheckFunction.hs
index f3543f8..32a2f04 100644
--- a/src/ShiTT/CheckFunction.hs
+++ b/src/ShiTT/CheckFunction.hs
@@ -13,7 +13,6 @@ import Control.Monad (forM, when, join, guard)
 import Data.Maybe (fromJust, isJust, isNothing)
 import ShiTT.Meta
 import Data.IORef (readIORef)
-import Data.Foldable (forM_)
 import Debug.Trace (trace)
 import Control.Applicative (Alternative(empty))
 import Data.List (nub)
diff --git a/src/ShiTT/Parser.hs b/src/ShiTT/Parser.hs
index 2917828..15f165a 100644
--- a/src/ShiTT/Parser.hs
+++ b/src/ShiTT/Parser.hs
@@ -115,7 +115,7 @@ keywords =  [ "U", "let", "in", "fun", "λ"
             , "data", "where", "def", "fun"
             , "nomatch", "auto", "traceContext"
             , "inductive", "higher", "when"
-            , "unmatchable", "axiom" ]
+            , "unmatchable", "axiom", "mutual", "begin", "end" ]
 
 pIdent :: Parser Name
 pIdent = do
@@ -559,11 +559,10 @@ putLn = liftIO . putStrLn
 checkFunction :: Parser () 
 checkFunction = do
     isAxiom <- (symbol "axiom" >> pure True) <|> pure False
-    let checker = checkFun
     fun <- pFun 
     ctx <- getCtx
     pos <- getSourcePos
-    checked_fun <- liftIO $ checker ctx (not isAxiom) fun 
+    checked_fun <- liftIO $ checkFun ctx (not isAxiom) fun 
       `catch` \e -> putStrLn ("In function " ++ fun.funName ++ ":" ++ sourcePosPretty pos) >> case e of  
         PMErr pm -> error (show pm)
         UnifyE u v -> error ("(PatternMatch) Can't unify " ++ show u ++ " with " ++ show v) 
@@ -572,11 +571,48 @@ checkFunction = do
         ConflictName n -> error $ "Don't use the name: " ++ n
     addFun checked_fun
 
+pMutualBody :: [D.Fun] -> Parser ()
+pMutualBody [] = pure ()
+pMutualBody header = do 
+  fun_name <- symbol "fun" >> pIdent 
+  let lookup :: [D.Fun] -> [D.Fun] -> Maybe (D.Fun, [D.Fun])
+      lookup _ [] = Nothing 
+      lookup fore (f:fs)
+        | f.funName == fun_name = Just (f, fore ++ fs)
+        | otherwise = lookup (fore ++ [f]) fs
+  case lookup [] header of 
+    Nothing -> error $ "The funcion " ++ fun_name ++ " should not define in mutual block."
+    Just (fun_header, rest_headers) -> do  
+
+      clauses <- many (pClause (D.funPara fun_header))
+      let raw_fun = fun_header { D.clauses = clauses }
+      ctx <- getCtx
+      pos <- getSourcePos
+      checked_fun <- liftIO $ checkFun ctx True raw_fun 
+        `catch` \e -> putStrLn ("In function " ++ raw_fun.funName ++ ":" ++ sourcePosPretty pos) >> case e of  
+          PMErr pm -> error (show pm)
+          UnifyE u v -> error ("(PatternMatch) Can't unify " ++ show u ++ " with " ++ show v) 
+          UsedK -> error "Are you using K?"
+          BoundaryMismatch fun_name sp -> error "Boundary Mismatch."
+          ConflictName n -> error $ "Don't use the name: " ++ n
+      addFun checked_fun
+      pMutualBody rest_headers
+
 pMutual :: Parser () 
-pMutual = undefined
+pMutual = do 
+  raw_headers <- symbol "mutual" >> many pFunHeader <* symbol "begin"
+  let mkFun fun = Fun
+        { funName = fun.funName
+        , funPara = fun.funPara
+        , funRetType = fun.funRetType
+        , funClauses = Nothing
+        }
+  let headers = mkFun <$> raw_headers
+  mapM_ addFun headers
+  pMutualBody raw_headers <* symbol "end"  
 
 pTopLevel :: Parser () 
-pTopLevel = choice [data_type, checkFunction, command] where 
+pTopLevel = choice [data_type, checkFunction, pMutual, command] where 
 
   data_type = do 
     dat <- pData