This is part of a plugin I'm writing for TeXmacs
that translates the Hybrid Logic input and output
of the HyLoRes and HyLoTab proof systems from ASCII
into TeX.
#!/usr/bin/perl -w
# negation: ! ~ -
# conjunction: ^ & &&
# disjunction: v | ||
# top: true top
# bottom: false bottom
# implication: -> <-
# equivalence: <->
# prop.letters: p P P[0-9]+ (all words excluding the letter v)
# nominals: n N N[0-9]+ (all words excl...)
# relations: r R R[0-9]+ (...)
# diamonds: <> <label> (e.g. "<R2>" a relation 2 diamond)
# boxes: [] [label]
# down arrow: down
# at operator: @i expr. (where i is a nominal)
# nominal : expr. (e.g. "Here : P^<>Q")
while(<>) {
chomp;
s/\{([^\}]*)\}/$1/; # {...} blocks
s/\<\>/\\wasyDiamond /g; # diamonds
s/\<(\w+)\>/\\wasyDiamond_{$1}/g; # named diamonds
s/\[\]/\\box /g; # boxes
s/\[(\w+)\]/\\box_{$1}/g; # named boxes
s/\<-\>/\\leftrightarrow /g; # equivalence
s/-\>/\\rightarrow /g; # implication (right)
s/\<-/\\leftarrow /g; # implication (left)
s/down/\\downarrow /ig; # down (case insensitive)
s/\@(\w+)/\@_{$1}/g; # at @
s/(\w+)\s*:/\@_{$1}/g;
s/\@\(\s*(\S+)\s*,([^\]]*)\)/\@_{$1} $2/g;
s/\@\((\w+),/\@_{$1} \(/g;
s/(v|\|{1,2})/\\vee /g; # disjunction
s/(-|!|~)/\\neg /g; # negation
s/(true|top)/\\top /ig; # top
s/(false|bottom)/\\perp /ig; # bottom
s/(\^|\&{1,2})/\\wedge /g; # conjunction
s/\[([^\]]*)\]/$1/g; # [...] blocks
s/p([0-9]+)/P_{$1} /ig; # prop letters
s/n([0-9]+)/N_{$1} /ig; # nominal letters
s/r([0-9]+)/R_{$1} /ig; # relation letters
print "\\par\\noindent\$$_\$";
}
print "\\bye";