Skip to content

Commit

Permalink
fix: improve optional antiquotes
Browse files Browse the repository at this point in the history
  • Loading branch information
@david-christiansen
david-christiansen committed Oct 28, 2024
1 parent 70a47e8 commit 3574d76
Show file tree
Hide file tree
Showing 2 changed files with 165 additions and 92 deletions.
55 changes: 48 additions & 7 deletions Manual/Language/Classes.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -344,28 +344,31 @@ The only syntactic differences are that the keyword {keywordOf Lean.Parser.Comma

:::syntax Lean.Parser.Command.instance

Most instances take the form of definitions of each method:
Most instances define each method using {keywordOf Lean.Parser.Command.declaration}`where` syntax:

```grammar
instance $_? : $_ where
instance $[(priority := $p:prio)]? $name? $_ where
$_*
```

However, type classes are inductive types and instances can be constructed using any expression with an appropriate type:
However, type classes are inductive types, so instances can be constructed using any expression with an appropriate type:

```grammar
instance $_? : $_ := $_
instance $[(priority := $p:prio)]? $_? $_ :=
$_
```

Instances may also be defined by cases; however, this feature is rarely used:
Instances may also be defined by cases; however, this feature is rarely used outside of {name}`Decidable` instances:

```grammar
instance $_? : $_
instance $[(priority := $p:prio)]? $_? $_
$[| $_ => $_]*
```

:::



Elaboration of instances is almost identical to the elaboration of ordinary definitions, with the exception of the caveats documented below.
If no name is provided, then one is created automatically.
It is possible to refer to this generated name directly, but the algorithm used to generate the names has changed in the past and may change in the future.
Expand Down Expand Up @@ -556,9 +559,47 @@ instance instDecidableEqStringList : DecidableEq StringList


::: planned 62
This section will describe the specification of priorities, but not their function in the synthesis algorithm..
This section will describe the specification of priorities, but not their function in the synthesis algorithm.
:::

Instances may be assigned {deftech}_priorities_.
During instance synthesis, higher-priority instances are preferred; see {TODO}[ref] for details of instance synthesis.

:::syntax prio open:=false
Priorities may be numeric:
```grammar
$n:num
```

If no priority is specified, the default priority that corresponds to {evalPrio}`default` is used:
```grammar
default
```

Three named priorities are available when numeric values are too fine-grained, corresponding to {evalPrio}`low`, {evalPrio}`mid`, and {evalPrio}`high` respectively.
The {keywordOf prioMid}`mid` priority is lower than {keywordOf prioDefault}`default`.
```grammar
low
```
```grammar
mid
```
```grammar
high
```

Finally, priorities can be added and subtracted, so `default + 2` is a valid priority, corresponding to {evalPrio}`default + 2`:
```grammar
($_)
```
```grammar
$_ + $_
```
```grammar
$_ - $_
```

:::

# Instance Synthesis
%%%
Expand Down
202 changes: 117 additions & 85 deletions Manual/Meta/Syntax.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,24 @@ namespace Manual
-- TODO upstream this to enable cross-reference generation the usual Verso way
def syntaxKindDomain := `Manual.syntaxKind

@[role_expander evalPrio]
def evalPrio : RoleExpander
| args, inlines => do
ArgParse.done.run args
let #[inl] := inlines
| throwError "Expected a single code argument"
let `(inline|code{ $s:str }) := inl
| throwErrorAt inl "Expected code literal with the priority"
let altStr ← parserInputString s
match runParser (← getEnv) (← getOptions) (andthen ⟨{}, whitespace⟩ priorityParser) altStr (← getFileName) with
| .ok stx =>
let n ← liftMacroM (Lean.evalPrio stx)
pure #[← `(Verso.Doc.Inline.text $(quote s!"{n}"))]
| .error es =>
for (pos, msg) in es do
log (severity := .error) (mkErrorStringWithPos "<example>" pos msg)
throwError s!"Failed to parse priority from '{s.getString}'"

def Block.syntax : Block where
name := `Manual.syntax

Expand Down Expand Up @@ -199,7 +217,104 @@ def GrammarConfig.parse [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadError m]
((·.getD 0) <$> .named `prec .nat true)


