print warning for unsolved metas

HigherOrderCO · Oct 18, 2024 · e93bc53 · e93bc53
1 parent 50e7760
commit e93bc53
Show file tree

Hide file tree

Showing 2 changed files with 83 additions and 65 deletions.
diff --git a/src/Kind/API.hs b/src/Kind/API.hs
@@ -1,3 +1,5 @@
+-- //./Type.hs//
+
 module Kind.API where
 
 import Control.Monad (forM, forM_, foldM)
@@ -89,10 +91,12 @@ apiCheckFile book defs path = do
     case envRun (doCheck term) book of
       Done state value -> do
         apiPrintLogs state
+        apiPrintWarn term state
         putStrLn $ "\x1b[32m✓ " ++ name ++ "\x1b[0m"
         return $ Right ()
       Fail state -> do
         apiPrintLogs state
+        apiPrintWarn term state
         putStrLn $ "\x1b[31m✗ " ++ name ++ "\x1b[0m"
         return $ Left $ "Error."
   putStrLn ""
@@ -147,11 +151,21 @@ apiToJS book name = do
 
 -- Prints logs from the type-checker
 apiPrintLogs :: State -> IO ()
-apiPrintLogs (State book fill susp logs) =
+apiPrintLogs (State book fill susp logs) = do
   forM_ logs $ \log -> do
     result <- infoShow book fill log
     putStrLn result
 
+-- Prints a warning if there are unsolved metas
+apiPrintWarn :: Term -> State -> IO ()
+apiPrintWarn term (State _ fill _ _) = do
+  let metaCount = countMetas term
+  let fillCount = IM.size fill
+  if (metaCount > fillCount) then do
+    putStrLn $ "WARNING: " ++ show (metaCount - fillCount) ++ " unsolved metas."
+  else
+    return ()
+
 -- Gets dependencies of a term
 getDeps :: Term -> [String]
 getDeps term = case term of

diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs
@@ -255,68 +255,72 @@ bind (Src src val) ctx =
   Src src val'
 
 genMetas :: Term -> Term
