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
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
|
-- Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd.
-- All rights reserved.
-- Copyright (C) 2007-2011, Gabriel Dos Reis.
-- All rights reserved.
--
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are
-- met:
--
-- - Redistributions of source code must retain the above copyright
-- notice, this list of conditions and the following disclaimer.
--
-- - Redistributions in binary form must reproduce the above copyright
-- notice, this list of conditions and the following disclaimer in
-- the documentation and/or other materials provided with the
-- distribution.
--
-- - Neither the name of The Numerical Algorithms Group Ltd. nor the
-- names of its contributors may be used to endorse or promote products
-- derived from this software without specific prior written permission.
--
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
-- TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
-- PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
-- OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
import c_-util
import g_-cndata
namespace BOOT
--%
++ List of global attributes.
$Attributes := []
--%
++ Returns true if `a' is a category (runtime) object.
categoryObject?: %Thing -> %Boolean
categoryObject? a ==
vector? a and #a > 5 and vectorRef(a,3) = $Category
++ Return true if the form `x' designates an instantiaion of a
++ category constructor known to the global database or the
++ envronement `e'.
isCategoryForm: (%Form,%Env) -> %Boolean
isCategoryForm(x,e) ==
if x isnt [.,:.] then
x := macroExpand(x,e)
x isnt [.,:.] => ident? x and getmode(x,e) = $Category
getConstructorKind(x.op) is 'category -- FIXME: check arguments too.
++ Returns a freshly built category object for a domain or package
++ (as indicated by `domainOrPackage'), with signature list
++ designated by `sigList', attribute list designated by `attList',
++ used domains list designated by `domList', and a princical ancestor
++ category object designated by `principal'.
mkCategory: (%ConstructorKind,%List %Sig,%List %Form,%List %Instantiation, %Maybe %Shell) -> %Shell
mkCategory(domainOrPackage,sigList,attList,domList,principal) ==
NSigList := nil
-- Unless extending a principal ancestor (from the end), start
-- from the first free, unencumbered slot.
count :=
principal = nil => $NRTbase
#principal
sigList:=
[if s is [sig,pred]
then
-- Don't retain duplicate signatures.
-- ??? Should we not check for predicate subsumption too?
or/[x is [[ =sig,.,:impl],:num] for x in NSigList] => [sig,pred,:impl]
--only needed for multiple copies of sig
num :=
domainOrPackage is "domain" => count
count-5
nsig := mkOperatorEntry(sig,pred,num)
NSigList := [[nsig,:count],:NSigList]
count := count+1
nsig
else s for s in sigList]
NewLocals:= nil
for s in sigList repeat
NewLocals:= union(NewLocals,Prepare s.mmTarget) where
Prepare u == "union"/[Prepare2 v for v in u]
Prepare2 v ==
v is '$ => nil
string? v => nil
v isnt [.,:.] => [v]
v.op is 'Union =>
"union"/[Prepare2 x for x in stripUnionTags v.args]
v.op is 'Mapping => "union"/[Prepare2 x for x in v.args]
v.op is 'Record => "union"/[Prepare2 third x for x in v.args]
v.op is 'Enumeration => nil
[v]
OldLocals:= nil
-- Remove possible duplicate local domain caches.
if principal then
for u in (OldLocals := categoryLocals principal) repeat
NewLocals := remove(NewLocals,first u)
-- New local domains caches are hosted in slots at the end onward
for u in NewLocals repeat
OldLocals := [[u,:count],:OldLocals]
count := count+1
-- Build a fresh category object stuffed with all updated information
v := newShell count
canonicalForm(v) := nil
categoryExports(v) := sigList
categoryAttributes(v) := attList
categoryRef(v,3) := $Category
if principal ~= nil then
for x in 6..#principal-1 repeat
categoryRef(v,x) := categoryRef(principal,x)
categoryAssociatedTypes(v) :=
[categoryPrincipals principal,
categoryAncestors principal,
OldLocals]
else
categoryAssociatedTypes(v) := [nil,nil,OldLocals]
categoryRef(v,5) := domList
for [nsig,:n] in NSigList repeat
categoryRef(v,n) := nsig
v
--% Subsumption code (for operators)
DropImplementations a ==
a is [sig,pred,[q,:.]] and q in '(ELT CONST) =>
q = "ELT" => [sig,pred]
[[:sig,'constant],pred]
a
SigListUnion(extra,original,principal) ==
--augments original %with everything in extra that is not in original
for (o:=[[ofn,osig,:.],opred,:.]) in original repeat
-- The purpose of this loop is to detect cases when the
-- original list contains, e.g. ** with NonNegativeIntegers, and
-- the extra list would like to add ** with PositiveIntegers.
-- The PI map is therefore gives an implementation of "Subsumed"
for x in SigListOpSubsume(o,extra) repeat
[[xfn,xsig,:.],xpred,:.] := x
symbolEq?(xfn,ofn) and xsig = osig =>
--checking name and signature, but not a 'constant' marker
xpred = opred => extra := remove(extra,x)
--same signature and same predicate
opred = true => extra := remove(extra,x)
-- PRETTYPRINT ("we ought to subsume",x,o)
not MachineLevelSubsume(first o,first x) =>
'"Source level subsumption not implemented"
extra := remove(extra,x)
for e in extra repeat
[esig,epred,:.]:= e
eimplem:=[]
for x in SigListOpSubsume(e,original) repeat
--PRETTYPRINT(LIST("SigListOpSubsume",e,x))
not MachineLevelSubsume(first e,first x) =>
--systemError '"Source level subsumption not implemented"
original:= [e,:original]
return nil -- this exits from the innermost for loop
original := remove(original,x)
[xsig,xpred,:ximplem]:= x
-- if xsig ~= esig then -- not quite strong enough
if first xsig ~= first esig or second xsig ~= second esig then
-- the new version won't get confused by "constant"markers
if ximplem is [["Subsumed",:.],:.] then
original := [x,:original]
else
original:= [[xsig,xpred,["Subsumed",:esig]],:original]
else epred := mkOr(epred,xpred,$e)
-- this used always to be done, as noted below, but that's not safe
if not(ximplem is [["Subsumed",:.],:.]) then eimplem:= ximplem
if eimplem then esig:=[first esig,second esig]
-- in case there's a constant marker
e:= [esig,epred,:eimplem]
-- e:= [esig,mkOr(xpred,epred,$e),:ximplem]
-- Original version -gets it wrong if the new operator is only
-- present under certain conditions
-- We must pick up the previous implementation, if any
--+
if ximplem is [[q,.,index]] and integer? index and (q="ELT" or q="CONST")
then bufferRef(principal,index) := e
original:= [e,:original]
original
mkOr: (%Form,%Form,%Env) -> %Form
mkOr(a,b,e) ==
a=true => true
b=true => true
b=a => a
l:=
a is ["OR",:a'] =>
(b is ["OR",:b'] => union(a',b'); mkOr2(b,a',e) )
b is ["OR",:b'] => mkOr2(a,b',e)
(a is ["has",avar,acat]) and (b is ["has",=avar,bcat]) =>
descendant?(acat,bcat,e) => [b]
descendant?(bcat,acat,e) => [a]
[a,b]
a is ['AND,:a'] and listMember?(b,a') => [b]
b is ['AND,:b'] and listMember?(a,b') => [a]
a is ["and",:a'] and listMember?(b,a') => [b]
b is ["and",:b'] and listMember?(a,b') => [a]
[a,b]
#l = 1 => first l
["OR",:l]
mkOr2: (%Form,%Form,%Env) -> %Form
mkOr2(a,b,e) ==
--a is a condition, "b" a list of them
listMember?(a,b) => b
a is ["has",avar,acat] =>
aRedundant:=false
for c in b | c is ["has",=avar,ccat] repeat
descendant?(acat,ccat,e) =>
return (aRedundant:=true)
if descendant?(ccat,acat,e) then b := remove(b,c)
aRedundant => b
[a,:b]
[a,:b]
mkAnd: (%Form,%Form,%Env) -> %Form
mkAnd(a,b,e) ==
a=true => b
b=true => a
b=a => a
l:=
a is ["AND",:a'] =>
(b is ["AND",:b'] => union(a',b'); mkAnd2(b,a',e) )
b is ["AND",:b'] => mkAnd2(a,b',e)
(a is ["has",avar,acat]) and (b is ["has",=avar,bcat]) =>
descendant?(acat,bcat,e) => [a]
descendant?(bcat,acat,e) => [b]
[a,b]
[a,b]
#l = 1 => first l
["AND",:l]
mkAnd2: (%Form,%Form,%Env) -> %Form
mkAnd2(a,b,e) ==
--a is a condition, "b" a list of them
listMember?(a,b) => b
a is ["has",avar,acat] =>
aRedundant:=false
for c in b | c is ["has",=avar,ccat] repeat
descendant?(ccat,acat,e) =>
return (aRedundant:=true)
if descendant?(acat,ccat,e) then b := remove(b,c)
aRedundant => b
[a,:b]
[a,:b]
++ Return true if `a implies b' in the logical sense.
predicateImplies(a,b) ==
b is true => true
a is true => false
a = b -- for now.
SigListOpSubsume([[name1,sig1,:.],:.],list) ==
--does m subsume another operator in the list?
--see "operator subsumption" in JHD's report
--if it does, returns the subsumed member
lsig1 := #sig1
ans := []
for (n:=[[name2,sig2,:.],:.]) in list | symbolEq?(name1,name2) repeat
lsig1 = #sig2 and sig1 = sig2 => ans := [n,:ans]
return ans
MachineLevelSubsume([name1,[out1,:in1],:flag1],[name2,[out2,:in2],:flag2]) ==
-- Checks for machine-level subsumption
-- true if the first signature subsumes the second
-- flag1 = flag2 and: this really should be checked, but
symbolEq?(name1,name2) and MachineLevelSubset(out1,out2) and
(and/[MachineLevelSubset(inarg2,inarg1) for inarg1 in in1 for inarg2 in in2]
)
MachineLevelSubset(a,b) ==
--true if a is a machine-level subset of b
a=b => true
b is ["Union",:blist] and listMember?(a,blist) and
(and/[string? x for x in blist | x~=a]) => true
--all other branches must be distinct objects
not null isSubDomain(a,b)
--we assume all subsets are true at the machine level
--% Ancestor chasing code
++ Subroutine of JoinInner.
++ Given a list `l' of 2-list [cat,pred] of category object and associated
++ predicate, return a list of similar structures of all fundamental
++ ancestors with appropriate conditions.
FindFundAncs(l,e) ==
l = nil => nil
[hd:=[f1,p1],:l] := l
canonicalForm f1 = nil => FindFundAncs(l,e)
ans := FindFundAncs(l,e)
for u in FindFundAncs([[CatEval(first x,e),mkAnd(p1,second x,e)]
for x in categoryAncestors f1],e) repeat
x := objectAssoc(first u,ans) =>
ans := [[first u,mkOr(second x,second u,e)],:remove(ans,x)]
ans := [u,:ans]
--testing to see if hd is already there
x := objectAssoc(f1,ans) => [[f1,mkOr(p1,second x,e)],:remove(ans,x)]
p1 is true =>
for x in categoryPrincipals f1 repeat
if y := objectAssoc(CatEval(x,e),ans) then ans := remove(ans,y)
[hd,:ans]
for x in categoryPrincipals f1 repeat
if y := objectAssoc(CatEval(x,e),ans) then ans:=
[[first y,mkOr(p1,second y,e)],:remove(ans,y)]
[hd,:ans]
-- Our new thing may have, as an alternate view, a principal
-- descendant of something previously added which is therefore
-- subsumed
CatEval: (%Thing,%Env) -> %Shell
CatEval(x,e) ==
vector? x => x
if $InteractiveMode then
e := $CategoryFrame
compMakeCategoryObject(x,e).expr
ancestor?: (%Form,%List %Instantiation,%Env) -> %Form
ancestor?(xname,leaves,env) ==
-- checks for being a principal ancestor of one of the leaves
listMember?(xname,leaves) => xname
for y in leaves repeat
listMember?(xname,categoryPrincipals CatEval(y,env)) => return y
CondAncestorP(xname,leaves,condition,env) ==
-- checks for being a principal ancestor of one of the leaves
for u in leaves repeat
u':=first u
ucond:=
null rest u => true
second u
xname = u' or listMember?(xname,categoryPrincipals CatEval(u',env)) =>
predicateImplies(condition,ucond) => return u'
++ Returns true if the form `a' designates a category that is any
++ kind of descendant of the category designated by the form `b'.
descendant?: (%Form,%Form,%Env) -> %Boolean
descendant?(a,b,e) ==
a=b => true
a is ["ATTRIBUTE",:.] => false
a is ["SIGNATURE",:.] => false
a:= CatEval(a,e)
b is ["ATTRIBUTE",b'] =>
(l := assoc(b',categoryAttributes a)) => TruthP second l
listMember?(b,categoryPrincipals a) => true
ancestor?(b,[first u for u in categoryAncestors a],e) => true
false
--% The implementation of Join
++ We have a list `l' of category objects to be joined.
++ Some of them may harbor other categories that exist only under
++ certain conditions. Collect all those that are indisputably conditional
++ and attempt to detect those apparent conditional categories whose
++ predicates are satified in the current elaboration environment.
++ The end result is a 2-list, the first component being a list of
++ (catobj,pred) pairs and the second component being the list of
++ newly discovered unconditional categories.
filterConditionalCategories(l,e) ==
conditionals := nil
unconditionals := nil
for cat in l repeat
for [at,pred] in categoryAttributes cat repeat
if at isnt [.,:.] then at := [at]
-- the variable $Attributes is built globally, so that true
-- attributes can be detected without calling isCategoryForm
symbolMember?(first at,$Attributes) => nil
not isCategoryForm(at,e) => $Attributes := [first at,:$Attributes]
listMember?(pred,get("$Information","special",e)) =>
--It's true, so we add it as unconditional
unconditionals := [CatEval(at,e),:unconditionals]
pred isnt ["and",:.] =>
conditionals := [[CatEval(at,e),pred],:conditionals]
pred' := [x for x in pred.args |
not listMember?(x,get("$Information","special",e))
and x isnt true]
pred' = nil => unconditionals := [CatEval(at,e),:unconditionals]
pred' is [.] => conditionals := [[CatEval(at,e),pred'],:conditionals]
conditionals := [[CatEval(at,e),["and",:pred']],:conditionals]
[conditionals,reverse! unconditionals]
JoinInner(l,$e) ==
[CondList,uncondList] := filterConditionalCategories(l,$e)
[principal,:l] := [:l,:uncondList]
principal := mkBuffer principal
l' := [:CondList,:[[u,true] for u in l]]
-- This is a list of all the categories that this extends
-- conditionally or unconditionally
sigl := categoryExports bufferData principal
attl := categoryAttributes bufferData principal
globalDomains := categoryParameters bufferData principal
FundamentalAncestors := categoryAncestors bufferData principal
if name := canonicalForm bufferData principal then
FundamentalAncestors := [[name],:FundamentalAncestors]
-- this skips buggy code which discards needed categories
for [b,condition] in FindFundAncs(l',$e) | bname := b.0 repeat
CondAncestorP(bname,FundamentalAncestors,condition,$e) => nil
f := ancestor?(bname,[first u for u in FundamentalAncestors],$e) =>
[.,.,index] := assoc(f,FundamentalAncestors)
FundamentalAncestors := [[bname,condition,index],:FundamentalAncestors]
PrinAncb := categoryPrincipals CatEval(bname,$e)
--Principal Ancestors of b
reallynew := true
-- This loop implements Category Subsumption
for anc in FundamentalAncestors | listMember?(first anc,PrinAncb) repeat
if rest anc then
anccond := second anc
ancindex := third anc
else
anccond := true
ancindex := nil
if predicateImplies(anccond,condition) then
FundamentalAncestors :=
-- the new 'b' is more often true than the old one 'anc'
[[bname,condition,ancindex],:remove(FundamentalAncestors,anc)]
else if ancindex then
--the new 'b' is less often true
newentry := [bname,condition,ancindex]
if not listMember?(newentry,FundamentalAncestors) then
FundamentalAncestors := [newentry,:FundamentalAncestors]
else ancindex := nil
if ancindex then
bufferRef(principal,ancindex) := bname
reallynew := false
if reallynew then
n := bufferLength principal
FundamentalAncestors := [[b.0,condition,n],:FundamentalAncestors]
resizeBuffer(principal,n + 1)
bufferRef(principal,n) := b.0
for b in l repeat
sigl := SigListUnion([DropImplementations u for u in categoryExports b],
sigl,principal)
attl := S_+(categoryAttributes b,attl)
globalDomains := [:globalDomains,:S_-(categoryParameters b,globalDomains)]
for b in CondList repeat
newpred := second b
for u in categoryAttributes first b repeat
v := assoc(first u,attl)
null v =>
attl :=
second u is true => [[first u,newpred],:attl]
[[first u,["and",newpred,second u]],:attl]
second v is true => nil
attl := remove(attl,v)
attl :=
second u is true => [[first u,mkOr(second v,newpred,$e)],:attl]
[[first u,mkOr(second v,mkAnd(newpred,second u,$e),$e)],:attl]
sigl := SigListUnion(
[AddPredicate(DropImplementations u,newpred)
for u in categoryExports(first b)],sigl,principal) where
AddPredicate(op is [sig,oldpred,:implem],newpred) ==
newpred is true => op
oldpred is true => [sig,newpred,:implem]
[sig,mkpf([oldpred,newpred],"and"),:implem]
FundamentalAncestors := [x for x in FundamentalAncestors | rest x]
--strip out the pointer to Principal Ancestor
c := categoryPrincipals bufferData principal
pName := canonicalForm bufferData principal
if pName and not listMember?(pName,c) then c := [pName,:c]
categoryAssociatedTypes(bufferData principal) :=
[c,FundamentalAncestors,categoryLocals bufferData principal]
mkCategory("domain",sigl,attl,globalDomains,bufferToVector principal)
Join(:l) ==
e :=
null $e or $InteractiveMode => $CategoryFrame
$e
JoinInner(l, e)
|