open Manual.Meta.PPrint in
namespace Meta.PPrint.Grammar
def antiquoteOf : Name → Option Name
| .str n "antiquot" => pure n
| _ => none

def nonTerm : Name → String
| .str x "pseudo" => nonTerm x
| .str _ x => x
| x => x.toString

def empty : Syntax → Bool
| .node _ _ #[] => true
| _ => false

partial def kleeneLike (mod : String) : Syntax → Format → TagFormatT GrammarTag DocElabM Format
| .atom .., f
| .ident .., f
| .missing, f => do return f ++ (← tag .bnf mod)
| .node _ _ args, f => do
let nonempty := args.filter (!empty ·)
if h : nonempty.size = 1 then
kleeneLike mod nonempty[0] f
else
return (← tag .bnf "(") ++ f ++ (← tag .bnf s!"){mod}")

def kleene := kleeneLike "*"

def perhaps := kleeneLike "?"

def lined (ws : String) : Format :=
Format.line.joinSep (ws.splitOn "\n")


def infoWrap (info : SourceInfo) (doc : Format) : Format :=
if let .original leading _ trailing _ := info then
lined leading.toString ++ doc ++ lined trailing.toString
else doc

def infoWrap2 (info1 : SourceInfo) (info2 : SourceInfo) (doc : Format) : Format :=
let pre := if let .original leading _ _ _ := info1 then lined leading.toString else .nil
let post := if let .original _ _ trailing _ := info2 then lined trailing.toString else .nil
pre ++ doc ++ post

