mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-18 03:40:28 +03:00
prevent recursive holes (check condition 3)
This commit is contained in:
parent
057c8d51de
commit
9cbaf6c4d5
@ -1,6 +1,6 @@
|
|||||||
use Equal.{refl}
|
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 {
|
match e {
|
||||||
refl: {=}
|
refl: {=}
|
||||||
}
|
}
|
||||||
|
@ -1,10 +1,10 @@
|
|||||||
use Nat.{succ,zero,half,double}
|
use Nat.{succ,zero,half,double}
|
||||||
|
|
||||||
bft (n: Nat) : (Equal Nat (half (double n)) n) =
|
bft (n: Nat) : {(half (double n)) = n} =
|
||||||
match n {
|
match n {
|
||||||
succ:
|
succ:
|
||||||
let ind = (bft n.pred)
|
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
|
prf
|
||||||
zero: {=}
|
zero: {=}
|
||||||
}
|
}
|
||||||
|
30
src/kind2.hs
30
src/kind2.hs
@ -473,8 +473,7 @@ termIdenticalGo a b dep =
|
|||||||
-- ?X = λx λy λz ... K
|
-- ?X = λx λy λz ... K
|
||||||
-- In this implementation, checking condition `2` is not necessary, because we
|
-- In this implementation, checking condition `2` is not necessary, because we
|
||||||
-- subst holes directly where they occur (rather than on top-level definitions),
|
-- 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
|
-- so, it is impossible for unbound variables to appear.
|
||||||
-- condition 3, and just allow recursive solutions.
|
|
||||||
|
|
||||||
-- If possible, solves a `(?X x y z ...) = K` problem, generating a subst.
|
-- If possible, solves a `(?X x y z ...) = K` problem, generating a subst.
|
||||||
termUnify :: Int -> [Term] -> Term -> Int -> Env Bool
|
termUnify :: Int -> [Term] -> Term -> Int -> Env Bool
|
||||||
@ -482,13 +481,15 @@ termUnify uid spn b dep = do
|
|||||||
fill <- envGetFill
|
fill <- envGetFill
|
||||||
let unsolved = not (mapHas (key uid) fill)
|
let unsolved = not (mapHas (key uid) fill)
|
||||||
let solvable = termUnifyValid fill spn []
|
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
|
let solution = termUnifySolve fill uid spn b
|
||||||
-- trace ("solve: " ++ show uid ++ " " ++ termShow solution dep) $ do
|
-- trace ("solve: " ++ show uid ++ " " ++ termShow solution dep) $ do
|
||||||
envFill uid solution
|
envFill uid solution
|
||||||
return True
|
return True
|
||||||
else
|
else case b of
|
||||||
return False
|
(Met bUid bSpn) -> return $ uid == bUid
|
||||||
|
other -> return $ False
|
||||||
|
|
||||||
-- Checks if an problem is solveable by pattern unification.
|
-- Checks if an problem is solveable by pattern unification.
|
||||||
termUnifyValid :: Map Term -> [Term] -> [Int] -> Bool
|
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)
|
(Var nam idx) -> Lam nam $ \x -> termUnifySubst idx x (termUnifySolve fill uid spn b)
|
||||||
otherwise -> error "unreachable"
|
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`.
|
-- Substitutes a Bruijn level variable by a `neo` value in `term`.
|
||||||
termUnifySubst :: Int -> Term -> Term -> Term
|
termUnifySubst :: Int -> Term -> Term -> Term
|
||||||
-- termUnifySubst lvl neo term = term
|
-- termUnifySubst lvl neo term = term
|
||||||
|
Loading…
Reference in New Issue
Block a user