view Paper/escape_agda.rb @ 5:339fb67b4375

INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents 9176dff8f38a
children
line wrap: on
line source

#!/usr/bin/env ruby
# coding: utf-8

Suffix     = '.agda.replaced'
EscapeChar = '!'
FileName   = ARGV.first

ReplaceTable = {
  '→' => 'rightarrow',
  '->' => 'rightarrow',
  '⊔'  => 'sqcup',
  '∷' => 'text{::}',
  '∙'  => 'circ',
  '≡' => 'equiv',
  '×' => 'times',
  '⟨'  => 'langle',
  '⟩'  => 'rangle',
  'ℕ' => 'mathbb{N}',
  '₁' => '_{1}',
  '₂' => '_{2}',
  '₃' => '_{3}',
  '∎'  => 'blacksquare',
  'λ' => 'lambda',
  '∧' => 'wedge',
  '/\\' => 'wedge',
  '⇒' => 'Rightarrow',
  '¬' => 'neg',
  '≤' => 'leq',
  '⊥' => 'bot',
  '∀' => 'forall',
  '#' => '\#',
  '⊤' => '\top',
  '\'' => '\prime',
  '≈' =>  '\approx'
}

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)