-
Notifications
You must be signed in to change notification settings - Fork 2
/
DaaseDatabase.spad
225 lines (182 loc) · 6.5 KB
/
DaaseDatabase.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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
)abbrev domain DCMM DaaseCtorModeMap
DaaseCtorModeMap() : Exports == Implementation where
)include SpadTypeDefs.inc
Exports ==> Join(CoercibleTo(N), CoercibleTo(PF)) with
convert : SEX -> %
elt : (%, "name") -> Symbol
elt : (%, "type") -> N
elt : (%, "args") -> List(TD)
Implementation ==> add
Rep := Record(ctor : List(SEX), unused : SEX)
import SpadNode
import Printer
convert x ==
x pretend %
elt (x, "name") ==
symbol car x.ctor.1
elt (x, "type") ==
parse x.ctor.2
elt (x, "args") ==
ts := [parse t for t in rest(x.ctor, 2)]
as := [[symbol a] for a in destruct cdr x.ctor.1]
[[a, t]$TD for a in as for t in ts]
coerce x ==
ftor := bold hconcat [x.name :: PF, paren [arg :: PF for arg in x.args]]
pile [spaces [ftor, ":" :: PF], x.type :: PF]
)abbrev domain DOP DaaseOperation
DaaseOperation() : Exports == Implementation where
)include SpadTypeDefs.inc
Exports ==> CoercibleTo(PF) with
convert : SEX -> %
elt : (%, "name") -> Symbol
elt : (%, "type") -> MT
elt : (%, "signature") -> TD
elt : (%, "condition") -> N
coerce : % -> N
Implementation ==> add
import SpadNode
import Printer
Rep := Record(op_name : Symbol, op_info : List(List(SEX)))
convert x == x pretend %
elt (x, "name") ==
x.op_name
elt (x, "type") ==
sig := x.op_info.1
tl := [parse t for t in destruct sig.1]
if #sig >= 4 and symbol sig.4 = 'CONST then
tl := concat(tl, ['constant])
[rest tl, first tl]$MT
elt (x, "signature") ==
[[x.name], [x.type]]$TD
elt (x, "condition") ==
sig := x.op_info.1
#sig < 3 or (symbol? sig.3 and symbol sig.3 = 'T) => null
parse sig.3
coerce (x : %) : N ==
c := x.condition
t := nodeTypeDecl([x.name], [x.type])
null? c => t
nodeCondExpr(c, t, null)
coerce (x : %) : PF ==
cond := x.condition
null? cond => x.signature :: PF
pile [x.signature :: PF, spaces [bold("when" :: PF), cond :: PF]]
)abbrev domain DDB DaaseDatabase
DaaseDatabase() : Exports == Implementation where
)include SpadTypeDefs.inc
Exports ==> with
getOperationList : Symbol -> List DaaseOperation
getCtorArgs : Symbol -> List Symbol
++ returns constructor argument names
getCtorArgsKind : Symbol -> List Boolean
++ returns constructor argument kind: true when a type, false when a value
getCtorCategory : Symbol -> N
getCtorKind : Symbol -> Union("domain", "category", "package")
++ returns constructor kind
inDatabase? : Symbol -> Boolean
getCtorModeMap : Symbol -> DaaseCtorModeMap
safeGetCtorModeMap : Symbol -> Union(DaaseCtorModeMap, "failed")
getAbbrev : Symbol -> Symbol
getSourceFile : Symbol -> String
getSuperDomain : Symbol -> N
isSubDomain? : (Symbol, Symbol) -> Boolean
Implementation ==> add
import SExpression
import SpadNode
import Logger('Daase)
getOperationList t ==
-- Integer
sex : SEX := GETDATABASE(t, 'OPERATIONALIST)$Lisp
null? sex => error "Unknown constructor!"
opList := sex pretend List(SEX)
[convert op for op in reverse opList |
not(list? op and symbol? op.1 and (symbol op.1) = '_$unique)]
getCtorArgsKind t ==
sex : SEX := GETDATABASE(t,'COSIG)$Lisp
null? sex => error "Unknown constructor!"
(cdr sex) pretend List(Boolean)
getCtorCategory t ==
sex : SEX := GETDATABASE(t, 'CONSTRUCTORCATEGORY)$Lisp
null? sex => error "Unknown constructor!"
parse(sex)
inDatabase? t ==
sex : SEX := GETDATABASE(t, 'CONSTRUCTORMODEMAP)$Lisp
not null? sex
safeGetCtorModeMap t ==
sex : SEX := GETDATABASE(t, 'CONSTRUCTORMODEMAP)$Lisp
null? sex => "failed"
convert(sex)
getCtorModeMap t ==
cmm := safeGetCtorModeMap t
cmm case "failed" =>
fail ["Unknown constructor:" :: PrintableForm, bold(t :: PrintableForm)]
error ""
cmm
getCtorArgs t ==
sex : SEX := GETDATABASE(t, 'CONSTRUCTORARGS)$Lisp
sex pretend List(Symbol)
getCtorKind t ==
sex : SEX := GETDATABASE(t, 'CONSTRUCTORKIND)$Lisp
null? sex => error "Unknown constructor!"
kind := symbol sex
kind = 'domain => "domain"
kind = 'category => "category"
kind = 'package => "package"
error "Unknown constructor kind!"
getAbbrev t ==
sex : SEX := GETDATABASE(t, 'ABBREVIATION)$Lisp
null? sex => error "Unknown constructor!"
sex pretend Symbol
getSourceFile t ==
sex : SEX := GETDATABASE(t, 'SOURCEFILE)$Lisp
null? sex => error "Unknown constructor!"
sex pretend String
getSuperDomain t ==
sex : SEX := GETDATABASE(t, 'SUPERDOMAIN)$Lisp
null? sex => null
(domain, guard) := (sex.1, sex.2)
nodeTypeGuard(parse domain, parse guard.2)
isSubDomain?(s, t) ==
s = t => true
type := getSuperDomain(s)
while not null? type repeat
dom := (type :: TG).expr :: APP
s := dom.function :: Symbol
s = t => return true
type := getSuperDomain(s)
false
)abbrev package DDBT DaaseDatabaseTest
DaaseDatabaseTest() : Exports == Implementation where
)include SpadTypeDefs.inc
Exports ==> with
test1 : () -> Void
test2 : () -> Void
test3 : () -> Void
test4 : () -> Void
Implementation ==> add
import Printer
import DaaseDatabase
test1 () ==
printOps (s : Symbol) : Void ==
println pile([bold hconcat[s :: PF, ":" :: PF],
:[op :: PF for op in getOperationList(s)]])
printOps 'AbelianMonoid
printOps 'List
printOps 'BasicType
test2 () ==
println (getCtorModeMap('AbelianSemiGroup) :: PF)
println (getCtorModeMap('AbelianSemiGroup_&) :: PF)
println (getCtorModeMap('BasicType) :: PF)
println (getCtorModeMap('BasicType_&) :: PF)
println (getCtorModeMap('List) :: PF)
println (getCtorModeMap('PositiveInteger) :: PF)
test3() ==
-- TwoDimensionalArrayCategory(#1 : Type(),
-- #2 : FiniteLinearAggregate(t#1),
-- #3 : FiniteLinearAggregate(t#1))
println (getCtorModeMap('TwoDimensionalArrayCategory) :: PF)
test4() ==
println (isSubDomain?('Integer, 'Integer) :: PF)
println (isSubDomain?('NonNegativeInteger, 'Integer) :: PF)
println (isSubDomain?('PositiveInteger, 'NonNegativeInteger) :: PF)
println (isSubDomain?('PositiveInteger, 'Integer) :: PF)