partial def production (stx : Syntax) : TagFormatT GrammarTag DocElabM Format := do
match stx with
| .atom info str => infoWrap info <$> tag .keyword str
| .missing => tag .error "<missing>"
| .ident info _ x _ =>
let d? ← findDocString? (← getEnv) x
-- TODO render markdown
let tok ←
tag (.nonterminal x d?) <|
match x with
| .str x' "pseudo" => x'.toString
| _ => x.toString
return infoWrap info tok
| .node info k args => do
infoWrap info <$>
match k, antiquoteOf k, args with
| `many.antiquot_suffix_splice, _, #[starred, star] =>
infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= kleene starred)
| `optional.antiquot_suffix_splice, _, #[questioned, star] => -- See also the case for antiquoted identifiers below
infoWrap2 questioned.getHeadInfo star.getTailInfo <$> (production questioned >>= perhaps questioned)
| `sepBy.antiquot_suffix_splice, _, #[starred, star] =>
infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= kleeneLike ",*" starred)
| `many.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info star] =>
infoWrap2 dollar.getHeadInfo info <$> (production contents >>= kleene contents)
| `optional.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info _star] =>
infoWrap2 dollar.getHeadInfo info <$> (production contents >>= perhaps contents)
| `sepBy.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info _star] =>
infoWrap2 dollar.getHeadInfo info <$> (production contents >>= kleeneLike ",*" contents)
| `choice, _, opts => do
return (← tag .bnf "(") ++ (" " ++ (← tag .bnf "|") ++ " ").joinSep (← opts.toList.mapM production) ++ (← tag .bnf ")")
| _, some k', #[a, b, c, d] => do
--
let doc? ← findDocString? (← getEnv) k'
let last :=
if let .node _ _ #[] := d then c else d
-- Optional quasiquotes $NAME? where kind FOO is expected look like this:
-- k := FOO.antiquot
-- k' := FOO
-- args := #["$", [], `NAME?, []]
if let (.atom _ "$", .node _ nullKind #[], .ident _ _ x _) := (a, b, c) then
if x.toString.back == '?' then
return infoWrap2 a.getHeadInfo last.getTailInfo ((← tag (.nonterminal k' doc?) (nonTerm k')) ++ (← tag .bnf "?"))

infoWrap2 a.getHeadInfo last.getTailInfo <$> tag (.nonterminal k' doc?) (nonTerm k')
| _, _, _ => do -- return ((← args.mapM production) |>.toList |> (Format.joinSep · " "))
let mut out := Format.nil
for a in args do
out := out ++ (← production a)
let doc? ← findDocString? (← getEnv) k
tag (.fromNonterminal k doc?) out

end Meta.PPrint.Grammar


open Manual.Meta.PPrint Grammar in
@[directive_expander «syntax»]
partial def «syntax» : DirectiveExpander
| args, blocks => do
Expand All @@ -222,90 +337,6 @@ where
if nameStx.getId == `grammar then some (argsStx, contents, info, col, «open», i, close) else none
| _ => none

antiquoteOf : Name → Option Name
| .str n "antiquot" => pure n
| _ => none

nonTerm : Name → String
| .str x "pseudo" => nonTerm x
| .str _ x => x
| x => x.toString

empty : Syntax → Bool
| .node _ _ #[] => true
| _ => false

kleeneLike (mod : String) : Syntax → Format → TagFormatT GrammarTag DocElabM Format
| .atom .., f
| .ident .., f
| .missing, f => do return f ++ (← tag .bnf mod)
| .node _ _ args, f => do
let nonempty := args.filter (!empty ·)
if h : nonempty.size = 1 then
kleeneLike mod nonempty[0] f
else
return (← tag .bnf "(") ++ f ++ (← tag .bnf s!"){mod}")

kleene := kleeneLike "*"

perhaps := kleeneLike "?"


production (stx : Syntax) : TagFormatT GrammarTag DocElabM Format := do
match stx with
| .atom info str => infoWrap info <$> tag .keyword str
| .missing => tag .error "<missing>"
| .ident info _ x _ =>
let d? ← findDocString? (← getEnv) x
-- TODO render markdown
let tok ←
tag (.nonterminal x d?) <|
match x with
| .str x' "pseudo" => x'.toString
| _ => x.toString
return infoWrap info tok
| .node info k args => do
infoWrap info <$>
match k, antiquoteOf k, args with
| `many.antiquot_suffix_splice, _, #[starred, star] =>
infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= kleene starred)
| `optional.antiquot_suffix_splice, _, #[starred, star] =>
infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= perhaps starred)
| `sepBy.antiquot_suffix_splice, _, #[starred, star] =>
infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= kleeneLike ",*" starred)
| `many.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info star] =>
infoWrap2 dollar.getHeadInfo info <$> (production contents >>= kleene contents)
| `optional.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info _star] =>
infoWrap2 dollar.getHeadInfo info <$> (production contents >>= perhaps contents)
| `sepBy.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info _star] =>
infoWrap2 dollar.getHeadInfo info <$> (production contents >>= kleeneLike ",*" contents)
| `choice, _, opts => do
return (← tag .bnf "(") ++ (" " ++ (← tag .bnf "|") ++ " ").joinSep (← opts.toList.mapM production) ++ (← tag .bnf ")")
| _, some k', #[a, b, c, d] => do
let doc? ← findDocString? (← getEnv) k'
let last :=
if let .node _ _ #[] := d then c else d
infoWrap2 a.getHeadInfo last.getTailInfo <$> tag (.nonterminal k' doc?) (nonTerm k')
| _, _, _ => do -- return ((← args.mapM production) |>.toList |> (Format.joinSep · " "))
let mut out := Format.nil
for a in args do
out := out ++ (← production a)
let doc? ← findDocString? (← getEnv) k
tag (.fromNonterminal k doc?) out

lined (ws : String) : Format :=
Format.line.joinSep (ws.splitOn "\n")

infoWrap (info : SourceInfo) (doc : Format) : Format :=
if let .original leading _ trailing _ := info then
lined leading.toString ++ doc ++ lined trailing.toString
else doc

infoWrap2 (info1 : SourceInfo) (info2 : SourceInfo) (doc : Format) : Format :=
let pre := if let .original leading _ _ _ := info1 then lined leading.toString else .nil
let post := if let .original _ _ trailing _ := info2 then lined trailing.toString else .nil
pre ++ doc ++ post

categoryOf (env : Environment) (kind : Name) : Option Name := do
for (catName, contents) in (Lean.Parser.parserExtension.getState env).categories do
for (k, ()) in contents.kinds do
Expand All @@ -329,6 +360,7 @@ where
for (pos, msg) in es do
log (severity := .error) (mkErrorStringWithPos "<example>" pos msg)
`(sorry)

getBnf config isFirst howMany (stx : Syntax) : DocElabM (TaggedText GrammarTag) := do
return (← renderBnf config isFirst howMany stx |>.run).render (w := 5)

Expand Down

0 comments on commit 3574d76

Please sign in to comment.