minor stuff

HigherOrderCO · Oct 18, 2024 · 2849686 · 2849686
1 parent c6bb75b
commit 2849686
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 5 deletions.
diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs
@@ -289,10 +289,12 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
       envFail
 
 unreachable :: Maybe Cod -> Term -> Int -> Env ()
-unreachable src (Lam nam bod) dep = unreachable src (bod (Con "void" [])) (dep+1)
-unreachable src (Hol nam ctx) dep = envLog (Found nam (Hol "unreachable" []) ctx dep) >> return ()
-unreachable _   (Src src val) dep = unreachable (Just src) val dep
-unreachable src term          dep = return ()
+unreachable src (Lam nam bod)     dep = unreachable src (bod (Con "void" [])) (dep+1)
+unreachable src (Hol nam ctx)     dep = envLog (Found nam (Hol "unreachable" []) ctx dep) >> return ()
+unreachable src (Let nam val bod) dep = unreachable src (bod (Con "void" [])) (dep+1)
+unreachable src (Use nam val bod) dep = unreachable src (bod (Con "void" [])) (dep+1)
+unreachable _   (Src src val)     dep = unreachable (Just src) val dep
+unreachable src term              dep = return ()
 
 checkTele :: Maybe Cod -> Tele -> Term -> Int -> Env ()
 checkTele src tele typ dep = case tele of

diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs
@@ -6,6 +6,7 @@ import Debug.Trace
 import Prelude hiding (EQ, LT, GT)
 import Kind.Type
 import Kind.Reduce
+import Kind.Show
 import Highlight (highlightError, highlight)
 import Data.Char (ord)
 import qualified Data.Map.Strict as M
@@ -585,7 +586,8 @@ parseDef = do
         body <- parseTerm
         return (pats, body)
       let (mat, bods) = unzip rules
-      return (flattenDef mat bods 0)
+      let flat = (flattenDef mat bods 0)
+      return $ {-trace (termShow flat)-} flat
     ]
   (_, uses) <- P.getState
   let name' = expandUses uses name