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";