From f63f8607eae481306ee4b48d50507a039154dd45 Mon Sep 17 00:00:00 2001
From: KonjacSource <1435771606@qq.com>
Date: Mon, 9 Sep 2024 16:06:01 +0800
Subject: [PATCH] unmatchable, axiom

---
 README-zh.md           |  1 +
 README.md              |  1 +
 Test.shitt             | 33 ++++++++++-----
 src/ShiTT/Inductive.hs | 91 +++++++++++++++++++++++-------------------
 src/ShiTT/Meta.hs      |  9 ++++-
 src/ShiTT/Parser.hs    | 19 +++++++--
 src/Test.hs            |  2 +-
 7 files changed, 97 insertions(+), 59 deletions(-)

diff --git a/README-zh.md b/README-zh.md
index 0dbc393..11c0721 100644
--- a/README-zh.md
+++ b/README-zh.md
@@ -37,6 +37,7 @@ ghci> run "Eaxmple.shitt"
 - [x] 无K的模式匹配
 - [x] [语法高亮](https://github.com/KonjacSource/shitt-highlight)
 - [x] 高阶归纳类型(暂无边界检查)
+- [ ] REPL
 - [ ] 运算符
 - [ ] 停机检查
 - [ ] 归纳类型的极性检查
diff --git a/README.md b/README.md
index 18d5579..7451e67 100644
--- a/README.md
+++ b/README.md
@@ -35,6 +35,7 @@ ghci> run "Eaxmple.shitt"
 
 ## TODO
 
+- [ ] REPL
 - [ ] Operators
 - [ ] Termination checking
 - [ ] Positive checking for data types
diff --git a/Test.shitt b/Test.shitt
index 3c38abd..d9ae95b 100644
--- a/Test.shitt
+++ b/Test.shitt
@@ -1,15 +1,26 @@
-data N : U where  
-| zero : ...  
-| succ : (pre : N) -> ...  
+data Bool : U where 
+| true : ... 
+| false : ...
 
-higher inductive Int : U where 
-| pos : (n : N) -> ... 
-| neg : (n : N) -> ... 
+unmatchable data Interval : U where 
+| i0 : ... 
+| i1 : ...
+
+-- This is ok
+def reflTrue (i : Interval) : Bool 
+| i = true
+
+-- -- This is error
+-- def trueToFalse (i : Interval) : Bool
+-- | i0 = true 
+-- | i1 = false
+
+higher inductive S1 : U where 
+| base : ... 
+| loop : (i : Interval) -> ... 
     when 
-    | zero = pos zero
+    | i0 = base 
+    | i1 = base
 
-#eval neg zero -- pos zero
+#eval loop i0
 
-def abs (n : Int) : N where 
-| pos n = n
-| neg n = n 
diff --git a/src/ShiTT/Inductive.hs b/src/ShiTT/Inductive.hs
index 43286a7..91b6fd7 100644
--- a/src/ShiTT/Inductive.hs
+++ b/src/ShiTT/Inductive.hs
@@ -216,10 +216,11 @@ checkClauses ctx coverChGate fun cls = do
         case t of 
           Left ctx -> pure (p,ctx)
           Right (_,ctx) -> pure (p,ctx)
+
   -- Coverage Check
-  
-  when coverChGate $ 
-    checkCoverage fun.funName fun.funPara patsWithRes (genInitSp ctx fun.funPara)
+  when coverChGate $ do 
+    unmatchables <- readIORef allUnmatchableTypes
+    checkCoverage unmatchables fun.funName fun.funPara patsWithRes (genInitSp ctx fun.funPara)
 
   let rhss' = flip map rhss \case (p, Left _)  -> (p, Nothing) 
                                   (p, Right x) -> (p, Just x)
@@ -240,9 +241,20 @@ checkFun ctx fun = do
                }
   let ctx' =ctx { decls = insertFun preFun ctx.decls }
   val <- checkClauses ctx' True fun fun.clauses 
