/
ivar.spad
117 lines (103 loc) · 3.82 KB
/
ivar.spad
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
-------------------------------------------------------------------
---
--- IndexedVariable
--- Copyright (C) 2019-2020, Ralf Hemmecke <ralf@hemmecke.org>
---
-------------------------------------------------------------------
-- This program 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.
--
-- This program 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 this program. If not, see <http://www.gnu.org/licenses/>.
-------------------------------------------------------------------
)if LiterateDoc
\documentclass{article}
\usepackage{qeta}
\begin{document}
\title{Indexed variables}
\author{Ralf Hemmecke}
\date{22-Oct-2019}
\maketitle
\begin{abstract}
The domain \qetatype{IndexedVariable} is helper domain to represent
(infinitely many) variables that are ordered ascendingly by their
index.
\end{abstract}
\tableofcontents
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Implementation}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Helper macros}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
)endif
rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %
PP ==> PositiveInteger
ZZ ==> Integer
asPP x ==> x pretend PP
asZZ x ==> x pretend ZZ
)if LiterateDoc
%$
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{D IndexedVariable}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
)endif
)abbrev domain IVAR IndexedVariable
++ Author: Ralf Hemmecke
++ Description:
++ IndexedVariable(x) represents potentially infinitely many
++ variables, namely x1, x2, x3. etc. and orders them ascendingly like
++ the natural order of their indices.
IndexedVariable(v: String): Exports == Implementation where
Exports ==> Join(OrderedSet, ConvertibleTo Symbol) with
new: () -> %
++ new() returns a new (not yet used) variable.
rank: () -> ZZ
++ rank() returns the highest index of the currently known
++ variables. It returns 0 if no variables are known.
lookup: % -> PP
++ lookup(x) returns the index of the variable.
index: PP -> %
++ index(p) returns the variable v such that lookup(v) = p.
++ p > rank() all variables with numbers less than or equal to p
++ will internally be created and rank() will be updated..
Implementation ==> PP add
next: Reference ZZ := ref(1$ZZ)
syms: FlexibleArray Symbol := empty()
Rep ==> ZZ -- we only use positive integers (x>0)
rank(): ZZ ==
-- free next
deref(next) - 1
lookup(x: %): PP == asPP rep x
index(p: PP): % ==
z: ZZ := asZZ p
z < deref next => per z
-- Variable does not exist, create every variable with smaller
-- index.
while deref next < z repeat v: % := new()
return new()
new(): % ==
-- free next, syms
m: ZZ := deref next
s: String := concat(v, string m)
sym: Symbol := s::Symbol
concat!(syms, sym) -- destructively changes syms
setelt!(next, m+1)$Reference(ZZ)
per m
convert(x: %): Symbol == syms(rep x)
coerce(x: %): OutputForm ==
import from Symbol
(convert(x)@Symbol)::OutputForm
)if LiterateDoc
\end{document}
)endif