phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

whitelist generalizing and says. #173

Browse Source
This commit is contained in:
Jon Eugster
2024-01-19 10:53:43 +01:00
parent fd5e507541
commit ca576542ba
1 changed files with 4 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/FileWorker.lean
+4 -3
View File
@@ -97,9 +97,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
for arg in args do for arg in args do
findForbiddenTactics inputCtx gameWorkerState arg findForbiddenTactics inputCtx gameWorkerState arg
| .atom info val => | .atom info val =>
-- ignore syntax elements that do not start with a letter -- Whitelisted keywords.
-- and ignore "with" keyword -- Note: We need a whitelist because we cannot really distinguish keywords from tactics.
let allowed := ["with", "fun", "at", "only", "by", "to"] 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 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` let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
match levelInfo.tactics.find? (·.name.toString == val) with match levelInfo.tactics.find? (·.name.toString == val) with