annotate Paper/escape_agda.rb @ 4:0149a5c6d254

add 実験演習の説明を追加
author kiyama <e185758@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2023 01:09:33 +0900
parents 6e6dcd18b4f6
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 #!/usr/bin/env ruby
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 # coding: utf-8
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 Suffix = '.agda.replaced'
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 EscapeChar = '!'
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 FileName = ARGV.first
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 ReplaceTable = {
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 '→' => 'rightarrow',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 '->' => 'rightarrow',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 '⊔' => 'sqcup',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 '∷' => 'text{::}',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 '∙' => 'circ',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 '≡' => 'equiv',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 '×' => 'times',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 '⟨' => 'langle',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 '⟩' => 'rangle',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 'ℕ' => 'mathbb{N}',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 '₁' => '_{1}',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 '₂' => '_{2}',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 '₃' => '_{3}',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 '∎' => 'blacksquare',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 'λ' => 'lambda',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 '∧' => 'wedge',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 '/\\' => 'wedge',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 '⇒' => 'Rightarrow',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 '¬' => 'neg',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 '≤' => 'leq',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 '⊥' => 'bot',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 '∀' => 'forall',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 '#' => '\#',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 '⊤' => '\top',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 '\'' => '\prime',
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 '≈' => '\approx'
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 }
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 code = File.read(FileName)
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ReplaceTable.each do |k, v|
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 code = code.gsub(k, escaped_str)
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 end
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
6e6dcd18b4f6 add Paper
kiyama <e185758@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 File.write(FileName.sub(/.agda$/, Suffix), code)