-genMetas term = fst (go term 0) where
-  go :: Term -> Int -> (Term, Int)
-  go (All nam inp bod) c = 
-    let (inp', c1) = go inp c
-        (bod', c2) = go (bod (Var nam 0)) c1
-    in (All nam inp' (\_ -> bod'), c2)
-  go (Lam nam bod) c = 
-    let (bod', c1) = go (bod (Var nam 0)) c
-    in (Lam nam (\_ -> bod'), c1)
-  go (App fun arg) c = 
-    let (fun', c1) = go fun c
-        (arg', c2) = go arg c1
-    in (App fun' arg', c2)
-  go (Ann chk val typ) c = 
-    let (val', c1) = go val c
-        (typ', c2) = go typ c1
-    in (Ann chk val' typ', c2)
-  go (Slf nam typ bod) c = 
-    let (typ', c1) = go typ c
-        (bod', c2) = go (bod (Var nam 0)) c1
-    in (Slf nam typ' (\_ -> bod'), c2)
-  go (Ins val) c = 
-    let (val', c1) = go val c
-    in (Ins val', c1)
-  go (Dat scp cts) c = 
-    let (scp', c1) = foldr (\t (acc, c') -> let (t', c'') = go t c' in (t':acc, c'')) ([], c) scp
-        (cts', c2) = foldr (\(Ctr nm tele) (acc, c') -> let (tele', c'') = goTele tele c' in (Ctr nm tele' : acc, c'')) ([], c1) cts
-    in (Dat scp' cts', c2)
-  go (Con nam arg) c = 
-    let (arg', c1) = foldr (\(f, t) (acc, c') -> let (t', c'') = go t c' in ((f, t'):acc, c'')) ([], c) arg
-    in (Con nam arg', c1)
-  go (Mat cse) c = 
-    let (cse', c1) = foldr (\(cn, cb) (acc, c') -> let (cb', c'') = go cb c' in ((cn, cb'):acc, c'')) ([], c) cse
-    in (Mat cse', c1)
-  go (Swi zer suc) c = 
-    let (zer', c1) = go zer c
-        (suc', c2) = go suc c1
-    in (Swi zer' suc', c2)
-  go (Let nam val bod) c = 
-    let (val', c1) = go val c
-        (bod', c2) = go (bod (Var nam 0)) c1
-    in (Let nam val' (\_ -> bod'), c2)
-  go (Use nam val bod) c = 
-    let (val', c1) = go val c
-        (bod', c2) = go (bod (Var nam 0)) c1
-    in (Use nam val' (\_ -> bod'), c2)
-  go (Met _ spn) c = 
-    let (spn', c1) = foldr (\t (acc, c') -> let (t', c'') = go t c' in (t':acc, c'')) ([], c) spn
-    in (Met c1 spn', c1 + 1)
-  go (Hol nam ctx) c = 
-    let (ctx', c1) = foldr (\t (acc, c') -> let (t', c'') = go t c' in (t':acc, c'')) ([], c) ctx
-    in (Hol nam ctx', c1)
-  go (Src src val) c = 
-    let (val', c1) = go val c
-    in (Src src val', c1)
-  go term c = (term, c)
+genMetas term = fst (genMetasGo term 0)
 
-  goTele :: Tele -> Int -> (Tele, Int)
-  goTele (TRet term) c = 
-    let (term', c1) = go term c
-    in (TRet term', c1)
-  goTele (TExt nam typ bod) c = 
-    let (typ', c1) = go typ c
-        (bod', c2) = goTele (bod (Var nam 0)) c1
-    in (TExt nam typ' (\_ -> bod'), c2)
+genMetasGo :: Term -> Int -> (Term, Int)
+genMetasGo (All nam inp bod) c = 
+  let (inp', c1) = genMetasGo inp c
+      (bod', c2) = genMetasGo (bod (Var nam 0)) c1
+  in (All nam inp' (\_ -> bod'), c2)
+genMetasGo (Lam nam bod) c = 
+  let (bod', c1) = genMetasGo (bod (Var nam 0)) c
+  in (Lam nam (\_ -> bod'), c1)
+genMetasGo (App fun arg) c = 
+  let (fun', c1) = genMetasGo fun c
+      (arg', c2) = genMetasGo arg c1
+  in (App fun' arg', c2)
+genMetasGo (Ann chk val typ) c = 
+  let (val', c1) = genMetasGo val c
+      (typ', c2) = genMetasGo typ c1
+  in (Ann chk val' typ', c2)
+genMetasGo (Slf nam typ bod) c = 
+  let (typ', c1) = genMetasGo typ c
+      (bod', c2) = genMetasGo (bod (Var nam 0)) c1
+  in (Slf nam typ' (\_ -> bod'), c2)
+genMetasGo (Ins val) c = 
+  let (val', c1) = genMetasGo val c
+  in (Ins val', c1)
+genMetasGo (Dat scp cts) c = 
+  let (scp', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) scp
+      (cts', c2) = foldr (\(Ctr nm tele) (acc, c') -> let (tele', c'') = genMetasGoTele tele c' in (Ctr nm tele' : acc, c'')) ([], c1) cts
+  in (Dat scp' cts', c2)
+genMetasGo (Con nam arg) c = 
+  let (arg', c1) = foldr (\(f, t) (acc, c') -> let (t', c'') = genMetasGo t c' in ((f, t'):acc, c'')) ([], c) arg
+  in (Con nam arg', c1)
+genMetasGo (Mat cse) c = 
+  let (cse', c1) = foldr (\(cn, cb) (acc, c') -> let (cb', c'') = genMetasGo cb c' in ((cn, cb'):acc, c'')) ([], c) cse
+  in (Mat cse', c1)
+genMetasGo (Swi zer suc) c = 
+  let (zer', c1) = genMetasGo zer c
+      (suc', c2) = genMetasGo suc c1
+  in (Swi zer' suc', c2)
+genMetasGo (Let nam val bod) c = 
+  let (val', c1) = genMetasGo val c
+      (bod', c2) = genMetasGo (bod (Var nam 0)) c1
+  in (Let nam val' (\_ -> bod'), c2)
+genMetasGo (Use nam val bod) c = 
+  let (val', c1) = genMetasGo val c
+      (bod', c2) = genMetasGo (bod (Var nam 0)) c1
+  in (Use nam val' (\_ -> bod'), c2)
+genMetasGo (Met _ spn) c = 
+  let (spn', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) spn
+  in (Met c1 spn', c1 + 1)
+genMetasGo (Hol nam ctx) c = 
+  let (ctx', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) ctx
+  in (Hol nam ctx', c1)
+genMetasGo (Src src val) c = 
+  let (val', c1) = genMetasGo val c
+  in (Src src val', c1)
+genMetasGo term c = (term, c)
+
+genMetasGoTele :: Tele -> Int -> (Tele, Int)
+genMetasGoTele (TRet term) c = 
+  let (term', c1) = genMetasGo term c
+  in (TRet term', c1)
+genMetasGoTele (TExt nam typ bod) c = 
+  let (typ', c1) = genMetasGo typ c
+      (bod', c2) = genMetasGoTele (bod (Var nam 0)) c1
+  in (TExt nam typ' (\_ -> bod'), c2)
+
+countMetas :: Term -> Int
+countMetas term = snd (genMetasGo term 0)