From 9cbaf6c4d5f08294bf5d5f74493ef6aabb5a9739 Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Thu, 14 Mar 2024 12:10:05 -0300
Subject: [PATCH] prevent recursive holes (check condition 3)

---
 book/Equal.apply.kind2   |  2 +-
 book/Nat.lemma.bft.kind2 |  4 ++--
 src/kind2.hs             | 30 +++++++++++++++++++++++++-----
 3 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/book/Equal.apply.kind2 b/book/Equal.apply.kind2
index 1d2ab0f8..4a00c766 100644
--- a/book/Equal.apply.kind2
+++ b/book/Equal.apply.kind2
@@ -1,6 +1,6 @@
 use Equal.{refl}
 
-apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
+apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: {a = b}) : {(f a) = (f b)} =
   match e {
     refl: {=}
   }
diff --git a/book/Nat.lemma.bft.kind2 b/book/Nat.lemma.bft.kind2
index 14c4a879..12c454c3 100644
--- a/book/Nat.lemma.bft.kind2
+++ b/book/Nat.lemma.bft.kind2
@@ -1,10 +1,10 @@
 use Nat.{succ,zero,half,double}
 
-bft (n: Nat) : (Equal Nat (half (double n)) n) =
+bft (n: Nat) : {(half (double n)) = n} =
   match n {
     succ:
       let ind = (bft n.pred)
-      let prf = (Equal.apply Nat Nat succ (half (double n.pred)) n.pred ind)
+      let prf = (Equal.apply _ _ succ _ _ ind)
       prf
     zero: {=}
   }
diff --git a/src/kind2.hs b/src/kind2.hs
index da166cd1..d3529755 100644
--- a/src/kind2.hs
+++ b/src/kind2.hs
@@ -473,8 +473,7 @@ termIdenticalGo a b dep =
 --   ?X = λx λy λz ... K
 -- In this implementation, checking condition `2` is not necessary, because we
 -- subst holes directly where they occur (rather than on top-level definitions),
--- so, it is impossible for unbound variables to appear. We also don't check for
--- condition 3, and just allow recursive solutions.
+-- so, it is impossible for unbound variables to appear.
 
 -- If possible, solves a `(?X x y z ...) = K` problem, generating a subst.
 termUnify :: Int -> [Term] -> Term -> Int -> Env Bool
@@ -482,13 +481,15 @@ termUnify uid spn b dep = do
   fill <- envGetFill
   let unsolved = not (mapHas (key uid) fill)
   let solvable = termUnifyValid fill spn []
-  if unsolved && solvable then do
+  let no_loops = not $ termUnifyIsRec fill uid b dep
+  if unsolved && solvable && no_loops then do
     let solution = termUnifySolve fill uid spn b
     -- trace ("solve: " ++ show uid ++ " " ++ termShow solution dep) $ do
     envFill uid solution
     return True
-  else
-    return False
+  else case b of
+    (Met bUid bSpn) -> return $ uid == bUid
+    other           -> return $ False
 
 -- Checks if an problem is solveable by pattern unification.
 termUnifyValid :: Map Term -> [Term] -> [Int] -> Bool
@@ -504,6 +505,25 @@ termUnifySolve fill uid (x : spn) b = case termReduce fill 0 x of
   (Var nam idx) -> Lam nam $ \x -> termUnifySubst idx x (termUnifySolve fill uid spn b)
   otherwise     -> error "unreachable"         
 
+-- Checks if a hole uid occurs recursively inside a term
+termUnifyIsRec :: Map Term -> Int -> Term -> Int -> Bool
+termUnifyIsRec fill uid (All nam inp bod) dep = termUnifyIsRec fill uid inp dep || termUnifyIsRec fill uid (bod (Var nam dep)) (dep + 1)
+termUnifyIsRec fill uid (Lam nam bod)     dep = termUnifyIsRec fill uid (bod (Var nam dep)) (dep + 1)
+termUnifyIsRec fill uid (App fun arg)     dep = termUnifyIsRec fill uid fun dep || termUnifyIsRec fill uid arg dep
+termUnifyIsRec fill uid (Ann chk val typ) dep = termUnifyIsRec fill uid val dep || termUnifyIsRec fill uid typ dep
+termUnifyIsRec fill uid (Slf nam typ bod) dep = termUnifyIsRec fill uid typ dep || termUnifyIsRec fill uid (bod (Var nam dep)) (dep + 1)
+termUnifyIsRec fill uid (Ins val)         dep = termUnifyIsRec fill uid val dep
+termUnifyIsRec fill uid (Let nam val bod) dep = termUnifyIsRec fill uid val dep || termUnifyIsRec fill uid (bod (Var nam dep)) (dep + 1)
+termUnifyIsRec fill uid (Use nam val bod) dep = termUnifyIsRec fill uid val dep || termUnifyIsRec fill uid (bod (Var nam dep)) (dep + 1)
+termUnifyIsRec fill uid (Hol nam ctx)     dep = False
+termUnifyIsRec fill uid (Op2 opr fst snd) dep = termUnifyIsRec fill uid fst dep || termUnifyIsRec fill uid snd dep
+termUnifyIsRec fill uid (Mat nam x z s p) dep = termUnifyIsRec fill uid x dep || termUnifyIsRec fill uid z dep || termUnifyIsRec fill uid (s (Var (stringConcat nam "-1") dep)) (dep + 1) || termUnifyIsRec fill uid (p (Var nam dep)) dep
+termUnifyIsRec fill uid (Src src val)     dep = termUnifyIsRec fill uid val dep
+termUnifyIsRec fill uid (Met bUid bSpn)   dep = case termReduceMet fill 2 bUid bSpn of
+  (Met bUid bSpn) -> uid == bUid
+  term            -> termUnifyIsRec fill uid term dep
+termUnifyIsRec fill uid _                 dep = False
+
 -- Substitutes a Bruijn level variable by a `neo` value in `term`.
 termUnifySubst :: Int -> Term -> Term -> Term
 -- termUnifySubst lvl neo term = term