-
   -- TODO : HIT.Check Boundary
+  pure $ preFun { funVal = val }
+
 
+checkAxiom :: Context -> D.Fun -> IO Fun 
+checkAxiom ctx fun = do 
+  let preFun = Fun 
+               { funName = fun.funName 
+               , funPara = fun.funPara
+               , funRetType = fun.funRetType
+               , funVal = \ _ _ -> Nothing -- A fake definition, so that we may check the type of the definning function
+               }
+  let ctx' =ctx { decls = insertFun preFun ctx.decls }
+  val <- checkClauses ctx' False fun fun.clauses
   pure $ preFun { funVal = val }
 
 unify1 :: NameOrder -> Context -> [Def] -> Value -> Value -> Either CheckError [Def]
@@ -347,15 +359,27 @@ data MatchResult
   deriving Show 
 
 -- | ctx |- rhs, extraDef in ctx.
-splitMatch1 :: Context -> (Name, Icit, VType) -> Pattern -> (Value, Icit) -> MatchResult
-splitMatch1 ctx t p (v, i) | D.icit p == i = case (p, v) of 
+splitMatch1 :: Context -> [Name] -> (Name, Icit, VType) -> Pattern -> (Value, Icit) -> MatchResult
+splitMatch1 ctx unmatchables (_, _, VCon ty_name []) p (v, i) 
+  | D.icit p == i && ty_name `elem` unmatchables
+  = case (p, v) of 
+      (PVar x _, VPatVar v []) 
+        | isInacc ctx x  -> Done [x := VPatVar v []] -- Mark as flexibile
+        | otherwise      -> Done [x := VVar v]
+      (PVar x _, VVar v)  
+        | isInacc ctx x  -> Done [x := VPatVar v []]
+        | otherwise      -> Done [x := VVar v]
+      (PVar x _, v)      -> Done [x := v]
+      _                  -> error "Trying match an unmatchable"
+
+splitMatch1 ctx unmatchables t p (v, i) | D.icit p == i = case (p, v) of 
   (PVar x _, VPatVar v []) 
