Skip to content

Commit 7cf03d6

Browse files
cpitclaudelcpitclaudel
committed
literate: Add support for parameters in Coq directives
1 parent 072ae74 commit 7cf03d6

File tree

2 files changed

+168
-37
lines changed

2 files changed

+168
-37
lines changed

‎alectryon/literate.py‎

Lines changed: 161 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -338,34 +338,54 @@ def coq_partition(doc):
338338
COQDOC_CLOSE = re.compile(r"[ \t]*[*]+[)]\Z")
339339

340340
DEFAULT_HEADER = ".. coq::"
341-
DIRECTIVE = re.compile(r"([ \t]*)([.][.] coq::.*)?")
341+
INDENT = re.compile(r"(?P<indent>[ \t]*)")
342+
COQ_DIRECTIVE = re.compile(r"(?P<indent>[ \t]*)([.][.] coq::.*)")
342343

343-
Lit = namedtuple("Lit", "lines directive indent")
344+
Lit = namedtuple("Lit", "lines directive_lines indent")
344345
CodeBlock = namedtuple("CodeBlock", "lines indent")
345346

347+
def _last_coq_directive(lines):
348+
directive = deque()
349+
expected_coq_indent = float("+inf")
350+
while lines:
351+
line = lines.pop()
352+
directive.appendleft(line)
353+
indent = measure_indentation(line)
354+
m = line.match(COQ_DIRECTIVE)
355+
if m:
356+
if indent <= expected_coq_indent:
357+
return lines, m, directive
358+
break
359+
if not line.isspace():
360+
expected_coq_indent = min(expected_coq_indent, indent - 3)
361+
if expected_coq_indent < 0:
362+
break # No need to keep looping
363+
return lines + directive, None, None
364+
346365
def lit(lines, indent):
347366
strip_deque(lines)
348-
m = lines and lines[-1].match(DIRECTIVE)
349-
indent, directive = m.groups() if m else (indent, None)
350-
if directive:
351-
directive = lines.pop()
367+
lines, m, directive_lines = _last_coq_directive(lines)
368+
if directive_lines:
369+
indent = m.group("indent")
352370
strip_deque(lines)
353371
else:
354-
directive = indent + DEFAULT_HEADER
355-
return Lit(lines, directive=directive, indent=indent)
372+
if lines:
373+
indent = lines[-1].match(INDENT).group("indent")
374+
directive_lines = [indent + DEFAULT_HEADER]
375+
return Lit(lines, directive_lines=directive_lines, indent=indent)
356376

357377
def number_lines(span, start):
358378
lines = span.split("\n")
359379
d = deque(Line(num, [s]) for (num, s) in enumerate(lines, start=start))
360380
return start + len(lines) - 1, d
361381

362382
def gen_rst(spans):
363-
linum, indent, prefix = 0, "", DEFAULT_HEADER
383+
linum, indent, prefix = 0, "", [DEFAULT_HEADER]
364384
for span in spans:
365385
if isinstance(span, Comment):
366386
linum, lines = number_lines(span.v.trim(LIT_OPEN, LIT_CLOSE), linum)
367387
litspan = lit(lines, indent)
368-
indent, prefix = litspan.indent, litspan.directive
388+
indent, prefix = litspan.indent, litspan.directive_lines
369389
if litspan.lines:
370390
yield from (replace(l, UNQUOTE_PAIRS) for l in litspan.lines)
371391
yield ""
@@ -375,7 +395,7 @@ def gen_rst(spans):
375395
for l in lines:
376396
l.parts.insert(0, indent + " ")
377397
if lines:
378-
yield prefix
398+
yield from prefix
379399
yield ""
380400
yield from lines
381401
yield ""
@@ -399,6 +419,40 @@ def coq2rst_lines(coq):
399419
return gen_rst(coq_partition_literate(coq))
400420

