summaryrefslogtreecommitdiff
path: root/support/splint/examples/types/basic.sty
diff options
context:
space:
mode:
Diffstat (limited to 'support/splint/examples/types/basic.sty')
-rw-r--r--support/splint/examples/types/basic.sty464
1 files changed, 464 insertions, 0 deletions
diff --git a/support/splint/examples/types/basic.sty b/support/splint/examples/types/basic.sty
new file mode 100644
index 0000000000..856faf2374
--- /dev/null
+++ b/support/splint/examples/types/basic.sty
@@ -0,0 +1,464 @@
+% Copyright 2012-2014, Alexander Shibakov
+% This file is part of SPLinT
+%
+% SPLinT is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+%
+% SPLinT is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+%
+% You should have received a copy of the GNU General Public License
+% along with SPLinT. If not, see <http://www.gnu.org/licenses/>.
+
+% various macros that implement `expandable arithmetic' that can be
+% used with the tree evaluator macros;
+% these are here as an example only; a much more complete version of
+% big integer arithmetic (including division and exponentiation) is
+% implemented in the `bigintcalc' package by Heiko Oberdiek; I was
+% unaware of the existence of `bigintcalc' when these macros were written;
+% note that the tree evaluator macros perform recursive expansion of
+% their arguments; `bigintcalc' uses \number for the same purpose
+% (since \number will keep expanding tokens until a non digit is
+% encountered)
+
+% macros that expand into a sequence of given length
+
+% #1 is the 1-radix of the number read so far
+% #2 is the `digit'
+% #3 is the next 10-radix digit to be processed or `S'
+
+\def\unroll#1#2#3{\csname unroll#3\endcsname{#1}{#2}}
+\expandafter\def\csname unroll0\endcsname#1#2{\unroll{#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll1\endcsname#1#2{\unroll{#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll2\endcsname#1#2{\unroll{#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll3\endcsname#1#2{\unroll{#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll4\endcsname#1#2{\unroll{#2#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll5\endcsname#1#2{\unroll{#2#2#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll6\endcsname#1#2{\unroll{#2#2#2#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll7\endcsname#1#2{\unroll{#2#2#2#2#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll8\endcsname#1#2{\unroll{#2#2#2#2#2#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+\expandafter\def\csname unroll9\endcsname#1#2{\unroll{#2#2#2#2#2#2#2#2#2#1#1#1#1#1#1#1#1#1#1}{#2}}
+
+\def\unrollS#1#2#3{%
+ \ifx#3F%
+ \xskiptofi{#1S}%
+ \else
+ \xskiptofi{G{#1}}%
+ \fi
+}
+
+\def\sequence#1#2{\expandafter\s@quence\expandafter{\number#1}{#2}}
+\def\s@quence#1#2{\unrollbegin{}{#2}{}#1}
+
+\def\unrollbegin#1#2#3#4#5{%
+ \ifx#5S%
+ \ifx#40%
+ \yybreak@{S}%
+ \else
+ \yybreak@{\unroll{#1}{#2}{#3}#4#5}%
+ \fi
+ \else
+ \yybreak{\unroll{#1}{#2}{#3}#4#5}%
+ \yycontinue
+}
+
+% macros that count the number of non-S in a sequence
+
+\def\startconversion#1{%
+ \ifx#1S%
+ \xskiptofi{0}%
+ \else
+ \xskiptofi{\convertone{}{}}%
+ \fi
+}
+
+\def\convertzer@#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{#1}%
+ \else
+ \xskiptofi{\convertone{0#1}{#2}}%
+ \fi
+}
+
+\def\convertzero#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzer@{#1}{}#2S}%
+ \else
+ \xskiptofi{\convertone{#1}{#2}}%
+ \fi
+}
+
+\def\convertone#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{1#1}{}#2S}%
+ \else
+ \xskiptofi{\converttwo{#1}{#2}}%
+ \fi
+}
+
+\def\converttwo#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{2#1}{}#2S}%
+ \else
+ \xskiptofi{\convertthree{#1}{#2}}%
+ \fi
+}
+
+\def\convertthree#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{3#1}{}#2S}%
+ \else
+ \xskiptofi{\convertfour{#1}{#2}}%
+ \fi
+}
+
+\def\convertfour#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{4#1}{}#2S}%
+ \else
+ \xskiptofi{\convertfive{#1}{#2}}%
+ \fi
+}
+
+\def\convertfive#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{5#1}{}#2S}%
+ \else
+ \xskiptofi{\convertsix{#1}{#2}}%
+ \fi
+}
+
+\def\convertsix#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{6#1}{}#2S}%
+ \else
+ \xskiptofi{\convertseven{#1}{#2}}%
+ \fi
+}
+
+\def\convertseven#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{7#1}{}#2S}%
+ \else
+ \xskiptofi{\converteight{#1}{#2}}%
+ \fi
+}
+
+\def\converteight#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{8#1}{}#2S}%
+ \else
+ \xskiptofi{\convertnine{#1}{#2}}%
+ \fi
+}
+
+\def\convertnine#1#2#3{%
+ \ifx#3S%
+ \xskiptofi{\convertzero{9#1}{}#2S}%
+ \else
+ \xskiptofi{\convertzero{#1}{#2#3}}%
+ \fi
+}
+
+% list evaluator
+
+\def\expander#1#2{%
+ \ifcat\noexpand#2\relax
+ \xskiptofi{\@xp@nder#1}%
+ \else
+ \ifx#2G%
+ \grabexpanderpostfix{#1}%
+ \else
+ \xskiptofifi{#1}%
+ \fi
+ \fi
+ #2%
+}
+
+\def\@xpander#1#2{%
+ \ifcat\noexpand#2\relax
+ \xskiptofi{\expandafter\expander\expandafter{\expandafter#1\expandafter}#2}%
+ \else
+ \xskiptofi{\@xpander{#1\expandafter#2}}%
+ \fi
+}
+
+\def\@xp@nder#1{%
+ \ifcat\noexpand#1\relax
+ \xskiptofi{\expandafter\expander\expandafter{\expandafter}}%
+ \else
+ \xskiptofi
+ \@xpander%
+ \fi
+ #1%
+}
+
+
+\def\grabexpanderpostfix#1\else#2\fi\fi G#3{%
+ \fi\fi\expander{#1#3}%
+}
+
+% the next two macros set up the multiplication and addition tables in the form of
+% \xdigit a b c which expands to the two digits of a\times b + c
+% and
+% \sdigit a b c which expands to the two digits of a + b + c
+% where c \in \{0, 1\}.
+% altogether there are 1200 sequences in use. this number can be
+% reduced to under 500 at the expence of more sophisticated
+% conditionals:
+% o in the case of \xdigit, a == 1 or b == 1 reduces \xdigit a b c to
+% \sdigit a c 0 (for b == 1), whereas a == 0 or b == 0 makes
+% \xdigit a b c {c}{0}, finally for a == 2 or b == 2, \xdigit a b c is
+% the same as \sdigit a a c (if b == 2); in addition, \xdigit a b 0
+% and \xdigit a b 1 are the same for all pairs (a,b) other than (3,3)
+% and (7,7); thus, the number of \xdigit sequences can be reduced to
+% 261 (by also requiring that a < b)
+% o similar techniques can be used to reduce the number of \sdigit
+% sequences necessary to under 60
+
+\def\setxdigitmachine{%
+ \tempca=0
+ \loop
+ \ifnum10>\tempca
+ \expandafter\setxdcs\expandafter0\expandafter0\the\tempca
+ \else
+ \ifnum100>\tempca
+ \expandafter\setxdcs\expandafter0\the\tempca
+ \else
+ \expandafter\setxdcs\the\tempca
+ \fi
+ \fi
+ \advance\tempca\@ne
+ \ifnum1000>\tempca
+ \repeat
+}
+
+\def\setsdigitmachine{%
+ \tempca=0
+ \loop
+ \ifnum10>\tempca
+ \expandafter\setsdcs\expandafter0\expandafter0\the\tempca
+ \else
+ \ifnum100>\tempca
+ \expandafter\setsdcs\expandafter0\the\tempca
+ \else
+ \expandafter\setsdcs\the\tempca
+ \fi
+ \fi
+ \advance\tempca\@ne
+ \ifnum200>\tempca
+ \repeat
+}
+
+% #1: carry
+% #2: the first summand
+% #3: the second summand
+
+% the result:
+% {sum digit}{new carry}
+
+\def\setsdcs#1#2#3{%
+ \tempcb=#2
+ \advance\tempcb#3
+ \advance\tempcb#1
+ \ifnum10>\tempcb
+ \expandafter\edef\csname sdigit#2#3#1\endcsname{\expandafter\parenthesize\expandafter0\the\tempcb}%
+ \else
+ \expandafter\edef\csname sdigit#2#3#1\endcsname{\expandafter\parenthesize\the\tempcb}%
+ \fi
+}
+
+% #1: the first multiplier
+% #2: the second multiplier
+% #3: carry
+
+% the result:
+% {product digit}{new carry}
+
+\def\setxdcs#1#2#3{%
+ \tempcb=#1
+ \multiply\tempcb#2
+ \advance\tempcb#3
+ \ifnum10>\tempcb
+ \expandafter\edef\csname xdigit#1#2#3\endcsname{\expandafter\parenthesize\expandafter0\the\tempcb}%
+ \else
+ \expandafter\edef\csname xdigit#1#2#3\endcsname{\expandafter\parenthesize\the\tempcb}%
+ \fi
+}
+
+\def\parenthesize#1#2{{#2}{#1}}
+
+\setxdigitmachine
+\setsdigitmachine
+
+% #1: carryover
+% #2: shift
+% #3: multiplier
+% #4: carry
+% #5: digits so far
+% #6: next digit
+
+\def\smallmultiply#1#2#3#4#5#6{%
+ \ifx#6F%
+ \ifx#40%
+ \yybreak@{\attachnxtnumber#1{#2#5}}%
+ \else
+ \yybreak@{\attachnxtnumber#1{#2#5#4}}%
+ \fi
+ \else
+ \yybreak{\expandafter\expandafter\expandafter
+ \sm@llmultiply\csname xdigit#3#6#4\endcsname{#1}{#2}{#3}{#5}}%
+ \yycontinue
+}
+
+\def\sm@llmultiply#1#2#3#4#5#6{%
+ \smallmultiply{#3}{#4}{#5}{#2}{#6#1}%
+}
+
+% carryover:
+% {number1}{number2}{shift}{product so far}
+
+% #1: number1
+% #2: number2
+% #3: shift
+% #4: product so far
+% #5; new number
+
+\def\attachnxtnumber#1#2#3#4#5{%
+ \startnxtproduct{#1}{#2}{#30}{#4#5F}#1%
+}
+
+% #1: number1
+% #2: number2
+% #3: shift
+% #4: product so far
+% #5; next digit
+
+\def\startnxtproduct#1#2#3#4#5{%
+ \ifx#5F%
+ \xskiptofi{\addmultiples#4G}%
+ \else
+ \xskiptofi{\expandafter\sm@llm@ltiply\expandafter{\expandafter{\eatone#1}{#2}{#3}{#4}}{#3}{#5}{0}{#2}}%
+ \fi
+}
+
+% #1: carryover
+% #2: shift
+% #3: multiplier
+% #4: carry
+% #5: number2
+% #6: remainder of the number
+
+\def\sm@llm@ltiply#1#2#3#4#5#6F{%
+ \smallmultiply{#1}{#2}{#3}{#4}{}#5%
+}
+
+\def\addmultiples#1F#2{%
+ \ifx#2G%
+ \xskiptofi{\postprocesssum{#1}}%
+ \else
+ \xskiptofi{\startnxtsum{#1}#2}%
+ \fi
+}
+
+\def\postprocesssum#1#2{%
+ #2{#1}%
+}
+
+% the summation macro below can be used for subtraction, as well,
+% using a well known 9-complement + 1 technique (compare two numbers,
+% take the complement of the smaller, add 1, add the results, remove
+% the first nonzero digit of the sum; the result of the comparison
+% determines the sign of the sum;
+
+\def\startnxtsum#1#2F{%
+ \startnxts@m{}{0}{#1}{#2}%
+}
+
+% #1: sum so far
+% #2: carry
+% #3: first number
+% #4: second number
+
+\def\startnxts@m#1#2#3#4{%
+ \ifx F#3F% the first number is exhausted
+ \ifx F#4F% both numbers are exhausted: finished
+ \yybreak@{\addmultiples#1#2F}%
+ \else % the second number is still non empty
+ \yybreak@{\makesimples@m{#1}{#2}0F#4F}%
+ \fi
+ \else
+ \ifx F#4F% the second number is exhausted
+ \yybreak@{\makesimples@m{#1}{#2}#3F0F}%
+ \else % both numbers are non empty
+ \yybreak@{\makesimples@m{#1}{#2}#3F#4F}%
+ \fi
+ \yycontinue
+}
+
+% #1: sum so far
+% #2: carry
+% #3: first digit
+% #4: rest of first number
+% #5: second digit
+% #6: rest of second number
+
+\def\makesimples@m#1#2#3#4F#5#6F{%
+ \expandafter\expandafter\expandafter\makesimpl@s@m\csname sdigit#3#5#2\endcsname{#1}{#4}{#6}%
+}
+
+% #1: digit
+% #2: carry
+% #3: sum so far
+% #4: first number
+% #5: second mumber
+
+\def\makesimpl@s@m#1#2#3#4#5{%
+ \startnxts@m{#3#1}{#2}{#4}{#5}%
+}
+
+% #1: prefix
+% #2: postfix
+% #3: digits
+
+\def\reversepp#1#2#3{%
+ \r@versepp{#1}{#2}{}#3R%
+}
+
+\def\r@versepp#1#2#3#4{%
+ \ifx#4R%
+ \xskiptofi{#1#3#2}%
+ \else
+ \xskiptofi{\r@versepp{#1}{#2}{#4#3}}%
+ \fi
+}
+
+\def\xmul#1#2{%
+ \reversepp{\xm@l}{F}{#2F#1}%
+}
+
+\def\xm@l#1F#2F{%
+ \startnxtproduct{#1F}{#2F}{}{}#1F{\reversepp{\eatzeros}{F}}%
+}
+
+\def\xsum#1#2{%
+ \reversepp{\addmultiples}{FG{\reversepp{\eatzeros}{F}}}{#2F#1}%
+}
+
+\def\eatzeros#1{% to remove zero carry digits
+ \ifx#10%
+ \yybreak\eatzeros
+ \else
+ \ifx#1F%
+ \yybreak@0%
+ \else
+ \yybreak@{\removepostfix#1}%
+ \fi
+ \yycontinue
+}
+
+\def\removepostfix#1F{#1}