-    | isInacc ctx x -> Done [x := VPatVar v []] -- Mark as flexibile
-    | otherwise     -> Done [x := VVar v]
-  (PVar x _, VVar v) 
-    | isInacc ctx x -> Done [x := VPatVar v []]
-    | otherwise     -> Done [x := VVar v]
-  (PVar x _, v) -> Done [x := v]
+    | isInacc ctx x  -> Done [x := VPatVar v []] -- Mark as flexibile
+    | otherwise      -> Done [x := VVar v]
+  (PVar x _, VVar v)  
+    | isInacc ctx x  -> Done [x := VPatVar v []]
+    | otherwise      -> Done [x := VVar v]
+  (PVar x _, v)      -> Done [x := v]
   (PCon con_name ps _, VCon con_name' vs) -- note that length ps /= length vs, since vs includes data parameters
     | con_name == con_name' -> 
         -- 1. get data definition and constructor definition
@@ -371,6 +395,7 @@ splitMatch1 ctx t p (v, i) | D.icit p == i = case (p, v) of
         -- 3. try match vs against ps under the modified teles
         in case splitMatch 
                   ctx
+                  unmatchables 
                   teles
                   ps 
                   arg_vs
@@ -392,17 +417,17 @@ splitMatch1 ctx t p (v, i) | D.icit p == i = case (p, v) of
         (_,v,_) <- poss 
         pure [v]
   _ -> error $ "\n\nimpossible : " ++ show ctx ++ show t ++ " | " ++ show p ++ " | " ++ show (v, i) ++ "\n"
-splitMatch1 _ _ _ _ = error "impossible"
+splitMatch1 _ _ _ _ _ = error "impossible"
 
 -- | try match, if stuck, return the pattern with splitted variables.
-splitMatch :: Context -> Telescope -> [Pattern] -> Spine -> MatchResult
-splitMatch ctx ts ps vs = case (ts, ps, vs) of 
+splitMatch :: Context -> [Name] -> Telescope -> [Pattern] -> Spine -> MatchResult
+splitMatch ctx unmatchables ts ps vs = case (ts, ps, vs) of 
   ([], [], []) -> Done []
   (t:ts, p:ps, v:vs) -> 
-    case splitMatch1 ctx t p v of 
+    case splitMatch1 ctx unmatchables t p v of 
       Failed -> Failed 
       -- 
-      Done defs -> case splitMatch (ctx <: defs) ts ps vs of 
+      Done defs -> case splitMatch (ctx <: defs) unmatchables ts ps vs of 
         Failed -> Failed 
         Done defs' -> Done $ defs ++ defs' 
         Stucked poss -> Stucked do 
@@ -416,13 +441,13 @@ splitMatch ctx ts ps vs = case (ts, ps, vs) of
   _ -> error $ "impossible : " ++ show ctx ++ show ts ++ "\n" ++ show ps ++ "\n" ++ show vs 
 
 
-travPattern :: Telescope -> [([Pattern], Context)] -> Spine -> Maybe [Spine]
-travPattern ts [] sp = Just [sp]  -- passed
-travPattern ts pats@((ps,rhs_ctx): rest) sp = case splitMatch rhs_ctx ts ps sp of 
-  Failed -> travPattern ts rest sp 
+travPattern :: [Name] -> Telescope -> [([Pattern], Context)] -> Spine -> Maybe [Spine]
+travPattern unmatchables ts [] sp = Just [sp]  -- passed
+travPattern unmatchables ts pats@((ps,rhs_ctx): rest) sp = case splitMatch rhs_ctx unmatchables ts ps sp of 
+  Failed -> travPattern unmatchables ts rest sp 
   Done _ -> Nothing 
   Stucked new_sps -> 
-    let res = map (travPattern ts pats) new_sps
+    let res = map (travPattern unmatchables ts pats) new_sps
     in  if all isNothing res then 
           Nothing
         else Just do
@@ -431,9 +456,9 @@ travPattern ts pats@((ps,rhs_ctx): rest) sp = case splitMatch rhs_ctx ts ps sp o
             Nothing -> [] 
             Just sp -> sp
 
-checkCoverage :: Name -> Telescope -> [([Pattern], Context)] -> Spine -> IO () 
-checkCoverage fun_name ts ps sp = do 
-  case travPattern ts ps sp of 
+checkCoverage :: [Name] -> Name -> Telescope -> [([Pattern], Context)] -> Spine -> IO () 
+checkCoverage unmatchables fun_name ts ps sp = do 
+  case travPattern unmatchables ts ps sp of 
     Nothing -> pure () 
     Just sp -> putStrLn ("Warning: Missing patterns on function " ++ fun_name ++ "\n" ++ show sp)
 
@@ -482,22 +507,6 @@ checkHData ctx (dat, hcons) = do
     , higherCons = hcons'
     } 
 
-
-{-
-
-data HData = HData 
-  { basePart :: Data 
-  , higherCons :: [HConstructor]
-  } 
-
-data HConstructor = HConstructor 
-  { hconName     :: Name
-  , hconVars     :: [Name]
-  , hconClauses  :: Context -> Spine -> Maybe Value
-  }
-
--}
-
 -- asValue :: [Def] -> Int -> Pattern -> ((Value, Icit), [Def])
 -- asValue fvs nameCount = \case 
 --   PVar x i -> ((VVar x, i), freeVar (freshName (emptyCtx <: fvs) $ '*':show nameCount ++ x) : fvs)
diff --git a/src/ShiTT/Meta.hs b/src/ShiTT/Meta.hs
index e974133..f091183 100644
--- a/src/ShiTT/Meta.hs
+++ b/src/ShiTT/Meta.hs
@@ -5,6 +5,8 @@ import ShiTT.Syntax
 import Data.IORef
 import System.IO.Unsafe
 
