From db4c5e7fbb2749c7e224242fdb0930bcc5eba1a9 Mon Sep 17 00:00:00 2001 From: Justus Matthiesen Date: Thu, 9 Nov 2023 13:59:53 +0000 Subject: [PATCH] Cleanup of `sizeEq` (#3138) --- src/Core/Termination/CallGraph.idr | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr index 99abe3549..e79432ed2 100644 --- a/src/Core/Termination/CallGraph.idr +++ b/src/Core/Termination/CallGraph.idr @@ -20,14 +20,15 @@ Show Guardedness where show Guarded = "Guarded" show InDelay = "InDelay" -sizeEq : Term vars -> -- RHS - Term vars -> -- LHS: may contain dot-patterns, try both sides of as patterns - Bool +sizeEq : {auto 0 cv : CompatibleVars rhsVars lhsVars} -> + Term rhsVars -> -- RHS + Term lhsVars -> -- LHS: may contain dot-patterns, try both sides of as patterns + Bool sizeEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx' sizeEq (Ref _ _ n) (Ref _ _ n') = n == n' sizeEq (Meta _ _ i args) (Meta _ _ i' args') = i == i' && assert_total (all (uncurry sizeEq) (zip args args')) -sizeEq (Bind _ _ b sc) (Bind _ _ b' sc') = eqBinderBy sizeEq b b' && sizeEq sc (believe_me sc') +sizeEq (Bind _ _ b sc) (Bind _ _ b' sc') = eqBinderBy sizeEq b b' && sizeEq sc sc' sizeEq (App _ f a) (App _ f' a') = sizeEq f f' && sizeEq a a' sizeEq (As _ _ a p) p' = sizeEq p p' sizeEq p (As _ _ a p') = sizeEq p a || sizeEq p p' @@ -36,8 +37,7 @@ sizeEq (TDelay _ _ t x) (TDelay _ _ t' x') = sizeEq t t' && sizeEq x x' sizeEq (TForce _ _ t) (TForce _ _ t') = sizeEq t t' sizeEq (PrimVal _ c) (PrimVal _ c') = c == c' -- traverse dotted LHS terms -sizeEq t (Erased _ (Dotted t')) = sizeEq t t' -sizeEq (Erased _ i) (Erased _ i') = i == i' +sizeEq t (Erased _ (Dotted t')) = believe_me t == t' -- t' is no longer a pattern sizeEq (TType _ _) (TType _ _) = True sizeEq _ _ = False