DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Add references

Browse source
This commit is contained in:
jstoobysmith 2024-09-15 10:18:05 -04:00
parent 016fb72af8
commit b1cfbe9a7a
1 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

24
HepLean/Meta/Informal.lean
View file

@ -13,6 +13,8 @@ open Lean Elab System
/-! TODO: Derive a means to extract informal definitions and informal lemmas. -/
/-! TODO: Can likely make this a bona-fide command. -/
/-- The structure representating an informal definition. -/
structure InformalDefinition where
/-- The name of the informal definition. This is autogenerated. -/
@ -21,6 +23,8 @@ structure InformalDefinition where
math : String
/-- The physics description of the definition. -/
physics : String
/-- References. -/
ref : String
/-- The structure representating an informal proof. -/
structure InformalLemma where
@ -32,6 +36,8 @@ structure InformalLemma where
physics : String
/-- A description of the proof. -/
proof : String
/-- References. -/
ref : String
namespace Informal
@ -49,6 +55,7 @@ syntax (name := informal_definition) "informal_definition " ident
macro "informal_definition " name:ident " where " assignments:informalAssignment* : command => do
let mut math_def? : Option (TSyntax `term) := none
let mut physics_def? : Option (TSyntax `term) := none
let mut ref_def? : Option (TSyntax `term) := none
for assignment in assignments do
match assignment with
| `(informalAssignment| physics :≈ $val:str) =>
@ -57,15 +64,19 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
| `(informalAssignment| math :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
math_def? := some (← `($(Lean.quote strVal)))
| `(informalAssignment| ref :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
ref_def? := some (← `($(Lean.quote strVal)))
| _ => Macro.throwError "invalid assignment syntax"
unless physics_def?.isSome && math_def?.isSome do
Macro.throwError "Both 'physics' and 'math' assignments are required"
unless math_def?.isSome do
Macro.throwError "A 'math' assignments is required"
`(
/-- An informal definition. -/
def $name : InformalDefinition := {
name := $(Lean.quote name.getId),
physics := $(physics_def?.getD (← `("No physics description provided"))),
math := $(math_def?.getD (panic! "math not assigned"))
math := $(math_def?.getD (panic! "math not assigned")),
ref := $(ref_def?.getD (← `("No references provided")))
})
/-- The syntax for the command `informal_lemma`. -/
@ -77,6 +88,7 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
let mut math_def? : Option (TSyntax `term) := none
let mut physics_def? : Option (TSyntax `term) := none
let mut proof_def? : Option (TSyntax `term) := none
let mut ref_def? : Option (TSyntax `term) := none
for assignment in assignments do
match assignment with
| `(informalAssignment| physics :≈ $val:str) =>
@ -88,9 +100,12 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
| `(informalAssignment| proof :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for proof"
proof_def? := some (← `($(Lean.quote strVal)))
| `(informalAssignment| ref :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
ref_def? := some (← `($(Lean.quote strVal)))
| _ => Macro.throwError "invalid assignment syntax"
unless math_def?.isSome do
Macro.throwError "Both 'physics' and 'math' assignments are required"
Macro.throwError "A 'math' assignments is required"
`(
/-- An informal lemma. -/
def $name : InformalLemma := {
@ -98,6 +113,7 @@ def $name : InformalLemma := {
physics := $(physics_def?.getD (← `("No physics description provided"))),
math := $(math_def?.getD (panic! "math not assigned")),
proof := $(proof_def?.getD (← `("No proof description provided"))),
ref := $(ref_def?.getD (← `("No references provided")))
})
end Informal