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

cleanup

Browse Source
This commit is contained in:
Jon Eugster
2024-06-18 16:10:54 +02:00
parent 5310e69d98
commit aab6dbb329
1 changed files with 10 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/Commands.lean
+10 -10
View File
@@ -326,15 +326,15 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
"Statement" statementName:ident ? preamble:preambleArg ? sig:declSig val:declVal : command => do "Statement" statementName:ident ? preamble:preambleArg ? sig:declSig val:declVal : command => do
let lvlIdx ← getCurLevelIdx let lvlIdx ← getCurLevelIdx
-- add an optional tactic sequence that the engine executes before the game starts -- Add an optional tactic sequence that the engine executes before the game starts
let preambleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preamble with let preambleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preamble with
| none => `(Parser.Tactic.tacticSeq|skip) | some arg => match arg with
| some x => match x with
| `(preambleArg| (preamble := $tac)) => pure tac | `(preambleArg| (preamble := $tac)) => pure tac
| _ => `(Parser.Tactic.tacticSeq|skip) | _ => `(Parser.Tactic.tacticSeq| skip)
| none => `(Parser.Tactic.tacticSeq| skip)
let docContent ← parseDocComment doc -- Translate the docstring of the `Statement`
let docContent ← match docContent with let docComment : Option String ← match (← parseDocComment doc) with
| none => pure none | none => pure none
| some d => d.translate | some d => d.translate
@@ -356,7 +356,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
let modifiedVal ← match val with let modifiedVal ← match val with
| `(Parser.Command.declVal| := by $proof) => | `(Parser.Command.declVal| := by $proof) =>
`(Parser.Command.declVal| := by {let_intros; $(⟨preambleSeq⟩); $(⟨proof⟩)}) `(Parser.Command.declVal| := by {let_intros; $(⟨preambleSeq⟩); $(⟨proof⟩)})
| _ => panic "expected `:= by`" | _ => panic "Expected `:= by`!"
-- Add theorem to context. -- Add theorem to context.
match statementName with match statementName with
@@ -374,12 +374,12 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $modifiedVal) let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $modifiedVal)
elabCommand thmStatement elabCommand thmStatement
-- Check that statement has a docs entry. -- Check that statement has a docs entry.
checkInventoryDoc .Theorem name (name := fullName) (template := docContent) checkInventoryDoc .Theorem name (name := fullName) (template := docComment)
else else
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $modifiedVal) let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $modifiedVal)
elabCommand thmStatement elabCommand thmStatement
-- Check that statement has a docs entry. -- Check that statement has a docs entry.
checkInventoryDoc .Theorem name (name := fullName) (template := docContent) checkInventoryDoc .Theorem name (name := fullName) (template := docComment)
| none => | none =>
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $modifiedVal) let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $modifiedVal)
elabCommand thmStatement elabCommand thmStatement
@@ -460,7 +460,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
goal := sig, goal := sig,
preamble := preambleSeq preamble := preambleSeq
scope := scope, scope := scope,
descrText := docContent descrText := docComment
statementName := match statementName with statementName := match statementName with
| none => default | none => default
| some name => currNamespace ++ name.getId | some name => currNamespace ++ name.getId