without k

README-zh.md

@@ -34,7 +34,7 @@ ghci> run "Eaxmple.shitt"
 - [x] 元变量求解和隐式变量
 - [x] 代数数据类型和模式匹配
 - [x] 模式完全性检查
-- [x] (可选的)无K的模式匹配(Weak K 目前没有排除)
+- [x] 无K的模式匹配
 - [ ] 运算符
 - [ ] 停机检查
 - [ ] 归纳类型的极性检查

README.md

@@ -27,7 +27,7 @@ ghci> run "Eaxmple.shitt"
 - [x] Meta variables and implict arugments (pattern unification)
 - [x] Pattern matching and data type
 - [x] Coverage checking
-- [x] (Optional) Withou K (but Weak K still works for now)
+- [x] Withou K
 
 ## TODO
 

WithoutKTest.shitt

@@ -21,4 +21,12 @@ fun K1 {A : U} {a : A} (P : Id a a -> U) (p : P (refl _)) (e : Id a a) : P e whe
 
 -- not OK
 fun uip1 {B : U} {x x1 : B} (p q: Id x x1) : Id {Id x x1} p q where 
-| (refl _) (refl _) = refl (refl _)
+| (refl _) (refl _) = refl (refl _)
+
+-- not OK
+fun weakK 
+  {A : U} {a : A} 
+  (P : Id {Id a a} (refl _) (refl _) -> U) 
+  (p : P (refl _)) (e : Id {Id a a} (refl _) (refl _))
+: P e where 
+| P p (refl _) = p

src/ShiTT/Inductive.hs

@@ -14,7 +14,6 @@ import Control.Exception
 import Control.Monad (forM)
 import Data.Maybe (fromJust, isJust, isNothing)
 import ShiTT.Meta 
-import Debug.Trace (trace)
 import Data.IORef (readIORef)
 
 match :: Context -> [Pattern] -> Spine -> Maybe [Def]