From ca576542bac5efceb35e9e5a52af56174b25f77c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 19 Jan 2024 10:53:43 +0100 Subject: [PATCH] whitelist generalizing and says. #173 --- server/GameServer/FileWorker.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 6ca86c3..c25910f 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -97,9 +97,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) for arg in args do findForbiddenTactics inputCtx gameWorkerState arg | .atom info val => - -- ignore syntax elements that do not start with a letter - -- and ignore "with" keyword - let allowed := ["with", "fun", "at", "only", "by", "to"] + -- Whitelisted keywords. + -- Note: We need a whitelist because we cannot really distinguish keywords from tactics. + let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"] + -- ignore syntax elements that do not start with a letter or are allowed if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` match levelInfo.tactics.find? (·.name.toString == val) with