401421
def coq2rst(coq):
422+
"""Translate a fragment of Coq code to reST.
423+
424+
>>> print(coq2rst('''
425+
... (*|
426+
... Example:
427+
... |*)
428+
...
429+
... Goal True.
430+
...
431+
... (*|
432+
... Second example:
433+
...
434+
... .. coq::
435+
... :name:
436+
... snd
437+
... |*)
438+
...
439+
... exact I. Qed.
440+
... '''))
441+
Example:
442+
<BLANKLINE>
443+
.. coq::
444+
<BLANKLINE>
445+
Goal True.
446+
<BLANKLINE>
447+
Second example:
448+
<BLANKLINE>
449+
.. coq::
450+
:name:
451+
snd
452+
<BLANKLINE>
453+
exact I. Qed.
454+
<BLANKLINE>
455+
"""
402456
return join_lines(coq2rst_lines(coq))
403457

404458
def coq2rst_marked(coq, point, marker):
@@ -417,31 +471,68 @@ def coq2rst_marked(coq, point, marker):
417471
# note that it detects *all* ‘.. coq::’ blocks, including quoted ones.
418472

419473
COQ_BLOCK = re.compile(r"""
420-
^(?P<indent>[ \t]*)[.][.][ ]coq::.*
474+
(?P<directive>
475+
^(?P<indent>[ \t]*)
476+
[.][.][ ]coq::.*
477+
(?P<options>
478+
(?:\n
479+
(?P=indent)[ ][ ][ ] [ \t]*[^ \t].*$)*))
421480
(?P<body>
422-
(?:\n
423-
(?:[ \t]*\n)*
424-
(?P=indent)[ ][ ][ ].*$)*)
481+
(?:\n
482+
(?:[ \t]*\n)*
483+
(?P=indent)[ ][ ][ ] .*$)*)
425484
""", re.VERBOSE | re.MULTILINE)
426485

427486
def rst_partition(s):
487+
"""Identify ``.. coq::`` blocks in reST sources.
488+
489+
>>> import black
490+
>>> print(black.format_str(repr(list(rst_partition('''\\
491+
... .. coq::
492+
...
493+
... Goal True.
494+
... exact I. Qed.\\
495+
... '''))), mode=black.FileMode()))
496+
[
497+
Lit(
498+
lines=deque([Line(num=0, parts=[""])]),
499+
directive_lines=deque([Line(num=0, parts=[".. coq::"])]),
500+
indent=0,
501+
),
502+
CodeBlock(
503+
lines=deque(
504+
[
505+
Line(num=0, parts=[""]),
506+
Line(num=1, parts=[""]),
507+
Line(num=2, parts=[" Goal True."]),
508+
Line(num=3, parts=[" exact I. Qed."]),
509+
]
510+
),
511+
indent=0,
512+
),
513+
]
514+
<BLANKLINE>
515+
"""
428516
beg, linum = 0, 0
429517
for m in COQ_BLOCK.finditer(s):
430518
indent = len(m.group("indent"))
431519
rst = StringView(s, beg, m.start())
432-
block = StringView(s, *m.span())
520+
directive = StringView(s, *m.span('directive'))
521+
body = StringView(s, *m.span('body'))
433522

434523
linum, rst_lines = number_lines(rst, linum)
435-
linum, block_lines = number_lines(block, linum)
436-
directive = block_lines.popleft()
524+
linum, directive_lines = number_lines(directive, linum)
525+
linum, body_lines = number_lines(body, linum)
526+
527+
# body_lines.popleft() # Discard initial blank
437528

438-
yield Lit(rst_lines, directive=directive, indent=indent)
439-
yield CodeBlock(block_lines, indent=indent)
529+
yield Lit(rst_lines, directive_lines=directive_lines, indent=indent)
530+
yield CodeBlock(body_lines, indent=indent)
440531
beg = m.end()
441532
if beg < len(s):
442533
rst = StringView(s, beg, len(s))
443534
linum, lines = number_lines(rst, linum)
444-
yield Lit(lines, directive=None, indent=None)
535+
yield Lit(lines, directive_lines=None, indent=None)
445536

