Escape Agda for LaTeX

escape_agda.rb

#!/usr/bin/env ruby

Suffix     = '.eagda'
EscapeChar = '@'
FileName   = ARGV.first

ReplaceTable = {
  '->' => 'rightarrow',
  '≡' => 'equiv',
  '⟨'  => 'langle',
  '⟩'  => 'rangle',
  '∎'  => 'blacksquare'
}

code = File.read(FileName)
ReplaceTable.each do |k, v|
  escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar
  code        = code.gsub(k, escaped_str)
end

File.write(FileName.sub(/.agda$/, Suffix), code)

escape_agda.tex

\documentclass[a4j,12pt]{jreport}
\usepackage[dvipdfmx]{graphicx}
\usepackage{listings}
\usepackage{amssymb}

\title{Agda のソースを listings で LaTeX に埋め込む}
\lstset{
  escapechar={@},
}


\begin{document}
\maketitle
こんな感じ?

\begin{table}[html]
    \lstinputlisting[label=src:nat, caption=自然数の加算の交換法則] {nat.eagda}
\end{table}
\end{document}

Makefile

# Settings
TARGET=escape_agda
SOURCES=$(wildcard *.agda)
SOURCES_FOR_TEX=$(subst .agda,.eagda,$(SOURCES))


# dependencies
$(TARGET).pdf : $(TARGET).dvi
	dvipdfmx $<

$(TARGET).dvi : $(wildcard *.tex) $(SOURCES_FOR_TEX)
	platex  $(TARGET).tex
	platex  $(TARGET).tex
	platex  $(TARGET).tex

%.eagda: %.agda
	ruby escape_agda.rb $<


# commands
.PHONY : clean open remake

clean:
	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg

open: $(TARGET).pdf
	open $(TARGET).pdf

remake:
	make clean
	make

nat.agda

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

module nat where

data Nat : Set where
  O : Nat
  S : Nat -> Nat

_+_ : Nat -> Nat -> Nat
O   + n = n 
S m + n = S (m + n)

right-increment : (n m : Nat) -> S (n + m) ≡ n + (S m)
right-increment O m     = refl
right-increment (S n) m = cong S (right-increment n m)


add-sym : (n m : Nat) -> n + m ≡ m + n
add-sym O O = refl
add-sym O (S m) = cong S (add-sym O m)
add-sym (S n) O = cong S (add-sym n O)
add-sym (S n) (S m) = begin
  (S n) + (S m) ≡⟨ refl ⟩
  S (n + S m)   ≡⟨ (cong S (add-sym n (S m))) ⟩
  S (S m + n)   ≡⟨ cong S (right-increment m n) ⟩
  S (m + S n)   ≡⟨ refl ⟩
  (S m) + (S n) ∎