Skip to content

Commit

Permalink
Fix: Clean up Formatting of Generic Parser (#466)
Browse files Browse the repository at this point in the history
See
#455
for more information.
Changes made:
1. Added a documentation string to the function `getSuffixId`
2. Improve indentation and formatting of `getSuffixId`

---------

Co-authored-by: Atticus Kuhn <[email protected]>
Co-authored-by: Alex Keizer <[email protected]>
  • Loading branch information
3 people authored Jul 17, 2024
1 parent ab81800 commit 81f28e0
Showing 1 changed file with 16 additions and 4 deletions.
20 changes: 16 additions & 4 deletions SSA/Core/MLIRSyntax/GenericParser.lean
Original file line number Diff line number Diff line change
Expand Up @@ -501,6 +501,19 @@ syntax mlir_suffix_id := num <|> ident
syntax "{" ("^" mlir_suffix_id ("(" sepBy(mlir_bb_operand, ",") ")")? ":")? mlir_ops "}" : mlir_region
syntax "[mlir_region|" mlir_region "]": term

/--
`getSuffixId` converts the syntax object of a `suffix id` to a string.
A `suffix id` is a notion from the MLIR standard defined as
```bnf
suffix-id ::= (digit+ | ((letter|id-punct) (letter|id-punct|digit)*))
```
See more at
https://mlir.llvm.org/docs/LangRef/#identifiers-and-keywords
If the suffix id is a number (the left choice), we convert that number to a string
If the suffix id is an identifier (the right choice), we convert that identifier to a string
`getSuffixId` is used in parsing the syntax of MLIR to a Lean AST
-/
def getSuffixId : TSyntax ``mlir_suffix_id → String
| `(mlir_suffix_id| $x:ident) => x.getId.toString
| `(mlir_suffix_id| $x:num) => toString (x.getNat)
Expand Down Expand Up @@ -724,10 +737,9 @@ macro_rules
| none, some y => Macro.throwErrorAt y "Caret closed without being opened"
| some x, none => Macro.throwErrorAt x "Caret opened without being closed"
| _ , _ =>

let attrsList <- attrEntries.getElems.toList.mapM (fun x => `([mlir_attr_entry| $x]))
let attrsList <- quoteMList attrsList (<- `(MLIR.AST.AttrEntry _))
`(AttrDict.mk $attrsList)
let attrsList <- attrEntries.getElems.toList.mapM (fun x => `([mlir_attr_entry| $x]))
let attrsList <- quoteMList attrsList (<- `(MLIR.AST.AttrEntry _))
`(AttrDict.mk $attrsList)
-- dict attribute val
syntax mlir_attr_dict : mlir_attr_val

Expand Down

0 comments on commit 81f28e0

Please sign in to comment.