File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -53,17 +53,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
5353 /** Gets the rank of element `e`, which is used internally in the string encoding. */
5454 int getRank ( Element e ) { e = DenseRank< DenseRankInput > :: denseRank ( result ) }
5555
56- private module AsciiDenseRankInput implements DenseRankInputSig {
57- class Ranked = string ;
58-
59- int getRank ( string s ) {
60- result = asciiPrintable ( s ) and
61- s != "." // used as element separator
62- }
63- }
64-
56+ pragma [ nomagic]
6557 private string interpretAsciiCode ( int code ) {
66- result = DenseRank< AsciiDenseRankInput > :: denseRank ( code + 1 )
58+ exists ( int dot , int c |
59+ c = code + 1 and
60+ dot = asciiPrintable ( "." ) and // used as element separator
61+ if c < dot then c = asciiPrintable ( result ) else c + 1 = asciiPrintable ( result )
62+ )
6763 }
6864
6965 private int asciiCodes ( ) { result = strictcount ( interpretAsciiCode ( _) ) }
You can’t perform that action at this time.
0 commit comments