446537
# Conversion
447538
# ----------
@@ -451,29 +542,34 @@ def measure_indentation(line):
451542
m = line.match(INDENTATION_RE)
452543
return m.end() - m.start()
453544

545+
def redundant_directive(directive_lines, directive_indent, last_indent):
546+
return (
547+
directive_lines and
548+
len(directive_lines) == 1 and
549+
str(directive_lines[0]).strip() == DEFAULT_HEADER
550+
and directive_indent == last_indent
551+
)
552+
454553
def trim_rst_block(block, last_indent, keep_empty):
455554
strip_deque(block.lines)
456-
directive_indent = block.indent # Stored here for convenience
457555
last_indent = measure_indentation(block.lines[-1]) if block.lines else last_indent
458556

459-
directive = block.directive
460-
keep_empty = keep_empty and directive is not None
461-
if (directive
462-
and str(directive).strip() == DEFAULT_HEADER
463-
and directive_indent == last_indent):
464-
directive = None
557+
directive_lines = block.directive_lines
558+
keep_empty = keep_empty and directive_lines
559+
if redundant_directive(directive_lines, block.indent, last_indent):
560+
directive_lines = None
465561

466-
if not block.lines and not directive:
562+
if not block.lines and not directive_lines:
467563
if keep_empty:
468564
yield "(*||*)"
469565
yield ""
470566
else:
471567
yield "(*|"
472568
yield from (replace(l, QUOTE_PAIRS) for l in block.lines)
473-
if directive:
569+
if directive_lines:
474570
if block.lines:
475571
yield ""
476-
yield directive
572+
yield from directive_lines
477573
yield "|*)"
478574
yield ""
479575

@@ -497,6 +593,40 @@ def rst2coq_lines(rst):
497593
return gen_coq(rst_partition(rst))
498594

499595
def rst2coq(rst):
596+
"""Translate a fragment of reST code to Coq.
597+
598+
>>> print(rst2coq('''
599+
... Example:
600+
...
601+
... .. coq::
602+
...
603+
... Goal True.
604+
...
605+
... Second example:
606+
...
607+
... .. coq::
608+
... :name:
609+
... snd
610+
...
611+
... exact I. Qed.
612+
... '''))
613+
(*|
614+
Example:
615+
|*)
616+
<BLANKLINE>
617+
Goal True.
618+
<BLANKLINE>
619+
(*|
620+
Second example:
621+
<BLANKLINE>
622+
.. coq::
623+
:name:
624+
snd
625+
|*)
626+
<BLANKLINE>
627+
exact I. Qed.
628+
<BLANKLINE>
629+
"""
500630
return join_lines(rst2coq_lines(rst))
501631

502632
def rst2coq_marked(rst, point, marker):
@@ -545,10 +675,5 @@ def main():
545675
contents = fstream.read()
546676
sys.stdout.write(args.fn(contents))
547677

548-
def run_doctest():
549-
import sys
550-
import doctest
551-
doctest.debug(sys.modules.get('__main__'), "__main__.partition", pm=True)
552-
553678
if __name__ == '__main__':
554679
main()

‎recipes/_output/tests/doctests.out‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,19 @@
11
annotate (alectryon.core)
22
Doctest: alectryon.core.annotate ... ok
3+
coq2rst (alectryon.literate)
4+
Doctest: alectryon.literate.coq2rst ... ok
35
coq_partition (alectryon.literate)
46
Doctest: alectryon.literate.coq_partition ... ok
7+
rst2coq (alectryon.literate)
8+
Doctest: alectryon.literate.rst2coq ... ok
9+
rst_partition (alectryon.literate)
10+
Doctest: alectryon.literate.rst_partition ... ok
511
add_tokens (alectryon.pygments)
612
Doctest: alectryon.pygments.add_tokens ... ok
713
highlight_html (alectryon.pygments)
814
Doctest: alectryon.pygments.highlight_html ... ok
915

1016
----------------------------------------------------------------------
11-
Ran 4 tests
17+
Ran 7 tests
1218

1319
OK

0 commit comments

Comments
 (0)