+-- Meta Context
+----------------
 data MetaEntry = Unsolved | Solved Value
   deriving Show
 
@@ -45,5 +47,8 @@ allSolved = do
 withoutKRef :: IORef Bool 
 withoutKRef = runIO $ newIORef False 
 
-withoutK :: Bool 
-withoutK = runIO $ readIORef withoutKRef
\ No newline at end of file
+-- Other Global
+---------------
+
+allUnmatchableTypes :: IORef [Name]
+allUnmatchableTypes = runIO $ newIORef []
\ No newline at end of file
diff --git a/src/ShiTT/Parser.hs b/src/ShiTT/Parser.hs
index 0cd6d47..265f112 100644
--- a/src/ShiTT/Parser.hs
+++ b/src/ShiTT/Parser.hs
@@ -23,7 +23,7 @@ import Data.IORef
 import Control.Category ((>>>))
 import Control.Exception hiding (try)
 import Test (testContext2)
-import ShiTT.Meta (allSolved, reset, withoutKRef)
+import ShiTT.Meta (allSolved, reset, withoutKRef, allUnmatchableTypes)
 
 
 type PatVars = [Name]
@@ -118,7 +118,11 @@ inCtx name = do
 
 
 keywords :: [String]
-keywords = ["U", "let", "in", "fun", "λ", "data", "where", "def", "fun", "nomatch", "auto", "traceContext", "inductive", "higher", "when"]
+keywords =  [ "U", "let", "in", "fun", "λ"
+            , "data", "where", "def", "fun"
+            , "nomatch", "auto", "traceContext"
+            , "inductive", "higher", "when"
+            , "unmatchable", "axiom" ]
 
 pIdent :: Parser Name
 pIdent = do
@@ -275,7 +279,12 @@ Each constructor must give all indexes.
 --   Then return the fake definition.
 pDataHeader :: Parser Data
 pDataHeader = do
+  isUnmatchable <- (symbol "unmatchable" >> pure True) <|> pure False 
   data_name <- (symbol "data" <|> symbol "inductive") >> pIdent
+  
+  when isUnmatchable $ do 
+    liftIO $ modifyIORef allUnmatchableTypes (data_name:)
+
   isFresh data_name
   data_para <- pTelescope' -- Adding data parameters to context.
   data_ix <- symbol ":" >> pTelescope 
@@ -581,11 +590,13 @@ pTopLevel = choice [data_type, function, command, hdata_type] where
     hdat <- liftIO $ checkHData ctx dat 
     addHData hdat
 
-  function = do 
+  function = do
+    isAxiom <- (symbol "axiom" >> pure True) <|> pure False
+    let checker = if isAxiom then checkAxiom else checkFun
     fun <- pFun 
     ctx <- getCtx
     pos <- getSourcePos
-    checked_fun <- liftIO $ checkFun ctx fun 
+    checked_fun <- liftIO $ checker ctx 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) 
diff --git a/src/Test.hs b/src/Test.hs
index f57df17..c25fba2 100644
--- a/src/Test.hs
+++ b/src/Test.hs
@@ -392,7 +392,7 @@ splitTest4 = splitCase (testContext <: ("m", natType) :=! VPatVar "m" []) ("v",
 
 --  Context -> (Name, Icit, VType) -> Pattern -> (Value, Icit) -> MatchResult
 
-matchTest1 = I.splitMatch1 testContext2 ("_", Expl, natType) (PCon "zero" [] Expl) (VVar "x" ,Expl)
+matchTest1 = I.splitMatch1 testContext2 [] ("_", Expl, natType) (PCon "zero" [] Expl) (VVar "x" ,Expl)
 
 -- matchTest1 = trace (show ps) $ I.match' (testContext2 <: res.typeLevelDef) rhs_ctx ts ps vs
 --   where