Bug Summary

File:src/tfsat.c
Warning:line 1508, column 10
Value stored to 'res' during its initialization is never read

Annotated Source Code

Press '?' to see keyboard shortcuts

clang -cc1 -cc1 -triple x86_64-unknown-linux-gnu -analyze -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name tfsat.c -analyzer-checker=core -analyzer-checker=apiModeling -analyzer-checker=unix -analyzer-checker=deadcode -analyzer-checker=security.insecureAPI.UncheckedReturn -analyzer-checker=security.insecureAPI.getpw -analyzer-checker=security.insecureAPI.gets -analyzer-checker=security.insecureAPI.mktemp -analyzer-checker=security.insecureAPI.mkstemp -analyzer-checker=security.insecureAPI.vfork -analyzer-checker=nullability.NullPassedToNonnull -analyzer-checker=nullability.NullReturnedFromNonnull -analyzer-output plist -w -setup-static-analyzer -mrelocation-model pic -pic-level 2 -pic-is-pie -mframe-pointer=all -fmath-errno -ffp-contract=on -fno-rounding-math -mconstructor-aliases -funwind-tables=2 -target-cpu x86-64 -tune-cpu generic -debugger-tuning=gdb -fdebug-compilation-dir=/home/kfp/aldor/aldor/aldor/src -fcoverage-compilation-dir=/home/kfp/aldor/aldor/aldor/src -resource-dir /usr/local/lib/clang/18 -D PACKAGE_NAME="aldor" -D PACKAGE_TARNAME="aldor" -D PACKAGE_VERSION="1.4.0" -D PACKAGE_STRING="aldor 1.4.0" -D PACKAGE_BUGREPORT="aldor@xinutec.org" -D PACKAGE_URL="" -D PACKAGE="aldor" -D VERSION="1.4.0" -D YYTEXT_POINTER=1 -D HAVE_STDIO_H=1 -D HAVE_STDLIB_H=1 -D HAVE_STRING_H=1 -D HAVE_INTTYPES_H=1 -D HAVE_STDINT_H=1 -D HAVE_STRINGS_H=1 -D HAVE_SYS_STAT_H=1 -D HAVE_SYS_TYPES_H=1 -D HAVE_UNISTD_H=1 -D STDC_HEADERS=1 -D HAVE_LIBREADLINE=1 -D HAVE_READLINE_READLINE_H=1 -D HAVE_READLINE_HISTORY=1 -D HAVE_READLINE_HISTORY_H=1 -D USE_GLOOP_SHELL=1 -D GENERATOR_COROUTINES=0 -D HAVE_DLFCN_H=1 -D LT_OBJDIR=".libs/" -I . -D VCSVERSION="2c53e759f1e00e345f8b172e7139debda72fda13" -internal-isystem /usr/local/lib/clang/18/include -internal-isystem /usr/local/include -internal-isystem /usr/lib/gcc/x86_64-linux-gnu/14/../../../../x86_64-linux-gnu/include -internal-externc-isystem /usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-externc-isystem /usr/include -O0 -Wno-empty-body -Wno-enum-compare -Wno-missing-field-initializers -Wno-unused -Wno-unused-parameter -Wno-error=format -Wno-error=type-limits -Wno-error=strict-aliasing -Wno-sign-compare -Wno-error=shift-negative-value -Wno-error=clobbered -std=c99 -ferror-limit 19 -fgnuc-version=4.2.1 -fskip-odr-check-in-gmf -analyzer-output=html -faddrsig -D__GCC_HAVE_DWARF2_CFI_ASM=1 -o /tmp/scan-build-2026-01-15-223856-845667-1 -x c tfsat.c
1/*****************************************************************************
2 *
3 * tfsat.c: Type form satisfaction.
4 *
5 * Copyright (c) 1990-2007 Aldor Software Organization Ltd (Aldor.org).
6 *
7 ****************************************************************************/
8
9#include "ablogic.h"
10#include "absub.h"
11#include "axlobs.h"
12#include "comsg.h"
13#include "debug.h"
14#include "format.h"
15#include "ostream.h"
16#include "sefo.h"
17#include "tconst.h"
18#include "tfsat.h"
19#include "tposs.h"
20#include "spesym.h"
21#include "stab.h"
22#include "store.h"
23#include "terror.h"
24#include "ti_top.h"
25#include "util.h"
26
27Bool tfsDebug = false((int) 0);
28Bool tfsMultiDebug = false((int) 0);
29Bool tfsExportDebug = false((int) 0);
30Bool tfsParentDebug = false((int) 0);
31
32#define tfsDEBUGif (!tfsDebug) { } else afprintf DEBUG_IF(tfs)if (!tfsDebug) { } else afprintf
33#define tfsMultiDEBUGif (!tfsMultiDebug) { } else afprintf DEBUG_IF(tfsMulti)if (!tfsMultiDebug) { } else afprintf
34#define tfsExportDEBUGif (!tfsExportDebug) { } else afprintf DEBUG_IF(tfsExport)if (!tfsExportDebug) { } else afprintf
35#define tfsParentDEBUGif (!tfsParentDebug) { } else afprintf DEBUG_IF(tfsParent)if (!tfsParentDebug) { } else afprintf
36
37static int tfsDepthNo;
38static int tfsSerialNo;
39
40extern void tiBottomUp (Stab, AbSyn, TForm);
41extern void tiTopDown (Stab, AbSyn, TForm);
42extern Bool tiUnaryToRaw (Stab, AbSyn, TForm);
43extern Bool tiRawToUnary (Stab, AbSyn, TForm);
44extern Stab stabFindLevel (Stab, Syme);
45
46/*
47 * Naming convention:
48 * S - source type
49 * T - target type
50 */
51
52/******************************************************************************
53 *
54 * :: Type form satisfaction flags.
55 *
56 *****************************************************************************/
57
58/*
59 * (operation modes)
60 * TFS_Probe Allow side-fx w/o changing state.
61 * TFS_Commit Perform side-fx operations.
62 * TFS_Missing Collect missing exports.
63 * TFS_Sigma Just collect the substitution.
64 * TFS_Conditions Allow use of abCondKnown
65 *
66 * (type form embeddings)
67 * TFS_Pending Pending T -> T
68 * TFS_AnyToNone S -> ()
69 * TFS_Sefo S -> T
70 *
71 * TFS_CrossToTuple Cross(A, ..., A) -> Tuple(A)
72 * TFS_CrossToMulti Cross(A, ..., B) -> (A, ..., B)
73 * TFS_CrossToUnary Cross(S) -> S
74 * TFS_MultiToTuple (A, ..., A) -> Tuple(A)
75 * TFS_MultiToCross (A, ..., B) -> Cross(A, ..., B)
76 * TFS_MultiToUnary (S) -> S
77 * TFS_UnaryToTuple S -> Tuple(S)
78 * TFS_UnaryToCross S -> Cross(S)
79 * TFS_UnaryToMulti S -> (S)
80 *
81 * (error return modes)
82 * TFS_Fail
83 * TFS_ExportsMissing
84 * TFS_EmbedFail
85 * TFS_ArgMissing
86 * TFS_BadArgType
87 * TFS_DifferentArity
88 */
89
90/*!! Remember to update tfSatAbEmbed when these change. */
91struct maskInfo {
92 String name;
93};
94struct maskInfo tfSatMaskInfo[] = {
95 {"Probe"},
96 {"Commit"},
97 {"Missing"},
98 {"Sigma"},
99 {"Info"},
100 {"Conditions"},
101 {"Pending"},
102 {"AnyToNone"},
103 {"Sefo"},
104 {"CrossToTuple"},
105 {"CrossToMulti"},
106 {"CrossToUnary"},
107 {"MultiToTuple"},
108 {"MultiToCross"},
109 {"MultiToUnary"},
110 {"UnaryToTuple"},
111 {"UnaryToCross"},
112 {"UnaryToMulti"},
113 {"Fail"},
114 {"ExportsMissing"},
115 {"EmbedFail"},
116 {"ArgMissing"},
117 {"BadArgType"},
118 {"DifferentArity"},
119 {NULL((void*)0)}
120};
121
122#define TFS_Succeed((SatMask) 0) ((SatMask) 0)
123
124#define TFS_Probe(((SatMask) 1) << 0) (((SatMask) 1) << 0)
125#define TFS_Commit(((SatMask) 1) << 1) (((SatMask) 1) << 1)
126#define TFS_Missing(((SatMask) 1) << 2) (((SatMask) 1) << 2)
127#define TFS_Sigma(((SatMask) 1) << 3) (((SatMask) 1) << 3)
128#define TFS_Info(((SatMask) 1) << 4) (((SatMask) 1) << 4)
129#define TFS_Conditions(((SatMask) 1) << 5) (((SatMask) 1) << 5)
130
131#define TFS_Pending(((SatMask) 1) << 6) (((SatMask) 1) << 6)
132#define TFS_AnyToNone(((SatMask) 1) << 7) (((SatMask) 1) << 7)
133#define TFS_Sefo(((SatMask) 1) << 8) (((SatMask) 1) << 8)
134
135#define TFS_EmbedShift9 9
136#define TFS_CrossToTuple(((SatMask) 1) << 9) (((SatMask) 1) << 9)
137#define TFS_CrossToMulti(((SatMask) 1) << 10) (((SatMask) 1) << 10)
138#define TFS_CrossToUnary(((SatMask) 1) << 11) (((SatMask) 1) << 11)
139#define TFS_MultiToTuple(((SatMask) 1) << 12) (((SatMask) 1) << 12)
140#define TFS_MultiToCross(((SatMask) 1) << 13) (((SatMask) 1) << 13)
141#define TFS_MultiToUnary(((SatMask) 1) << 14) (((SatMask) 1) << 14)
142#define TFS_UnaryToTuple(((SatMask) 1) << 15) (((SatMask) 1) << 15)
143#define TFS_UnaryToCross(((SatMask) 1) << 16) (((SatMask) 1) << 16)
144#define TFS_UnaryToMulti(((SatMask) 1) << 17) (((SatMask) 1) << 17)
145
146#define TFS_Fail(((SatMask) 1) << 18) (((SatMask) 1) << 18)
147#define TFS_ExportsMissing(((SatMask) 1) << 19) (((SatMask) 1) << 19)
148#define TFS_EmbedFail(((SatMask) 1) << 20) (((SatMask) 1) << 20)
149#define TFS_ArgMissing(((SatMask) 1) << 21) (((SatMask) 1) << 21)
150#define TFS_BadArgType(((SatMask) 1) << 22) (((SatMask) 1) << 22)
151#define TFS_DifferentArity(((SatMask) 1) << 23) (((SatMask) 1) << 23)
152
153
154#define TFS_BitsWidth24 24
155#define TFS_BitsMask((((SatMask) 1) << 24) - 1) ((((SatMask) 1) << TFS_BitsWidth24) - 1)
156
157#define TFS_ModeMask( (((SatMask) 1) << 0) | (((SatMask) 1) << 1) | (
((SatMask) 1) << 2) | (((SatMask) 1) << 3) | (((SatMask
) 1) << 4) ) (\
158 TFS_Probe(((SatMask) 1) << 0) | \
159 TFS_Commit(((SatMask) 1) << 1) | \
160 TFS_Missing(((SatMask) 1) << 2) | \
161 TFS_Sigma(((SatMask) 1) << 3) | \
162 TFS_Info(((SatMask) 1) << 4) )
163
164#define TFS_EmbedMask( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) (\
165 TFS_Pending(((SatMask) 1) << 6) | \
166 TFS_AnyToNone(((SatMask) 1) << 7) | \
167 TFS_Sefo(((SatMask) 1) << 8) | \
168 TFS_CrossToTuple(((SatMask) 1) << 9) | \
169 TFS_CrossToMulti(((SatMask) 1) << 10) | \
170 TFS_CrossToUnary(((SatMask) 1) << 11) | \
171 TFS_MultiToTuple(((SatMask) 1) << 12) | \
172 TFS_MultiToCross(((SatMask) 1) << 13) | \
173 TFS_MultiToUnary(((SatMask) 1) << 14) | \
174 TFS_UnaryToTuple(((SatMask) 1) << 15) | \
175 TFS_UnaryToCross(((SatMask) 1) << 16) | \
176 TFS_UnaryToMulti(((SatMask) 1) << 17) )
177
178#define TFS_ErrorMask( (((SatMask) 1) << 18) | (((SatMask) 1) << 19) |
(((SatMask) 1) << 20) | (((SatMask) 1) << 21) | (
((SatMask) 1) << 22) | (((SatMask) 1) << 23) ) (\
179 TFS_Fail(((SatMask) 1) << 18) | \
180 TFS_ExportsMissing(((SatMask) 1) << 19) | \
181 TFS_EmbedFail(((SatMask) 1) << 20) | \
182 TFS_ArgMissing(((SatMask) 1) << 21) | \
183 TFS_BadArgType(((SatMask) 1) << 22) | \
184 TFS_DifferentArity(((SatMask) 1) << 23) )
185
186#define TFS_ParnMask(~((((SatMask) 1) << 24) - 1)) (~TFS_BitsMask((((SatMask) 1) << 24) - 1))
187
188#define tfsParNBits(n)(((SatMask) (n)) << 24) (((SatMask) (n)) << TFS_BitsWidth24)
189
190#define TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) (TFS_EmbedMask( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~TFS_Sefo(((SatMask) 1) << 8))
191#define TFS_NPendingMask((( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) |
(((SatMask) 1) << 8) | (((SatMask) 1) << 9) | ((
(SatMask) 1) << 10) | (((SatMask) 1) << 11) | (((
SatMask) 1) << 12) | (((SatMask) 1) << 13) | (((SatMask
) 1) << 14) | (((SatMask) 1) << 15) | (((SatMask)
1) << 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) & ~(((SatMask) 1) << 6)) (TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) & ~TFS_Pending(((SatMask) 1) << 6))
192#define TFS_NAnyToNoneMask((( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) |
(((SatMask) 1) << 8) | (((SatMask) 1) << 9) | ((
(SatMask) 1) << 10) | (((SatMask) 1) << 11) | (((
SatMask) 1) << 12) | (((SatMask) 1) << 13) | (((SatMask
) 1) << 14) | (((SatMask) 1) << 15) | (((SatMask)
1) << 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) & ~(((SatMask) 1) << 7)) (TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) & ~TFS_AnyToNone(((SatMask) 1) << 7))
193
194#define tfSatMode(m)((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) ((m) & TFS_ModeMask( (((SatMask) 1) << 0) | (((SatMask) 1) << 1) | (
((SatMask) 1) << 2) | (((SatMask) 1) << 3) | (((SatMask
) 1) << 4) ))
195#define tfSatEmbed(m)((m) & ( (((SatMask) 1) << 6) | (((SatMask) 1) <<
7) | (((SatMask) 1) << 8) | (((SatMask) 1) << 9)
| (((SatMask) 1) << 10) | (((SatMask) 1) << 11) |
(((SatMask) 1) << 12) | (((SatMask) 1) << 13) | (
((SatMask) 1) << 14) | (((SatMask) 1) << 15) | ((
(SatMask) 1) << 16) | (((SatMask) 1) << 17) )) ((m) & TFS_EmbedMask( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ))
196#define tfSatError(m)((m) & ( (((SatMask) 1) << 18) | (((SatMask) 1) <<
19) | (((SatMask) 1) << 20) | (((SatMask) 1) << 21
) | (((SatMask) 1) << 22) | (((SatMask) 1) << 23)
)) ((m) & TFS_ErrorMask( (((SatMask) 1) << 18) | (((SatMask) 1) << 19) |
(((SatMask) 1) << 20) | (((SatMask) 1) << 21) | (
((SatMask) 1) << 22) | (((SatMask) 1) << 23) ))
197#define tfSatParn(m)((m) & (~((((SatMask) 1) << 24) - 1))) ((m) & TFS_ParnMask(~((((SatMask) 1) << 24) - 1)))
198
199#define tfSatProbe(m)((m) & (((SatMask) 1) << 0)) ((m) & TFS_Probe(((SatMask) 1) << 0))
200#define tfSatCommit(m)((m) & (((SatMask) 1) << 1)) ((m) & TFS_Commit(((SatMask) 1) << 1))
201#define tfSatMissing(m)((m) & (((SatMask) 1) << 2)) ((m) & TFS_Missing(((SatMask) 1) << 2))
202#define tfSatSigma(m)((m) & (((SatMask) 1) << 3)) ((m) & TFS_Sigma(((SatMask) 1) << 3))
203#define tfSatInfo(m)((m) & (((SatMask) 1) << 4)) ((m) & TFS_Info(((SatMask) 1) << 4))
204#define tfSatUseConditions(m)((m) & (((SatMask) 1) << 5)) ((m) & TFS_Conditions(((SatMask) 1) << 5))
205
206#define tfSatAllow(m,c)((m) & (c)) ((m) & (c))
207
208#define tfSatResult(m,c)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (c)) (tfSatMode(m)((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (c))
209#define tfSatParNFail(m, r, n)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (r) | (((SatMask) (n)) <<
24)) (tfSatMode(m)((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (r) | tfsParNBits(n)(((SatMask) (n)) << 24))
210
211
212#define tfSatTrue(m)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0))) tfSatResult(m, TFS_Succeed)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)))
213#define tfSatFalse(m)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
))) tfSatResult(m, TFS_Fail)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)))
214
215#define tfSatInner(m)(((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((m) & ((((SatMask) 1)
<< 6)))) \
216 (tfSatMode(m)((m) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | tfSatAllow(m, TFS_Pending)((m) & ((((SatMask) 1) << 6))))
217
218
219/******************************************************************************
220 *
221 * :: Local declarations.
222 *
223 *****************************************************************************/
224
225localstatic SatMask tfSatArgPoss (SatMask, AbSyn S, TForm T);
226localstatic SatMask tfSatArg (SatMask, AbSyn, TForm);
227
228
229localstatic SatMask tfSatDOM (SatMask, TForm S);
230localstatic SatMask tfSatCAT (SatMask, TForm S);
231localstatic SatMask tfSatTYPE (SatMask, TForm S);
232
233localstatic SatMask tfSatUsePending (SatMask, TForm S, TForm T);
234localstatic SatMask tfSatUsePending1 (SatMask, AbSyn, TForm, TForm);
235localstatic SatMask tfSatEvery (SatMask, TForm S, TForm T);
236localstatic SatMask tfSatEach (SatMask, TForm S, TForm T);
237localstatic SatMask tfSatMap0 (SatMask, TForm S, TForm T);
238localstatic SatMask tfSatTuple (SatMask, TForm S, TForm T);
239localstatic SatMask tfSatCross (SatMask, TForm S, TForm T);
240localstatic SatMask tfSatMulti (SatMask, TForm S, TForm T);
241localstatic SatMask tfSatExcept (SatMask, TForm S, TForm T);
242
243localstatic SatMask tfSatCatExports (SatMask, AbSyn Sab, TForm S, TForm T);
244localstatic SatMask tfSatThdExports (SatMask, TForm S, TForm T);
245
246localstatic SatMask tfSatExports (SatMask,SymeList,SymeList,SymeList);
247localstatic SatMask tfSatExport (SatMask,SymeList,AbSyn Stf, SymeList S,Syme t, AbSub *lazy);
248localstatic AbSub tfSatExportLazySelfSubst(SymeList mods, Sefo Sab, AbSub *lazySelfSubst);
249localstatic SatMask tfSatParents (SatMask,SymeList, AbSyn, SymeList,SymeList);
250
251localstatic SatMask tfSatConditions (SatMask, SymeList, Syme, Syme);
252localstatic Bool sefoListMemberMod (SymeList, Sefo, SefoList);
253localstatic void tfSatPushMapConds (TForm);
254localstatic void tfSatPopMapConds (TForm);
255localstatic Sefo tfSatCond (TForm);
256localstatic SefoList tfSatConds (void);
257
258localstatic SymeList tfSatExportsMissing (SatMask,SymeList,AbSyn,SymeList,SymeList);
259localstatic SymeList tfSatParentsFilterTable (SymeTSet, SymeList);
260
261localstatic void tfSatSetPendingFail (TForm);
262
263localstatic String tfSatMaskToString(SatMask mask);
264
265/******************************************************************************
266 *
267 * :: Type form satisfaction bit mask accessors.
268 *
269 *****************************************************************************/
270
271SatMask
272tfSatHasMask(void)
273{
274 return TFS_Probe(((SatMask) 1) << 0) | TFS_NPendingMask((( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) |
(((SatMask) 1) << 8) | (((SatMask) 1) << 9) | ((
(SatMask) 1) << 10) | (((SatMask) 1) << 11) | (((
SatMask) 1) << 12) | (((SatMask) 1) << 13) | (((SatMask
) 1) << 14) | (((SatMask) 1) << 15) | (((SatMask)
1) << 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) & ~(((SatMask) 1) << 6));
275}
276
277SatMask
278tfSatBupMask(void)
279{
280 return TFS_Probe(((SatMask) 1) << 0) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) | TFS_Conditions(((SatMask) 1) << 5);
281}
282
283SatMask
284tfSatTdnMask(void)
285{
286 return TFS_Commit(((SatMask) 1) << 1) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) | TFS_Conditions(((SatMask) 1) << 5);
287}
288
289SatMask
290tfSatTdnInfoMask(void)
291{
292 return TFS_Commit(((SatMask) 1) << 1) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) | TFS_Info(((SatMask) 1) << 4);
293}
294
295SatMask
296tfSatSefMask(void)
297{
298 return TFS_Commit(((SatMask) 1) << 1) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) | TFS_Sefo(((SatMask) 1) << 8);
299}
300
301SatMask
302tfSatTErrorMask(void)
303{
304 return TFS_Probe(((SatMask) 1) << 0) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8));
305}
306
307Bool
308tfSatSucceed(SatMask mask)
309{
310 return !tfSatError(mask)((mask) & ( (((SatMask) 1) << 18) | (((SatMask) 1) <<
19) | (((SatMask) 1) << 20) | (((SatMask) 1) << 21
) | (((SatMask) 1) << 22) | (((SatMask) 1) << 23)
));
311}
312
313Bool
314tfSatPending(SatMask mask)
315{
316 return mask & TFS_Pending(((SatMask) 1) << 6);
317}
318
319Bool
320tfSatFailedExportsMissing(SatMask mask)
321{
322 return mask & TFS_ExportsMissing(((SatMask) 1) << 19);
323}
324
325Bool
326tfSatFailedEmbedFail(SatMask mask)
327{
328 return mask & TFS_EmbedFail(((SatMask) 1) << 20);
329}
330
331Bool
332tfSatFailedArgMissing(SatMask mask)
333{
334 return mask & TFS_ArgMissing(((SatMask) 1) << 21);
335}
336
337Bool
338tfSatFailedBadArgType(SatMask mask)
339{
340 return mask & TFS_BadArgType(((SatMask) 1) << 22);
341}
342
343Bool
344tfSatFailedDifferentArity(SatMask mask)
345{
346 return mask & TFS_DifferentArity(((SatMask) 1) << 23);
347}
348
349Length
350tfSatParN(SatMask mask)
351{
352 return tfSatParn(mask)((mask) & (~((((SatMask) 1) << 24) - 1))) >> TFS_BitsWidth24;
353}
354
355Length
356tfSatArgN(AbSyn ab, Length argc, AbSynGetter argf, Length parN, TForm S)
357{
358 Length parmc, ai;
359 TForm tfi;
360 Bool def;
361
362 parmc = tfMapHasDefaults(S) ? tfMapArgc(S) : argc;
363 tfi = tfAsMultiArgN(tfMapArg(S)tfFollowArg(S, 0), parmc, parN);
364 tfAsMultiSelectArg(ab, argc, parN, argf, tfi, &def, &ai);
365
366 return ai;
367}
368
369AbEmbed
370tfSatAbEmbed(SatMask mask)
371{
372 SatMask result = tfSatEmbed(mask)((mask) & ( (((SatMask) 1) << 6) | (((SatMask) 1) <<
7) | (((SatMask) 1) << 8) | (((SatMask) 1) << 9)
| (((SatMask) 1) << 10) | (((SatMask) 1) << 11) |
(((SatMask) 1) << 12) | (((SatMask) 1) << 13) | (
((SatMask) 1) << 14) | (((SatMask) 1) << 15) | ((
(SatMask) 1) << 16) | (((SatMask) 1) << 17) ));
373 /* -1 to allow for AB_Embed_Identity */
374 AbEmbed embed = ((AbEmbed) result) >> (TFS_EmbedShift9-1);
375
376 return embed;
377}
378
379/* Return the embedding needed to convert tf1 into tf2 */
380AbEmbed
381tfSatEmbedType(TForm tf1, TForm tf2)
382{
383 TFormTag t1, t2;
384
385 tfFollow(tf1)((tf1) = tfFollowFn(tf1));
386 tfFollow(tf2)((tf2) = tfFollowFn(tf2));
387
388 /* Deal with delta-equality */
389 tf1 = tfDefineeMaybeType(tf1);
390 tf2 = tfDefineeMaybeType(tf2);
391 /* Ignore exceptions for the purposes of embedding as well */
392 tf2 = tfIgnoreExceptions(tf2);
393
394 // FIXME: This is for examples like Union(x: Cross(A, B))
395 // Need to figure out what the best thing here is..
396 tf1 = tfDefineeType(tf1);
397
398 t1 = tfTag(tf1)((tf1)->tag);
399 t2 = tfTag(tf2)((tf2)->tag);
400
401 if (t1 == t2) return AB_Embed_Identity(((AbEmbed) 1) << 0);
402 else if (t1 == TF_Exit) return AB_Embed_Identity(((AbEmbed) 1) << 0);
403 else if (t1 == TF_Cross) {
404 if (t2 == TF_Tuple) return AB_Embed_CrossToTuple(((AbEmbed) 1) << 1);
405 else if (t2 == TF_Cross) return AB_Embed_Identity(((AbEmbed) 1) << 0);
406 else if (t2 == TF_Multiple) return AB_Embed_CrossToMulti(((AbEmbed) 1) << 2);
407 else return AB_Embed_CrossToUnary(((AbEmbed) 1) << 3);
408 }
409 else if (t1 == TF_Multiple) {
410 if (t2 == TF_Tuple) return AB_Embed_MultiToTuple(((AbEmbed) 1) << 4);
411 else if (t2 == TF_Cross) return AB_Embed_MultiToCross(((AbEmbed) 1) << 5);
412 else if (t2 == TF_Multiple) return AB_Embed_Identity(((AbEmbed) 1) << 0);
413 else return AB_Embed_MultiToUnary(((AbEmbed) 1) << 6);
414 }
415 else {
416 if (t2 == TF_Tuple) return AB_Embed_UnaryToTuple(((AbEmbed) 1) << 7);
417 else if (t2 == TF_Cross) return AB_Embed_UnaryToCross(((AbEmbed) 1) << 8);
418 else if (t2 == TF_Multiple) return AB_Embed_UnaryToMulti(((AbEmbed) 1) << 9);
419 else return AB_Embed_Identity(((AbEmbed) 1) << 0);
420 }
421}
422
423TForm
424tfsEmbedResult(TForm tf, AbEmbed embed)
425{
426 TFormList tfl;
427 int i;
428
429 if (!tf) return tf;
430
431 tf = tfDefineeType(tf);
432 if (tfIsDefinedType(tf)) {
433 tf = tfDefinedVal(tf);
434 }
435
436 if (embed & AB_Embed_Identity(((AbEmbed) 1) << 0) || embed == 0)
437 return tf;
438
439 if (embed & AB_Embed_CrossToTuple(((AbEmbed) 1) << 1)) {
440 assert(tfIsCross(tf))do { if (!((((tf)->tag) == TF_Cross))) _do_assert(("tfIsCross(tf)"
),"tfsat.c",440); } while (0);
441 assert(tfCrossArgc(tf))do { if (!(tfCrossArgc(tf))) _do_assert(("tfCrossArgc(tf)"),"tfsat.c"
,441); } while (0);
442 return tfTuple(tfCrossArgN(tf, int0)tfFollowArg(tf, ((int) 0)));
443 }
444 if (embed & AB_Embed_CrossToMulti(((AbEmbed) 1) << 2)) {
445 assert(tfIsCross(tf))do { if (!((((tf)->tag) == TF_Cross))) _do_assert(("tfIsCross(tf)"
),"tfsat.c",445); } while (0);
446 tfl = listNil(TForm)((TFormList) 0);
447 for (i = tfArgc(tf)((tf)->argc) - 1; i >= 0; i--)
448 tfl = listCons(TForm)(TForm_listPointer->Cons)(tfCrossArgv(tf)((tf)->argv)[i], tfl);
449 tf = tfMultiFrList(tfl);
450 listFree(TForm)(TForm_listPointer->Free)(tfl);
451 return tf;
452 }
453 if (embed & AB_Embed_CrossToUnary(((AbEmbed) 1) << 3)) {
454 assert(tfIsCross(tf))do { if (!((((tf)->tag) == TF_Cross))) _do_assert(("tfIsCross(tf)"
),"tfsat.c",454); } while (0);
455 assert(tfCrossArgc(tf))do { if (!(tfCrossArgc(tf))) _do_assert(("tfCrossArgc(tf)"),"tfsat.c"
,455); } while (0);
456 return tfCrossArgN(tf, int0)tfFollowArg(tf, ((int) 0));
457 }
458 if (embed & AB_Embed_MultiToTuple(((AbEmbed) 1) << 4)) {
459 assert(tfIsMulti(tf))do { if (!((((tf)->tag) == TF_Multiple))) _do_assert(("tfIsMulti(tf)"
),"tfsat.c",459); } while (0);
460 assert(!tfIsEmptyMulti(tf))do { if (!(!((((tf)->tag) == TF_Multiple) && tfMultiArgc
(tf) == 0))) _do_assert(("!tfIsEmptyMulti(tf)"),"tfsat.c",460
); } while (0);
461 return tfTuple(tfMultiArgN(tf, int0)tfFollowArg(tf, ((int) 0)));
462 }
463 if (embed & AB_Embed_MultiToCross(((AbEmbed) 1) << 5)) {
464 assert(tfIsMulti(tf))do { if (!((((tf)->tag) == TF_Multiple))) _do_assert(("tfIsMulti(tf)"
),"tfsat.c",464); } while (0);
465 return tfCrossFrMulti(tf);
466 }
467 if (embed & AB_Embed_MultiToUnary(((AbEmbed) 1) << 6)) {
468 assert(tfIsMulti(tf))do { if (!((((tf)->tag) == TF_Multiple))) _do_assert(("tfIsMulti(tf)"
),"tfsat.c",468); } while (0);
469 assert(!tfIsEmptyMulti(tf))do { if (!(!((((tf)->tag) == TF_Multiple) && tfMultiArgc
(tf) == 0))) _do_assert(("!tfIsEmptyMulti(tf)"),"tfsat.c",469
); } while (0);
470 return tfMultiArgN(tf, int0)tfFollowArg(tf, ((int) 0));
471 }
472 if (embed & AB_Embed_UnaryToTuple(((AbEmbed) 1) << 7)) {
473 return tfTuple(tf);
474 }
475 if (embed & AB_Embed_UnaryToCross(((AbEmbed) 1) << 8)) {
476 return tfCross(1, tf);
477 }
478 if (embed & AB_Embed_UnaryToMulti(((AbEmbed) 1) << 9)) {
479 return tfMulti(1, tf);
480 }
481
482 return tf;
483}
484
485/******************************************************************************
486 *
487 * :: External entry points.
488 *
489 *****************************************************************************/
490
491Bool
492tfSatisfies(TForm S, TForm T)
493{
494 SatMask mask = TFS_Commit(((SatMask) 1) << 1) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8));
495 return tfSatBit(mask, S, T);
496}
497
498Bool
499tfSatisfies1(AbSyn Sab, TForm S, TForm T)
500{
501 SatMask mask = TFS_Commit(((SatMask) 1) << 1) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) | TFS_Conditions(((SatMask) 1) << 5);
502 return tfSatSucceed(tfSat1(mask, Sab, S, T));
503}
504
505Bool
506tfSatValues(TForm S, TForm T)
507{
508 SatMask mask = TFS_Commit(((SatMask) 1) << 1) | TFS_NAnyToNoneMask((( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) |
(((SatMask) 1) << 8) | (((SatMask) 1) << 9) | ((
(SatMask) 1) << 10) | (((SatMask) 1) << 11) | (((
SatMask) 1) << 12) | (((SatMask) 1) << 13) | (((SatMask
) 1) << 14) | (((SatMask) 1) << 15) | (((SatMask)
1) << 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8)) & ~(((SatMask) 1) << 7));
509 return tfSatBit(mask, S, T);
510}
511
512Bool
513tfSatReturn(TForm S, TForm T)
514{
515 SatMask mask = TFS_Commit(((SatMask) 1) << 1) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8));
516 return tfSatBit(mask, S, T);
517}
518
519Bool
520tfSatDom(TForm S)
521{
522 SatMask mask = TFS_Probe(((SatMask) 1) << 0);
523 return tfSatSucceed(tfSatDOM(mask, S));
524}
525
526Bool
527tfSatCat(TForm S)
528{
529 SatMask mask = TFS_Probe(((SatMask) 1) << 0);
530 return tfSatSucceed(tfSatCAT(mask, S));
531}
532
533Bool
534tfSatType(TForm S)
535{
536 SatMask mask = TFS_Probe(((SatMask) 1) << 0);
537 return tfSatSucceed(tfSatTYPE(mask, S));
538}
539
540AbSub
541tfSatSubList(AbSyn ab)
542{
543 AbSub sigma;
544
545 switch (abTag(ab)((ab)->abHdr.tag)) {
546 case AB_Id:
547 sigma = absNew(stabFile());
548 break;
549 case AB_Apply: {
550 SatMask mask = TFS_Probe(((SatMask) 1) << 0) | TFS_Sigma(((SatMask) 1) << 3) | TFS_UsualMask(( (((SatMask) 1) << 6) | (((SatMask) 1) << 7) | (
((SatMask) 1) << 8) | (((SatMask) 1) << 9) | (((SatMask
) 1) << 10) | (((SatMask) 1) << 11) | (((SatMask)
1) << 12) | (((SatMask) 1) << 13) | (((SatMask) 1
) << 14) | (((SatMask) 1) << 15) | (((SatMask) 1)
<< 16) | (((SatMask) 1) << 17) ) & ~(((SatMask
) 1) << 8));
551 AbSyn op = abApplyOp(ab)((ab)->abApply.op);
552 Length argc = abApplyArgc(ab)(((ab)->abHdr.argc)-1);
553 TForm S;
554
555 assert(abState(op) == AB_State_HasUnique)do { if (!(((op)->abHdr.state) == AB_State_HasUnique)) _do_assert
(("abState(op) == AB_State_HasUnique"),"tfsat.c",555); } while
(0);
556
557 S = abTUnique(op)((op)->abHdr.type.unique);
558 sigma = tfSatSubList(op);
559 mask = tfSatMapArgs(mask, sigma, S, ab, argc, abApplyArgf);
560
561 if (!tfSatSucceed(mask)) {
562 /*!! bug("tfSatSubList: tfSatMapArgs failed."); */
563 absFree(sigma);
564 sigma = absFail();
565 }
566 break;
567 }
568 default:
569 sigma = absFail();
570 break;
571 }
572
573 return sigma;
574}
575
576
577/******************************************************************************
578 *
579 * :: tfSatMap
580 *
581 *****************************************************************************/
582
583SatMask
584tfSatMap(SatMask mask, Stab stab, TForm S, TForm T,
585 AbSyn ab, Length argc, AbSynGetter argf)
586{
587 SatMask result;
588 TForm Sret;
589 AbSub sigma;
590
591 assert(tfIsAnyMap(S))do { if (!(((((S)->tag) == TF_Map) || (((S)->tag) == TF_PackedMap
)))) _do_assert(("tfIsAnyMap(S)"),"tfsat.c",591); } while (0);
592 Sret = tfMapRet(S)tfFollowArg(S, 1);
593
594 sigma = absNew(stab);
595
596 result = tfSatMapArgs(mask, sigma, S, ab, argc, argf);
597 if (tfSatSucceed(result)) {
598 Sret = tformSubst(sigma, Sret);
599 result = tfSatEmbed(result)((result) & ( (((SatMask) 1) << 6) | (((SatMask) 1)
<< 7) | (((SatMask) 1) << 8) | (((SatMask) 1) <<
9) | (((SatMask) 1) << 10) | (((SatMask) 1) << 11
) | (((SatMask) 1) << 12) | (((SatMask) 1) << 13)
| (((SatMask) 1) << 14) | (((SatMask) 1) << 15) |
(((SatMask) 1) << 16) | (((SatMask) 1) << 17) )) | tfSat1(mask, ab, Sret, T);
600
601 if (tfSatSucceed(result) && tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)))
602 abTUnique(ab)((ab)->abHdr.type.unique) = Sret;
603 }
604
605 absFreeDeeply(sigma);
606
607 return result;
608}
609
610SatMask
611tfSatMapArgs(SatMask mask, AbSub sigma, TForm S,
612 AbSyn ab, Length argc, AbSynGetter argf)
613{
614 return tfSatAsMulti(mask, sigma, tfMapArg(S)tfFollowArg(S, 0), S, ab, argc, argf);
615}
616
617SatMask
618tfSatAsMulti(SatMask mask, AbSub sigma, TForm S, TForm TScope,
619 AbSyn ab, Length argc, AbSynGetter argf)
620{
621 SatMask result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
622 Length i, parmc, usedc;
623 int serialThis;
624 Bool packed = tfIsPackedMap(TScope)(((TScope)->tag) == TF_PackedMap);
625 AbSyn abc = NULL((void*)0);
626
627 if (tfAsMultiEmbed(S, argc) == AB_Embed_Fail((AbEmbed) 0))
628 return tfSatResult(mask, TFS_EmbedFail)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 20
)));
629
630 tfsSerialNo += 1;
631 tfsDepthNo += 1;
632 serialThis = tfsSerialNo;
633
634 if (DEBUG(tfsMulti)tfsMultiDebug) {
635 fprintf(dbOut, "->Tfc: %*s%d= ", tfsDepthNo, "", serialThis);
636 tfPrint(dbOut, S);
637 fprintf(dbOut, " satisfies ");
638 abPrint(dbOut, ab);
639 fnewline(dbOut);
640 }
641
642 parmc = tfMultiHasDefaults(S) ? tfAsMultiArgc(S) : argc;
643
644 if (parmc != 1 && tfIsTuple(tfDefineeType(S))(((tfDefineeType(S))->tag) == TF_Tuple)) {
645 abc = abNewEmpty(AB_Comma, parmc);
646 }
647
648 for (i = 0, usedc = 0; i < parmc; i += 1) {
649 AbSyn abi;
650 TForm tfi;
651 Syme syme;
652 Length pi, ai;
653 Bool def;
654 SatMask maski = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
655
656 pi = (S->rho ? S->rho[i] : i);
657 tfi = tfAsMultiArgN(S, parmc, pi);
658 abi = tfAsMultiSelectArg(ab, argc, pi, argf, tfi, &def, &ai);
659
660 if (!abi) {
661 result = tfSatParNFail(mask, TFS_ArgMissing, pi)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 21
)) | (((SatMask) (pi)) << 24));
662 break;
663 }
664 if (!def) usedc += 1;
665
666 syme = tfDefineeSyme(tfi);
667 tfi = tfDefineeType(tfi);
668 tfi = tformSubst(sigma, tfi);
669
670 /* Check to see if abi satisfies tfi. */
671 if (!def && !tfSatSigma(mask)((mask) & (((SatMask) 1) << 3))) {
672 maski = tfSatArg(mask, abi, tfi);
673 if (!tfSatSucceed(maski)) {
674 result = tfSatParNFail(mask, TFS_BadArgType, pi)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 22
)) | (((SatMask) (pi)) << 24));
675 break;
676 }
677 if (tfSatPending(maski))
678 result = tfSatResult(mask, TFS_Pending)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 6
)));
679 }
680 /* Type infer abi of type tfi, if needed. */
681 if (tfSatCommit(mask)((mask) & (((SatMask) 1) << 1))) {
682 /*
683 * Ensure that we have the correct set of types
684 * for this expression. In almost every case we
685 * will return immediately but it doesn't hurt
686 * to make sure.
687 */
688 tiTopFns()->tiBottomUp(absStab(sigma)((sigma)->stab), abi, tfUnknown);
689
690
691 /*
692 * Occasionally tiTopDown returns false and in
693 * the past this meant that we had to TFS_Fail
694 * or something similar. Seems fine now.
695 */
696
697 tiTopFns()->tiTopDown(absStab(sigma)((sigma)->stab), abi, tfi);
698
699 if (abUse(abi)((abi)->abHdr.use) != AB_Use_Type) {
700 /* Double check the type on abi (now unique) against tfi
701 * - it may have changed due to embeddings being applied
702 * within abi itself. (Note: embeddings are applied by
703 * callers, with the type on the absyn being the 'original'
704 * type).
705 * cf. axllib/tests/bug13138 and aldor/tests/hang
706 */
707 SatMask checkMask = tfSatArg(mask, abi, tfi);
708 abAddTContext(abi, tfSatAbEmbed(checkMask));
709 }
710 }
711 /* Install the packed embedding on abi, if needed. */
712 if (tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)) && packed)
713 if (!tiTopFns()->tiUnaryToRaw(absStab(sigma)((sigma)->stab), abi, tfi)) {
714 result = tfSatParNFail(mask, TFS_BadArgType, pi)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 22
)) | (((SatMask) (pi)) << 24));
715 break;
716 }
717 /*
718 * Extend the sublist for dependent or recursive maps.
719 *
720 * BUG: if tfi is a tfSyntax then we will almost certainly
721 * fail to spot any dependencies. See bug 1303 for example.
722 */
723 if (syme && (tfSymeInducesDependency(syme, TScope)
724 || listMemq(Syme)(Syme_listPointer->Memq)(tfSymes(TScope)((TScope)->symes), syme)
725 || listMember(Syme)(Syme_listPointer->Member)(tfSymes(TScope)((TScope)->symes), syme, symeEqual))) {
726 abi = sefoCopy(abi);
727 tiTopFns()->tiBottomUp(absStab(sigma)((sigma)->stab), abi, tfUnknown);
728 tiTopFns()->tiTopDown (absStab(sigma)((sigma)->stab), abi, tfi);
729
730 if (abState(abi)((abi)->abHdr.state) == AB_State_HasUnique) {
731 if (absFVars(sigma)((sigma)->fv)) absSetFVars(sigma, NULL)((sigma)->fv = (((void*)0)));
732 sigma = absExtend(syme, abi, sigma);
733 }
734 else {
735 result = tfSatParNFail(mask, TFS_BadArgType, pi)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 22
)) | (((SatMask) (pi)) << 24));
736 break;
737 }
738 }
739 if (abc) {
740 abArgv(abc)((abc)->abGen.data.argv)[i] = sefoCopy(abi);
741 }
742 }
743
744 /* Extend the sublist for dependent and recursive maps. */
745 if (tfSatSucceed(result) && abc) {
746 Syme syme = tfDefineeSyme(S);
747 TForm tfi = tfDefineeType(S);
748 if (syme && (tfSymeInducesDependency(syme, TScope) ||
749 listMemq(Syme)(Syme_listPointer->Memq)(tfSymes(TScope)((TScope)->symes), syme))) {
750 tiTopFns()->tiBottomUp(absStab(sigma)((sigma)->stab), abc, tfUnknown);
751 tiTopFns()->tiTopDown (absStab(sigma)((sigma)->stab), abc, tfi);
752 if (abState(abc)((abc)->abHdr.state) == AB_State_HasUnique) {
753 if (absFVars(sigma)((sigma)->fv)) absSetFVars(sigma, NULL)((sigma)->fv = (((void*)0)));
754 sigma = absExtend(syme, abc, sigma);
755 }
756 else {
757 result = tfSatParNFail(mask, TFS_BadArgType, 1)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 22
)) | (((SatMask) (1)) << 24));
758 }
759 }
760 }
761
762 /* Install the packed embedding on the return value, if needed. */
763 if (tfSatSucceed(result) && tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)) && packed)
764 if (!tiTopFns()->tiRawToUnary(absStab(sigma)((sigma)->stab), ab, tfMapRet(TScope)tfFollowArg(TScope, 1)))
765 result = tfSatResult(mask, TFS_EmbedFail)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 20
)));
766
767 if (tfSatSucceed(result) && usedc < argc)
768 result = tfSatResult(mask, TFS_DifferentArity)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 23
)));
769
770 if (DEBUG(tfsMulti)tfsMultiDebug) {
771 fprintf(dbOut, "<-Tfc: %*s%d= %s!", tfsDepthNo, "",
772 serialThis, boolToString(tfSatSucceed(result))((tfSatSucceed(result)) ? "true" : "false"));
773 fnewline(dbOut);
774 }
775 tfsDepthNo -= 1;
776
777 return result;
778}
779
780SatMask
781tfSatArg(SatMask mask, AbSyn ab, TForm T)
782{
783 SatMask result;
784
785 mask &= ~TFS_AnyToNone(((SatMask) 1) << 7);
786
787 /* We'd rather not use pending embeddings to decide argc questions. */
788 if (tfIsMulti(T)(((T)->tag) == TF_Multiple) && tfIsPending(T)(((T)->state)==TF_State_Pending))
789 mask &= ~TFS_Pending(((SatMask) 1) << 6);
790
791 switch (abState(ab)((ab)->abHdr.state)) {
792 case AB_State_HasPoss:
793 result = tfSatArgPoss(mask, ab, T);
794 break;
795
796 case AB_State_HasUnique:
797 result = tfSat1(mask, ab, abTUnique(ab)((ab)->abHdr.type.unique), T);
798 break;
799
800 default:
801 result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
802 break;
803 }
804
805 return result;
806}
807
808localstatic SatMask
809tfSatArgPoss(SatMask mask, AbSyn Sab, TForm T)
810{
811 TFormList l;
812 SatMask result;
813 TPoss S = abTPoss(Sab)((Sab)->abHdr.type.poss);
814
815 if (tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6))) && tpossIsUnique(S)) {
816 tcSatPush(tpossUnique(S), T);
817 result = tfSatUsePending1(mask, Sab, tpossUnique(S), T);
818 tcSatPop();
819 if (tfSatSucceed(result))
820 return result;
821 }
822
823 TPossIterator ip;
824 for (tpossITER(ip, S)((ip).possl = (S ? (S)->possl : ((void*)0))); tpossMORE(ip)((ip).possl); tpossSTEP(ip)((ip).possl = (((ip).possl)->rest))) {
825 TForm s = tpossELT(ip)tpossELT_(&ip);
826 result = tfSat1(mask, Sab, s, T);
827 if (tfSatSucceed(result))
828 return result;
829 }
830
831 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
832}
833
834/******************************************************************************
835 *
836 * :: tfSat
837 *
838 *****************************************************************************/
839
840/*
841 * Succeed if S satisfies T.
842 */
843Bool
844tfSatBit(SatMask mask, TForm S, TForm T)
845{
846 return tfSatSucceed(tfSat(mask, S, T));
847}
848
849SatMask
850tfSat(SatMask mask, TForm S, TForm T)
851{
852 return tfSat1(mask, 0, S, T);
853}
854
855SatMask
856tfSat1(SatMask mask, AbSyn Sab, TForm S, TForm T)
857{
858 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
859 int serialThis;
860
861 S = tfFollowOnly(S);
862 T = tfFollowOnly(T);
863
864 tfsSerialNo += 1;
865 serialThis = tfsSerialNo;
866
867 /* If we can determine satisfaction w/o using tfFollow, do so. */
868 if (tfIsSubst(S)(((S)->tag) == TF_Subst)) {
869 tfsDEBUGif (!tfsDebug) { } else afprintf(dbOut, "(%d - skip subst\n", serialThis);
870 result = tfSat(mask & ~TFS_Pending(((SatMask) 1) << 6), tfSubstArg(S)tfFollowArg(S, 0), T);
871 tfsDEBUGif (!tfsDebug) { } else afprintf(dbOut, " %d - skip subst - %oBool)\n", serialThis, tfSatSucceed(result));
872 if (tfSatSucceed(result))
873 return result;
874 }
875 S = tfDefineeType(S);
876 T = tfDefineeType(T);
877
878 if (tfSatAllow(mask, TFS_Sefo)((mask) & ((((SatMask) 1) << 8))))
879 return tfSatResult(mask, TFS_Sefo)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 8
)));
880
881 tfsDepthNo += 1;
882
883 if (DEBUG(tfs)tfsDebug) {
884 fprintf(dbOut, "->Tfs: %*s%d= ", tfsDepthNo, "", serialThis);
885 tfPrint(dbOut, S);
886 fprintf(dbOut, " satisfies ");
887 tfPrint(dbOut, T);
888 fnewline(dbOut);
889 }
890
891 tcSatPush(S, T);
892
893 if (S == T)
894 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
895
896 /*
897 * tfType
898 */
899 else if (tfIsType(T)(((T)->tag) == TF_Type) || tfIsTypeSyntax(T)((((T)->tag) == TF_Syntax) && (((((T)->__absyn)
)->abHdr.tag == (AB_Id)) && ((((T)->__absyn))->
abId.sym)==(ssymType))))
900 result = tfSatTYPE(mask, S);
901
902 /*
903 * tfCategory
904 */
905 else if (tfIsCategory(T)(((T)->tag) == TF_Category) || tfIsCategorySyntax(T)((((T)->tag) == TF_Syntax) && (((((T)->__absyn)
)->abHdr.tag == (AB_Id)) && ((((T)->__absyn))->
abId.sym)==(ssymCategory))))
906 result = tfSatCAT(mask, S);
907
908 /*
909 * tfExit
910 */
911 else if (tfIsExit(S)(((S)->tag) == TF_Exit))
912 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
913 /*
914 * tfUnknown
915 */
916 else if (tfIsUnknown(T)(((T)->tag) == TF_Unknown))
917 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
918
919 else if (tfIsUnknown(S)(((S)->tag) == TF_Unknown))
920 result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
921
922 /*
923 * tfSyntax
924 */
925 else if (tfIsSyntax(S)(((S)->tag) == TF_Syntax) || tfIsSyntax(T)(((T)->tag) == TF_Syntax)) {
926 if (tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6))))
927 result = tfSatUsePending(mask, S, T);
928 }
929
930 /*
931 * tfRaw
932 */
933 else if (tfIsRaw(S)(((S)->tag) == TF_Raw))
934 result = tfSat(mask, tfRawType(tfRawArg(S)tfFollowArg(S, 0)), T);
935
936 else if (tfIsRaw(T)(((T)->tag) == TF_Raw))
937 result = tfSat(mask, S, tfRawType(tfRawArg(T)tfFollowArg(T, 0)));
938
939 /*
940 * tfExcept
941 */
942 else if (tfIsExcept(S)(((S)->tag) == TF_Except) && !tfIsExcept(T)(((T)->tag) == TF_Except))
943 result = tfSat(mask, tfExceptType(S)tfFollowArg(S, 0), T);
944 else if (tfIsExcept(T)(((T)->tag) == TF_Except))
945 result = tfSatExcept(mask, S, T);
946 /*
947 * tfMap
948 */
949 else if (tfIsAnyMap(T)((((T)->tag) == TF_Map) || (((T)->tag) == TF_PackedMap)
))
950 result = tfSatMap0(mask, S, T);
951
952 /*
953 * tfTuple
954 */
955 else if (tfIsTuple(T)(((T)->tag) == TF_Tuple))
956 result = tfSatTuple(mask, S, T);
957
958 /*
959 * tfCross
960 */
961 else if (tfIsCross(T)(((T)->tag) == TF_Cross)) {
962 result = tfSatCross(mask, S, T);
963 if (!(tfSatSucceed(result)))
964 {
965 /* Delta-equality of S with cross */
966 TForm Snorm = tfDefineeBaseType(S);
967 result = tfSatCross(mask, Snorm, T);
968 }
969 }
970
971 /*
972 * tfMultiple
973 */
974 else if (tfIsMulti(T)(((T)->tag) == TF_Multiple)) {
975 result = tfSatMulti(mask, S, T);
976 if (!(tfSatSucceed(result)))
977 {
978 /* Delta-equality of S with multi */
979 TForm Snorm = tfDefineeBaseType(S);
980 result = tfSatMulti(mask, Snorm, T);
981 }
982 }
983
984 /*
985 * Other product rules.
986 */
987 else if (tfIsCross(S)(((S)->tag) == TF_Cross)) {
988 TForm Sarg = tfCrossArgN(S, int0)tfFollowArg(S, ((int) 0));
989 /* Embed Cross(S) in S. */
990 if (tfSatAllow(mask, TFS_CrossToUnary)((mask) & ((((SatMask) 1) << 11))) &&
991 tfCrossArgc(S) == 1 &&
992 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), Sarg, T))
993 {
994 result = tfSatResult(mask, TFS_CrossToUnary)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 11
)));
995 }
996 else /* The logic of this needs cleaning up */
997 {
998 /* Delta-equality of T with cross/multi */
999 TForm Tnorm = tfDefineeBaseType(T);
1000 if (tfIsCross(Tnorm)(((Tnorm)->tag) == TF_Cross))
1001 result = tfSatCross(mask, S, Tnorm);
1002 else if (tfIsMulti(Tnorm)(((Tnorm)->tag) == TF_Multiple))
1003 result = tfSatMulti(mask, S, Tnorm);
1004 }
1005 }
1006 else if (tfIsMulti(S)(((S)->tag) == TF_Multiple)) {
1007 TForm Sarg = tfMultiArgN(S, int0)tfFollowArg(S, ((int) 0));
1008 /* Embed Multi(S) in S. */
1009 if (tfSatAllow(mask, TFS_MultiToUnary)((mask) & ((((SatMask) 1) << 14))) &&
1010 tfMultiArgc(S) == 1 &&
1011 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), Sarg, T))
1012 {
1013 result = tfSatResult(mask, TFS_MultiToUnary)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 14
)));
1014 }
1015 else /* The logic of this needs cleaning up */
1016 {
1017 /* Delta-equality of T with cross/multi */
1018 TForm Tnorm = tfDefineeBaseType(T);
1019 if (tfIsCross(Tnorm)(((Tnorm)->tag) == TF_Cross))
1020 result = tfSatCross(mask, S, Tnorm);
1021 else if (tfIsMulti(Tnorm)(((Tnorm)->tag) == TF_Multiple))
1022 result = tfSatMulti(mask, S, Tnorm);
1023 }
1024 }
1025
1026 /*
1027 * Category forms
1028 */
1029 else if (tfSatSucceed(tfSatDOM(mask, T))) {
1030 if (tfSatSucceed(tfSatDOM(mask, S))) {
1031 if (tfSatUseConditions(mask)((mask) & (((SatMask) 1) << 5)) && abCondKnown != NULL((void*)0)
1032 && Sab != NULL((void*)0)) {
1033 if (tfIsPending(S)(((S)->state)==TF_State_Pending)) {
1034 if (tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6)))) {
1035 result = tfSatUsePending1(mask,
1036 Sab, S, T);
1037 return result;
1038 }
1039 }
1040 TForm tf = ablogImpliedType(abCondKnown, Sab, S);
1041 if (tf != NULL((void*)0)) {
1042 tfsDEBUGif (!tfsDebug) { } else afprintf(dbOut, "Swapping type: %pTForm to %pTForm\n", S, tf);
1043 S = tf;
1044 }
1045 }
1046 result = tfSatCatExports(mask, Sab, S, T);
1047 }
1048 }
1049
1050 /*
1051 * Third forms
1052 */
1053 else if (tfSatSucceed(tfSatCAT(mask, T))) {
1054 if (tfSatSucceed(tfSatCAT(mask, S)))
1055 result = tfSatThdExports(mask, S, T);
1056 }
1057
1058 /*
1059 * Default case
1060 */
1061 else if (tfEqual(S, T))
1062 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1063
1064 tcSatPop();
1065
1066 if (DEBUG(tfs)tfsDebug) {
1067 fprintf(dbOut, "<-Tfs: %*s%d= %s!", tfsDepthNo, "",
1068 serialThis, boolToString(tfSatSucceed(result))((tfSatSucceed(result)) ? "true" : "false"));
1069 if (tfSatEmbed(result)((result) & ( (((SatMask) 1) << 6) | (((SatMask) 1)
<< 7) | (((SatMask) 1) << 8) | (((SatMask) 1) <<
9) | (((SatMask) 1) << 10) | (((SatMask) 1) << 11
) | (((SatMask) 1) << 12) | (((SatMask) 1) << 13)
| (((SatMask) 1) << 14) | (((SatMask) 1) << 15) |
(((SatMask) 1) << 16) | (((SatMask) 1) << 17) )))
1070 fprintf(dbOut, " (after embedding)");
1071 if (tfSatPending(result))
1072 afprintf(dbOut, " (pending) - %pTForm", tfSatGetPendingFail());
1073 fnewline(dbOut);
1074 }
1075 tfsDepthNo -= 1;
1076
1077 return result;
1078
1079}
1080
1081/******************************************************************************
1082 *
1083 * :: tfSat cases
1084 *
1085 *****************************************************************************/
1086
1087/*
1088 * Succeed if S is a category.
1089 */
1090#if 0
1091localstatic SatMask tfSatDOM0(SatMask mask, TForm S);
1092localstatic SatMask tfSatCAT0(SatMask mask, TForm S);
1093
1094localstatic SatMask
1095tfSatDOM(SatMask mask, TForm S)
1096{
1097 fprintf(dbOut, "(SatDom: ");
1098 tfPrintDb(S);
1099 mask = tfSatDOM0(mask, S);
1100 fprintf(dbOut, ")");
1101 return mask;
1102}
1103
1104localstatic SatMask
1105tfSatCAT(SatMask mask, TForm S)
1106{
1107 fprintf(dbOut, "(SatCat: ");
1108 tfPrintDb(S);
1109 mask = tfSatCAT0(mask, S);
1110 fprintf(dbOut, ")");
1111 return mask;
1112}
1113#endif
1114
1115localstatic SatMask
1116tfSatDOM(SatMask mask, TForm S)
1117{
1118 TForm nS = tfDefineeTypeSubst(S);
1119
1120 if (tfIsAnyMap(nS)((((nS)->tag) == TF_Map) || (((nS)->tag) == TF_PackedMap
)))
1121 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1122 else if (tfIsRawRecord(nS)(((nS)->tag) == TF_RawRecord) || tfIsRecord(nS)(((nS)->tag) == TF_Record) ||
1123 tfIsUnion(nS)(((nS)->tag) == TF_Union) || tfIsEnum(nS)(((nS)->tag) == TF_Enumerate) ||
1124 tfIsTrailingArray(nS)(((nS)->tag) == TF_TrailingArray))
1125 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1126 /*!! This clause is really not quite right. */
1127 else if (tfIsType(nS)(((nS)->tag) == TF_Type) || tfIsTypeSyntax(nS)((((nS)->tag) == TF_Syntax) && (((((nS)->__absyn
))->abHdr.tag == (AB_Id)) && ((((nS)->__absyn))
->abId.sym)==(ssymType))) || tfIsSyntax(nS)(((nS)->tag) == TF_Syntax))
1128 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1129
1130 else if (tfIsWith(nS)(((nS)->tag) == TF_With) || tfIsWithSyntax(nS)((((nS)->tag) == TF_Syntax) && ((((nS)->__absyn
))->abHdr.tag == (AB_With))) || tfIsIf(nS)(((nS)->tag) == TF_If) ||
1131 tfIsJoin(nS)(((nS)->tag) == TF_Join) || tfIsMeet(nS)(((nS)->tag) == TF_Meet))
1132 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1133
1134 else if (tfSatSucceed(tfSatCAT(mask, S)))
1135 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1136 else
1137 return tfSatCAT(mask, tfGetCategory(tfDefineeType(S)));
1138}
1139
1140
1141/*
1142 * Succeed if S is a third-order type.
1143 */
1144localstatic SatMask
1145tfSatCAT(SatMask mask, TForm S)
1146{
1147 TForm nS = tfDefineeTypeSubst(S);
1148
1149 if (tfIsAnyMap(nS)((((nS)->tag) == TF_Map) || (((nS)->tag) == TF_PackedMap
)))
1150 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1151 else if (tfIsRawRecord(nS)(((nS)->tag) == TF_RawRecord) || tfIsRecord(nS)(((nS)->tag) == TF_Record) ||
1152 tfIsUnion(nS)(((nS)->tag) == TF_Union) || tfIsEnum(nS)(((nS)->tag) == TF_Enumerate) ||
1153 tfIsTrailingArray(nS)(((nS)->tag) == TF_TrailingArray))
1154 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1155 else if (tfIsCategory(nS)(((nS)->tag) == TF_Category) || tfIsCategorySyntax(nS)((((nS)->tag) == TF_Syntax) && (((((nS)->__absyn
))->abHdr.tag == (AB_Id)) && ((((nS)->__absyn))
->abId.sym)==(ssymCategory))) || tfIsThird(nS)(((nS)->tag) == TF_Third))
1156 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1157 else
1158 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1159}
1160
1161/*
1162 * Succeed if S is a higher-order type.
1163 */
1164localstatic SatMask
1165tfSatTYPE(SatMask mask, TForm S)
1166{
1167 if (tfIsAnyMap(S)((((S)->tag) == TF_Map) || (((S)->tag) == TF_PackedMap)
))
1168 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1169
1170 else if (tfSatSucceed(tfSatDOM(mask, S)))
1171 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1172
1173 else if (tfSatSucceed(tfSatCAT(mask, S)))
1174 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1175
1176 else if (tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6))))
1177 return tfSatUsePending(mask, tfDefineeType(S), tfType);
1178
1179 else
1180 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1181}
1182
1183localstatic SatMask
1184tfSatUsePending(SatMask mask, TForm S, TForm T)
1185{
1186 return tfSatUsePending1(mask, NULL((void*)0), S, T);
1187}
1188
1189localstatic SatMask
1190tfSatUsePending1(SatMask mask, AbSyn Sab, TForm S, TForm T)
1191{
1192 SatMask result;
1193
1194 if (tfIsPending(S)(((S)->state)==TF_State_Pending)) {
1195 tfSatSetPendingFail(S);
1196 result = tfSatResult(mask, TFS_Pending)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 6
)));
1197 if (tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)))
1198 tcNewSat1(S, abCondKnown, Sab, S, T, NULL((void*)0));
1199 return result;
1200 }
1201 if (tfIsPending(T)(((T)->state)==TF_State_Pending)) {
1202 tfSatSetPendingFail(T);
1203 result = tfSatResult(mask, TFS_Pending)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 6
)));
1204 if (tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)))
1205 tcNewSat1(T, abCondKnown, Sab, S, T, NULL((void*)0));
1206 return result;
1207 }
1208
1209 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1210}
1211
1212/*
1213 * Succeed if every argument of S satisfies T.
1214 */
1215localstatic SatMask
1216tfSatEvery(SatMask mask, TForm S, TForm T)
1217{
1218 Length i;
1219
1220 for (i = 0; i < tfArgc(S)((S)->argc); i += 1)
1221 if (!tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), tfArgv(S)((S)->argv)[i], T))
1222 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1223
1224 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1225}
1226
1227/*
1228 * Succeed if each argument of S satisfies the corresponding argument of T.
1229 */
1230localstatic SatMask
1231tfSatEach(SatMask mask, TForm S, TForm T)
1232{
1233 SatMask result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1234 Stab stab = tfGetStab(T);
1235 AbSub sigma;
1236 Length i, argc = tfArgc(S)((S)->argc);
1237
1238 assert(tfArgc(S) == tfArgc(T))do { if (!(((S)->argc) == ((T)->argc))) _do_assert(("tfArgc(S) == tfArgc(T)"
),"tfsat.c",1238); } while (0);
1239
1240 for (i = 0; !stab && i < argc; i += 1) {
1241 TForm Targ = tfArgv(T)((T)->argv)[i];
1242 Syme Tsyme = tfDefineeSyme(Targ);
1243
1244 if (Tsyme) stab = stabFindLevel(stabFile(), Tsyme);
1245 }
1246
1247 sigma = absNew(stab);
1248 for (i = 0; tfSatSucceed(result) && i < argc; i += 1) {
1249 TForm Sarg = tfArgv(S)((S)->argv)[i];
1250 TForm Targ = tformSubst(sigma, tfArgv(T)((T)->argv)[i]);
1251 Syme Ssyme = tfDefineeSyme(Sarg);
1252 Syme Tsyme = tfDefineeSyme(Targ);
1253 AbSyn ab = NULL((void*)0);
1254
1255 if (!tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), Sarg, Targ))
1256 result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1257
1258 if (Ssyme && Ssyme != Tsyme)
1259 ab = abFrSyme(Ssyme);
1260 else if (tfIsDefine(Sarg)(((Sarg)->tag) == TF_Define))
1261 ab = tfGetExpr(tfDefineVal(Sarg))((tfFollowArg(Sarg, 1))->__absyn);
1262
1263 /* Extend the sublist for dependent symes. */
1264 if (stab && ab && Tsyme) {
1265 tiTopFns()->tiBottomUp(stab, ab, tfUnknown);
1266 tiTopFns()->tiTopDown (stab, ab, Targ);
1267 if (abState(ab)((ab)->abHdr.state) == AB_State_HasUnique) {
1268 if (absFVars(sigma)((sigma)->fv))
1269 absSetFVars(sigma, NULL)((sigma)->fv = (((void*)0)));
1270 sigma = absExtend(Tsyme, ab, sigma);
1271 }
1272 else
1273 result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1274 }
1275 }
1276
1277 absFree(sigma);
1278 return result;
1279}
1280
1281localstatic SatMask
1282tfSatMap0(SatMask mask, TForm S, TForm T)
1283{
1284 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1285 SatMask mask0 = tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6))));
1286
1287 if (!(tfTag(T)((T)->tag) == tfTag(S)((S)->tag) && tfMapArgc(T) == tfMapArgc(S)))
1288 /* result = tfSatFalse(mask) */;
1289
1290 else if (tfIsDependentMap(S) && tfIsPending(S)(((S)->state)==TF_State_Pending) &&
1291 tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6))))
1292 result = tfSatUsePending(mask, S, T);
1293
1294 else if (tfIsDependentMap(S)) {
1295 Stab stab = tfGetStab(S);
1296 AbSub sigma = absNew(stab);
1297 Length i, argc = tfMapArgc(S);
1298
1299 tfSatPushMapConds(T);
1300 result = tfSatTrue(mask0)(((mask0) & ( (((SatMask) 1) << 0) | (((SatMask) 1)
<< 1) | (((SatMask) 1) << 2) | (((SatMask) 1) <<
3) | (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1301 for (i = 0; tfSatSucceed(result) && i < argc; i += 1) {
1302 TForm Sarg = tformSubst(sigma, tfMapArgN(S,i));
1303 TForm Targ = tfMapArgN(T,i);
1304 Syme Ssyme = tfDefineeSyme(Sarg);
1305 Syme Tsyme = tfDefineeSyme(Targ);
1306
1307 result = tfSatEmbed(result)((result) & ( (((SatMask) 1) << 6) | (((SatMask) 1)
<< 7) | (((SatMask) 1) << 8) | (((SatMask) 1) <<
9) | (((SatMask) 1) << 10) | (((SatMask) 1) << 11
) | (((SatMask) 1) << 12) | (((SatMask) 1) << 13)
| (((SatMask) 1) << 14) | (((SatMask) 1) << 15) |
(((SatMask) 1) << 16) | (((SatMask) 1) << 17) )) |
1308 tfSat(mask0, Targ, Sarg);
1309
1310 /* Extend the sublist for dependent symes. */
1311 if (Ssyme && Tsyme && Ssyme != Tsyme &&
1312 (tfSymeInducesDependency(Ssyme, S) ||
1313 listMember(Syme)(Syme_listPointer->Member)(tfSymes(S)((S)->symes), Ssyme, symeEqual))) {
1314 /* listMemq(Syme)(tfSymes(S), Ssyme))) { */ /* Commented by C.O. for ALMA usage*/
1315 AbSyn ab = abFrSyme(Tsyme);
1316
1317 /** CODE INTRODUCED BY C.O. for ALMA usage**/
1318 int p; listFind(Syme)(Syme_listPointer->Find)(tfSymes(S)((S)->symes), Ssyme, symeEqual, &p);
1319 if(p>-1) {
1320 Ssyme = listElt(Syme)(Syme_listPointer->Elt)(tfSymes(S)((S)->symes), p);
1321 }
1322 /*****************************/
1323
1324 tiTopFns()->tiBottomUp(absStab(sigma)((sigma)->stab), ab, tfUnknown);
1325 tiTopFns()->tiTopDown (absStab(sigma)((sigma)->stab), ab, Sarg);
1326 if (abState(ab)((ab)->abHdr.state) == AB_State_HasUnique) {
1327 if (absFVars(sigma)((sigma)->fv))
1328 absSetFVars(sigma, NULL)((sigma)->fv = (((void*)0)));
1329 sigma = absExtend(Ssyme, ab, sigma);
1330 }
1331 else {
1332 result = tfSatResult(mask,(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 22
)))
1333 TFS_BadArgType)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 22
)));
1334 }
1335 }
1336 }
1337
1338
1339 if (tfSatSucceed(result)) {
1340 TForm Sret = tformSubst(sigma, tfMapRet(S)tfFollowArg(S, 1));
1341 TForm Tret = tfMapRet(T)tfFollowArg(T, 1);
1342 result = tfSatEmbed(result)((result) & ( (((SatMask) 1) << 6) | (((SatMask) 1)
<< 7) | (((SatMask) 1) << 8) | (((SatMask) 1) <<
9) | (((SatMask) 1) << 10) | (((SatMask) 1) << 11
) | (((SatMask) 1) << 12) | (((SatMask) 1) << 13)
| (((SatMask) 1) << 14) | (((SatMask) 1) << 15) |
(((SatMask) 1) << 16) | (((SatMask) 1) << 17) )) |
1343 tfSat(mask0, Sret, Tret);
1344 }
1345 tfSatPopMapConds(T);
1346 absFree(sigma);
1347 }
1348
1349 else {
1350 tfSatPushMapConds(T);
1351 result = tfSat(mask0, tfMapArg(T)tfFollowArg(T, 0), tfMapArg(S)tfFollowArg(S, 0));
1352 if (tfSatSucceed(result))
1353 result = tfSatEmbed(result)((result) & ( (((SatMask) 1) << 6) | (((SatMask) 1)
<< 7) | (((SatMask) 1) << 8) | (((SatMask) 1) <<
9) | (((SatMask) 1) << 10) | (((SatMask) 1) << 11
) | (((SatMask) 1) << 12) | (((SatMask) 1) << 13)
| (((SatMask) 1) << 14) | (((SatMask) 1) << 15) |
(((SatMask) 1) << 16) | (((SatMask) 1) << 17) )) |
1354 tfSat(mask0, tfMapRet(S)tfFollowArg(S, 1), tfMapRet(T)tfFollowArg(T, 1));
1355 tfSatPopMapConds(T);
1356 }
1357
1358 return result;
1359}
1360
1361localstatic SatMask
1362tfSatTuple(SatMask mask, TForm S, TForm T)
1363{
1364 TForm Targ = tfTupleArg(T)tfFollowArg(T, 0);
1365 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1366
1367 if (tfIsTuple(S)(((S)->tag) == TF_Tuple))
1368 result = tfSat(mask, tfTupleArg(S)tfFollowArg(S, 0), Targ);
1369
1370 else if (!tfSatEmbed(mask)((mask) & ( (((SatMask) 1) << 6) | (((SatMask) 1) <<
7) | (((SatMask) 1) << 8) | (((SatMask) 1) << 9)
| (((SatMask) 1) << 10) | (((SatMask) 1) << 11) |
(((SatMask) 1) << 12) | (((SatMask) 1) << 13) | (
((SatMask) 1) << 14) | (((SatMask) 1) << 15) | ((
(SatMask) 1) << 16) | (((SatMask) 1) << 17) )))
1371 /* result = tfSatFalse(mask) */;
1372
1373 else if (tfIsCross(S)(((S)->tag) == TF_Cross)) {
1374 /* Embed Cross(A, ..., A) in Tuple(A). */
1375 if (tfSatAllow(mask, TFS_CrossToTuple)((mask) & ((((SatMask) 1) << 9))) &&
1376 tfSatSucceed(tfSatEvery(mask, S, Targ)))
1377 result = tfSatResult(mask, TFS_CrossToTuple)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 9
)));
1378
1379 /* Embed S in Tuple(S). */
1380 else if (tfSatAllow(mask, TFS_UnaryToTuple)((mask) & ((((SatMask) 1) << 15))) &&
1381 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), S, Targ))
1382 result = tfSatResult(mask, TFS_UnaryToTuple)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 15
)));
1383 }
1384
1385 else if (tfIsMulti(S)(((S)->tag) == TF_Multiple)) {
1386 /* Embed Multi(A, ..., A) in Tuple(A). */
1387 if (tfSatAllow(mask, TFS_MultiToTuple)((mask) & ((((SatMask) 1) << 12))) &&
1388 tfSatSucceed(tfSatEvery(mask, S, Targ)))
1389 result = tfSatResult(mask, TFS_MultiToTuple)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 12
)));
1390 }
1391
1392 else {
1393 /* Embed S in Tuple(S). */
1394 if (tfSatAllow(mask, TFS_UnaryToTuple)((mask) & ((((SatMask) 1) << 15))) &&
1395 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), S, Targ))
1396 result = tfSatResult(mask, TFS_UnaryToTuple)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 15
)));
1397 }
1398
1399 return result;
1400}
1401
1402localstatic SatMask
1403tfSatCross(SatMask mask, TForm S, TForm T)
1404{
1405 Length argc = tfCrossArgc(T);
1406 TForm Targ = tfCrossArgN(T, int0)tfFollowArg(T, ((int) 0));
1407 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1408
1409 if (tfIsCross(S)(((S)->tag) == TF_Cross)) {
1410 if (tfCrossArgc(S) == argc &&
1411 tfSatSucceed(tfSatEach(mask, S, T)))
1412 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1413
1414 /* Embed S in Cross(S). */
1415 else if (tfSatAllow(mask, TFS_UnaryToCross)((mask) & ((((SatMask) 1) << 16))) &&
1416 argc == 1 &&
1417 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), S, Targ))
1418 result = tfSatResult(mask, TFS_UnaryToCross)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 16
)));
1419 }
1420
1421 else if (!tfSatEmbed(mask)((mask) & ( (((SatMask) 1) << 6) | (((SatMask) 1) <<
7) | (((SatMask) 1) << 8) | (((SatMask) 1) << 9)
| (((SatMask) 1) << 10) | (((SatMask) 1) << 11) |
(((SatMask) 1) << 12) | (((SatMask) 1) << 13) | (
((SatMask) 1) << 14) | (((SatMask) 1) << 15) | ((
(SatMask) 1) << 16) | (((SatMask) 1) << 17) )))
1422 /* result = tfSatFalse(mask) */;
1423
1424 else if (tfIsMulti(S)(((S)->tag) == TF_Multiple)) {
1425 /* Embed Multi(A, ..., B) in Cross(A, ..., B). */
1426 if (tfSatAllow(mask, TFS_MultiToCross)((mask) & ((((SatMask) 1) << 13))) &&
1427 tfMultiArgc(S) == argc &&
1428 tfSatSucceed(tfSatEach(mask, S, T)))
1429 result = tfSatResult(mask, TFS_MultiToCross)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 13
)));
1430 }
1431
1432 else {
1433 /* Embed S in Cross(S). */
1434 if (tfSatAllow(mask, TFS_UnaryToCross)((mask) & ((((SatMask) 1) << 16))) &&
1435 argc == 1 &&
1436 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), S, Targ))
1437 result = tfSatResult(mask, TFS_UnaryToCross)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 16
)));
1438 }
1439
1440 return result;
1441}
1442
1443localstatic SatMask
1444tfSatMulti(SatMask mask, TForm S, TForm T)
1445{
1446 Length argc = tfMultiArgc(T);
1447 TForm Targ = tfMultiArgN(T, int0)tfFollowArg(T, ((int) 0));
1448 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1449
1450 if (tfIsMulti(S)(((S)->tag) == TF_Multiple)) {
1451 if (tfMultiArgc(S) == argc &&
1452 tfSatSucceed(tfSatEach(mask, S, T)))
1453 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1454
1455 /* Embed S in Multi(). */
1456 else if (tfSatAllow(mask, TFS_AnyToNone)((mask) & ((((SatMask) 1) << 7))) && argc == 0)
1457 result = tfSatResult(mask, TFS_AnyToNone)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 7
)));
1458 }
1459
1460 else if (!tfSatEmbed(mask)((mask) & ( (((SatMask) 1) << 6) | (((SatMask) 1) <<
7) | (((SatMask) 1) << 8) | (((SatMask) 1) << 9)
| (((SatMask) 1) << 10) | (((SatMask) 1) << 11) |
(((SatMask) 1) << 12) | (((SatMask) 1) << 13) | (
((SatMask) 1) << 14) | (((SatMask) 1) << 15) | ((
(SatMask) 1) << 16) | (((SatMask) 1) << 17) )))
1461 /* result = tfSatFalse(mask) */;
1462
1463 else if (tfIsCross(S)(((S)->tag) == TF_Cross)) {
1464 /* Embed Cross(A, ..., B) in Multi(A, ..., B). */
1465 if (tfSatAllow(mask, TFS_CrossToMulti)((mask) & ((((SatMask) 1) << 10))) &&
1466 tfCrossArgc(S) == argc &&
1467 tfSatSucceed(tfSatEach(mask, S, T)))
1468 result = tfSatResult(mask, TFS_CrossToMulti)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 10
)));
1469
1470 /* Embed S in Multi(S). */
1471 else if (tfSatAllow(mask, TFS_UnaryToMulti)((mask) & ((((SatMask) 1) << 17))) &&
1472 argc == 1 &&
1473 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), S, Targ))
1474 result = tfSatResult(mask, TFS_UnaryToMulti)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 17
)));
1475
1476 /* Embed S in Multi(). */
1477 else if (tfSatAllow(mask, TFS_AnyToNone)((mask) & ((((SatMask) 1) << 7))) && argc == 0)
1478 result = tfSatResult(mask, TFS_AnyToNone)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 7
)));
1479 }
1480
1481 else {
1482 /* Embed S in Multi(S). */
1483 if (tfSatAllow(mask, TFS_UnaryToMulti)((mask) & ((((SatMask) 1) << 17))) &&
1484 argc == 1 &&
1485 tfSatBit(tfSatInner(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((mask) & ((((SatMask)
1) << 6)))), S, Targ))
1486 result = tfSatResult(mask, TFS_UnaryToMulti)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 17
)));
1487
1488 /* Embed S in Multi(). */
1489 else if (tfSatAllow(mask, TFS_AnyToNone)((mask) & ((((SatMask) 1) << 7))) && argc == 0)
1490 result = tfSatResult(mask, TFS_AnyToNone)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 7
)));
1491 }
1492
1493 return result;
1494}
1495
1496
1497/******************************************************************************
1498 *
1499 * :: Exceptions
1500 *
1501 *****************************************************************************/
1502
1503localstatic SatMask
1504tfSatExcept(SatMask mask, TForm S, TForm T)
1505{
1506 TForm si, ti;
1507 TForm se, te;
1508 SatMask res = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
Value stored to 'res' during its initialization is never read
1509
1510 assert(tfIsExcept(T))do { if (!((((T)->tag) == TF_Except))) _do_assert(("tfIsExcept(T)"
),"tfsat.c",1510); } while (0);
1511 ti = tfExceptType(T)tfFollowArg(T, 0);
1512 te = tfExceptExcept(T)tfFollowArg(T, 1);
1513
1514 if (tfIsExcept(S)(((S)->tag) == TF_Except)) {
1515 si = tfExceptType(S)tfFollowArg(S, 0);
1516 se = tfExceptExcept(S)tfFollowArg(S, 1);
1517 }
1518 else {
1519 si = S;
1520 se = NULL((void*)0);
1521 }
1522 /* !! this is a bit naugty, as then one can write:
1523 * foo(n: Integer): Integer == {
1524 * throw BBB
1525 * }
1526 *
1527 * bar(n: Integer): Integer except ZZZ == {
1528 * foo(n)
1529 * }
1530 *
1531 * Consequently, perhaps we should infer
1532 * identifiers as
1533 * id except ()
1534 * This would be horribly inefficient, so we don't do
1535 * it yet. Plus we'd need bigtime changes to the libraries
1536 * to force 'except ()' where necessary.
1537 */
1538
1539 res = tfSat(mask, si, ti);
1540 if (!se)
1541 return res;
1542 if (tfSatSucceed(res)) {
1543 TForm sei, tej;
1544 int i, j, sc, tc;
1545 SatMask eres;
1546
1547 sc = tfAsMultiArgc(se);
1548 tc = tfAsMultiArgc(te);
1549 eres = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1550 for (i=0; i < sc && tfSatSucceed(eres); i++) {
1551 sei = tfAsMultiArgN(se, sc, i);
1552 for (j=0; j < tc; j++) {
1553 eres = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1554 tej = tfAsMultiArgN(te, tc, j);
1555 if (tfSatSucceed(tfSat(mask, sei, tej))) {
1556 eres = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1557 break;
1558 }
1559 }
1560 }
1561 res = tfSatSucceed(eres) ? res : tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1562 }
1563 return res;
1564}
1565
1566
1567/******************************************************************************
1568 *
1569 * :: Type form exports
1570 *
1571 *****************************************************************************/
1572
1573/*
1574 * Succeed if the category exports of S satisfy the category exports of T.
1575 */
1576localstatic SatMask
1577tfSatCatExports(SatMask mask, AbSyn Sab, TForm S, TForm T)
1578{
1579 TForm Sp, Tp, p;
1580 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1581
1582 Sp = tfCatExportsPending(S);
1583 Tp = tfCatExportsPending(T);
1584 p = Sp ? Sp : Tp;
1585
1586 if (DEBUG(tfsExport)tfsExportDebug) {
1587 if (p) {
1588 fprintf(dbOut, "Pending: \n");
1589 tfPrintDb(S);
1590 tfPrintDb(T);
1591 tfPrintDb(p);
1592 }
1593 }
1594
1595 if (p == NULL((void*)0)) {
1596 SymeList mods, Ssymes, Tsymes;
1597
1598 assert(tfHasCatExports(S) && tfHasCatExports(T))do { if (!(tfHasCatExports(S) && tfHasCatExports(T)))
_do_assert(("tfHasCatExports(S) && tfHasCatExports(T)"
),"tfsat.c",1598); } while (0);
1599
1600 Tsymes = listCopy(Syme)(Syme_listPointer->Copy)(tfGetCatSelfSelf(T));
1601 if (Tsymes == listNil(Syme)((SymeList) 0))
1602 Tsymes = tfGetCatParents(T, true1);
1603 if (Tsymes == listNil(Syme)((SymeList) 0))
1604 Tsymes = tfGetCatExports(T);
1605 /*
1606 * PAB: Assume that if T has no exports, then
1607 * S must be OK.
1608 */
1609 if (Tsymes == listNil(Syme)((SymeList) 0)) {
1610 if (DEBUG(tfsExport)tfsExportDebug) {
1611 fprintf(dbOut, "tfSatCatExports: 'T' has no exports\n");
1612 tfPrintDb(T);
1613 }
1614 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1615 }
1616
1617 mods = listConcat(Syme)(Syme_listPointer->Concat)(tfGetCatSelf(S), tfGetCatSelf(T));
1618
1619 Ssymes = listCopy(Syme)(Syme_listPointer->Copy)(tfGetCatSelfSelf(S));
1620 if (Ssymes == listNil(Syme)((SymeList) 0))
1621 Ssymes = tfGetCatParents(S, true1);
1622 if (Ssymes == listNil(Syme)((SymeList) 0))
1623 Ssymes = tfGetCatExports(S);
1624
1625 result = tfSatParents(mask, mods, Sab, Ssymes, Tsymes);
1626 }
1627 else if (tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6)))) {
1628 extern AbSyn symeLazyCheckData;
1629 assert(tfIsPending(p))do { if (!((((p)->state)==TF_State_Pending))) _do_assert((
"tfIsPending(p)"),"tfsat.c",1629); } while (0);
1630 result = tfSatResult(mask, TFS_Pending)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 6
)));
1631 tfSatSetPendingFail(p);
1632 if (tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)))
1633 tcNewSat(p, abCondKnown, S, T, tfSatInfo(mask)((mask) & (((SatMask) 1) << 4)) ? symeLazyCheckData : NULL((void*)0));
1634 }
1635
1636 return result;
1637}
1638
1639/*
1640 * Succeed if the 3d-order exports of S satisfy the 3d-order exports of T.
1641 */
1642localstatic SatMask
1643tfSatThdExports(SatMask mask, TForm S, TForm T)
1644{
1645 TForm Sp, Tp, p;
1646 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1647
1648 Sp = tfThdExportsPending(S);
1649 Tp = tfThdExportsPending(T);
1650 p = Sp ? Sp : Tp;
1651
1652 if (p == NULL((void*)0)) {
1653 SymeList mods;
1654
1655 assert(tfHasThdExports(S) && tfHasThdExports(T))do { if (!(tfHasThdExports(S) && tfHasThdExports(T)))
_do_assert(("tfHasThdExports(S) && tfHasThdExports(T)"
),"tfsat.c",1655); } while (0);
1656
1657 mods = listConcat(Syme)(Syme_listPointer->Concat)(tfGetThdSelf(S), tfGetThdSelf(T));
1658 result = tfSatExports(mask, mods,
1659 tfGetThdExports(S),
1660 tfGetThdExports(T));
1661 }
1662 else if (tfSatAllow(mask, TFS_Pending)((mask) & ((((SatMask) 1) << 6)))) {
1663 extern AbSyn symeLazyCheckData;
1664 assert(tfIsPending(p))do { if (!((((p)->state)==TF_State_Pending))) _do_assert((
"tfIsPending(p)"),"tfsat.c",1664); } while (0);
1665 result = tfSatResult(mask, TFS_Pending)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 6
)));
1666 tfSatSetPendingFail(p);
1667 if (tfSatCommit(mask)((mask) & (((SatMask) 1) << 1)))
1668 tcNewSat(p, abCondKnown, S, T, tfSatInfo(mask)((mask) & (((SatMask) 1) << 4)) ? symeLazyCheckData : NULL((void*)0));
1669 }
1670
1671 return result;
1672}
1673
1674/*
1675 * Succeed if each of the symes in T can be found in S.
1676 */
1677localstatic SatMask
1678tfSatExports(SatMask mask, SymeList mods, SymeList S, SymeList T)
1679{
1680 SymeList missing = tfSatExportsMissing(mask, mods, NULL((void*)0), S, T);
1681
1682 if (missing) {
1683 listFree(Syme)(Syme_listPointer->Free)(missing);
1684 return tfSatResult(mask, TFS_ExportsMissing)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 19
)));
1685 }
1686 else
1687 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1688}
1689
1690localstatic SymeList
1691tfSatExportsMissing(SatMask mask, SymeList mods, AbSyn Sab, SymeList S, SymeList T)
1692{
1693 SymeList symes, missing;
1694 AbSub lazySelfSubst;
1695
1696 if (DEBUG(tfsExport)tfsExportDebug) {
1697 fprintf(dbOut, "(->tfSatExportMissing: %*s= source list: ",
1698 tfsDepthNo, "");
1699 listPrint(Syme)(Syme_listPointer->Print)(dbOut, S, symePrint);
1700 fnewline(dbOut);
1701 }
1702
1703 missing = listNil(Syme)((SymeList) 0);
1704 lazySelfSubst = NULL((void*)0);
1705 for (symes = T; symes; symes = cdr(symes)((symes)->rest)) {
1706 Syme syme = car(symes)((symes)->first);
1707
1708 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "->tfSatExportMissing: %*s= looking for: %pSyme %pTForm\n",
1709 tfsDepthNo, "", syme, symeType(syme));
1710
1711 if (tfSatSucceed(tfSatExport(mask, mods, Sab, S, syme, &lazySelfSubst)))
1712 continue;
1713
1714 missing = listCons(Syme)(Syme_listPointer->Cons)(syme, missing);
1715 if (tfSatMissing(mask)((mask) & (((SatMask) 1) << 2)))
1716 continue;
1717
1718 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "No: %s %pSyme)\n", syme->id->str, syme);
1719
1720 return missing;
1721 }
1722
1723 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "%s)\n", missing ? "OK" : "Bad news");
1724 return missing;
1725}
1726
1727typedef struct satModAbSyn {
1728 SymeList mods;
1729 AbSyn ab;
1730} *SatModAbSyn;
1731
1732localstatic SatModAbSyn
1733satModAbSynNew(SymeList mods, AbSyn ab)
1734{
1735 SatModAbSyn satModAbSyn;
1736
1737 satModAbSyn = (SatModAbSyn) stoAlloc(OB_Other0, sizeof(*satModAbSyn));
1738 satModAbSyn->mods = mods;
1739 satModAbSyn->ab = ab;
1740 return satModAbSyn;
1741}
1742
1743localstatic void
1744satModAbSynFree(SatModAbSyn satModAbSyn)
1745{
1746 stoFree(satModAbSyn);
1747}
1748
1749localstatic AbEqualValue
1750tfSatAbCompareModAbSyn(void *ctxt, AbSyn ab1, AbSyn ab2)
1751{
1752 SatModAbSyn satModAbSyn = (SatModAbSyn) ctxt;
1753 // For ids, make sure % in ab1, if present at all
1754 if (!abIsTheId(ab1, ssymSelf)(((ab1)->abHdr.tag == (AB_Id)) && ((ab1)->abId.
sym)==(ssymSelf)) && abIsTheId(ab2, ssymSelf)(((ab2)->abHdr.tag == (AB_Id)) && ((ab2)->abId.
sym)==(ssymSelf))) {
1755 return tfSatAbCompareModAbSyn(ctxt, ab2, ab1);
1756 }
1757 if (abTag(ab1)((ab1)->abHdr.tag) != AB_Id && abTag(ab2)((ab2)->abHdr.tag) == AB_Id) {
1758 return tfSatAbCompareModAbSyn(ctxt, ab2, ab1);
1759 }
1760
1761 if (abTag(ab1)((ab1)->abHdr.tag) != AB_Id) {
1762 return AbEqual_Struct;
1763 }
1764 else if (abIsTheId(ab1, ssymSelf)(((ab1)->abHdr.tag == (AB_Id)) && ((ab1)->abId.
sym)==(ssymSelf))) {
1765 Bool eqAbSyn = abEqualModDeclares(satModAbSyn->ab, ab2);
1766 if (eqAbSyn)
1767 return AbEqual_True;
1768 else {
1769 // NB: This is a bit too lax, but we can wait for a counterexample
1770 if (abIsTheId(ab2, ssymSelf)(((ab2)->abHdr.tag == (AB_Id)) && ((ab2)->abId.
sym)==(ssymSelf))) {
1771 return AbEqual_True;
1772 }
1773 Bool eq = sefoEqualMod(satModAbSyn->mods, ab1, ab2);
1774 return eq ? AbEqual_True : AbEqual_False;
1775 }
1776 }
1777 else {
1778 Bool eq = sefoEqualMod(satModAbSyn->mods, ab1, ab2);
1779 return eq ? AbEqual_True : AbEqual_False;
1780 }
1781}
1782
1783/*
1784 * Succeed if t can be found in S.
1785 */
1786localstatic SatMask
1787tfSatExport(SatMask mask, SymeList mods, AbSyn Sab, SymeList S, Syme t, AbSub *lazySelfSubst)
1788{
1789 SatMask result = tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1790 TForm substT;
1791 SymeList symes;
1792 Bool tryHarder = true1;
1793 static int serialNo = 0;
1794 int serialThis = serialNo++;
1795
1796 /* Check for % explicitly
1797 * More exactly, as long as Sab is %, find % from t; if it corresponds to Sab or mods,
1798 * then we have the thing we want.
1799 * This fixes up cases like Rng: C == with Module(%); Module(X: Rng) == ...
1800 */
1801 if (Sab && tfHasSelf(symeType(t))((symeType(t))->hasSelf)
1802 && abIsTheId(Sab, ssymSelf)(((Sab)->abHdr.tag == (AB_Id)) && ((Sab)->abId.
sym)==(ssymSelf))) {
1803 for (symes = tfSelf(symeType(t))((symeType(t))->self); !tfSatSucceed(result) && symes; symes = cdr(symes)((symes)->rest)) {
1804 if (listMemq(Syme)(Syme_listPointer->Memq)(mods, car(symes)((symes)->first))) {
1805 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1806 }
1807 }
1808 if (tfSatSucceed(result)) {
1809 return result;
1810 }
1811 }
1812
1813 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "tfSatExport[%d]:: Start S: %pAbSyn\n", serialThis, Sab);
1814 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "tfSatExport[%d]:: Target %pSyme %pTForm\n", serialThis, t, symeType(t));
1815
1816 if (symeHasDefault(t)(((((t)->kind == SYME_Trigger ? libGetAllSymes((t)->lib
) : ((void*)0)), (t))->bits) & (0x0080)) && !symeIsSelfSelf(t)(((t)->id) == ssymSelfSelf))
1817 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1818
1819 /* First round.. try "normally" */
1820 int iterCount = 0;
1821 for (symes = S; !tfSatSucceed(result) && symes; symes = cdr(symes)((symes)->rest)) {
1822 SatMask satConditions;
1823 Syme s = car(symes)((symes)->first);
1824 int iterThis = iterCount++;
1825
1826 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "tfSatExport[%d.%d]:: Test %pSyme %pTForm %pAbSynList\n",
1827 serialThis, iterThis, s, symeType(s), symeCondition(s));
1828 if (!symeEqualModConditions(mods, s, t))
1829 continue;
1830 satConditions = tfSatConditions(mask, mods, s, t);
1831 if (tfSatSucceed(satConditions)) {
1832 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1833 tryHarder = false((int) 0);
1834 }
1835 else if (tfSatPending(satConditions)) {
1836 result = tfSatPending(mask);
1837 tryHarder = false((int) 0);
1838 }
1839 }
1840
1841 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "tfSatExport[%d]:: Incoming S: %pAbSyn retry: %d\n", serialThis, Sab, tryHarder);
1842
1843 if (!tryHarder)
1844 return result;
1845
1846 if (Sab == NULL((void*)0))
1847 return result;
1848
1849 /* Second time, with feeling. */
1850 /* More precisely, we substitute anything in 'mods' with the original
1851 * 'S' Sefo, if we have it. The assumption is the mods should contain
1852 * various local values for '%', and swapping them with the value used locally
1853 * should let us match 'Foo %' with 'Foo X'.
1854 */
1855
1856 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "(tfSatExportExtra[%d]:: Incoming S: %pAbSyn %pTForm\n",
1857 serialThis, Sab, symeType(t));
1858
1859 SatModAbSyn satModAbSyn = satModAbSynNew(mods, Sab);
1860 for (symes = S; !tfSatSucceed(result) && symes; symes = cdr(symes)((symes)->rest)) {
1861 Syme s = car(symes)((symes)->first);
1862 Bool weakEq;
1863
1864 if (symeId(s)((s)->id) != symeId(t)((t)->id)) {
1865 continue;
1866 }
1867
1868 if (!abHasSymbol(tfExpr(symeType(s))tfToAbSyn(symeType(s)), ssymSelf))
1869 continue;
1870
1871 //substS = tfSubst(sigma, symeType(s));
1872 //weakEq = abEqualModDeclares(tfExpr(substS), tfExpr(substT));
1873 weakEq = abCompareModDeclares(tfSatAbCompareModAbSyn, satModAbSyn, tfExpr(symeType(s))tfToAbSyn(symeType(s)), tfExpr(symeType(t))tfToAbSyn(symeType(t)));
1874
1875 if (weakEq) {
1876 if (symeCondition(s) != listNil(Sefo)((SefoList) 0)) {
1877 result = tfSatConditions(mask, mods, s, t);
1878 }
1879 else {
1880 result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1881 }
1882 }
1883 }
1884 satModAbSynFree(satModAbSyn);
1885
1886 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, " tfSatExportExtra[%d]:: --> %d)\n",
1887 serialThis, tfSatSucceed(result));
1888
1889 return result;
1890}
1891
1892AbSub
1893tfSatExportLazySelfSubst(SymeList mods, Sefo Sab, AbSub *lazySelfSubst)
1894{
1895 AbSub sigma = *lazySelfSubst;
1896 if (sigma == NULL((void*)0)) {
1897 sigma = absFrSymes(stabFile(), mods, Sab);
1898 *lazySelfSubst = sigma;
1899 }
1900 return sigma;;
1901}
1902
1903
1904extern TForm tiGetTForm (Stab, AbSyn);
1905
1906static SatMask tfSatConditionOnSelf(SatMask mask, SymeList mods, Syme s, Sefo property);
1907
1908localstatic SatMask
1909tfSatConditions(SatMask mask, SymeList mods, Syme s, Syme t)
1910{
1911 SefoList Sconds = symeCondition(s);
1912 SefoList Tconds = symeCondition(t);
1913 SatMask result = tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1914 static int count = 0;
1915 int serial = count++;
1916
1917 for (; Sconds; Sconds = cdr(Sconds)((Sconds)->rest)) {
1918 Sefo cond = car(Sconds)((Sconds)->first);
1919 if (sefoListMemberMod(mods, cond, Tconds))
1920 continue;
1921 if (sefoListMemberMod(mods, cond, tfSatConds()))
1922 continue;
1923
1924 /*
1925 * This is to remove any trivially satisfied conditions
1926 * remaining on `s'.
1927 * Should consider squelching the condition out of the
1928 * export list.
1929 */
1930 if (abTag(cond)((cond)->abHdr.tag) == AB_Has) {
1931 TForm tfdom, tfcat;
1932 AbSyn dom, cat;
1933
1934 if (abIsTheId(cond->abHas.expr, ssymSelf)(((cond->abHas.expr)->abHdr.tag == (AB_Id)) && (
(cond->abHas.expr)->abId.sym)==(ssymSelf))) {
1935 if (tfSatSucceed(tfSatConditionOnSelf(mask, mods, s, cond->abHas.property)))
1936 continue;
1937 else
1938 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1939 }
1940 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "(%d Check condition %pSyme %pTForm %pAbSyn\n", serial, s, symeType(s), cond);
1941 dom = cond->abHas.expr;
1942 tfdom = abGetCategory(dom);
1943 if (tfTestSeen(tfdom, cond->abHas.property)) {
1944 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1945 }
1946 if (tfSatUseConditions(mask)((mask) & (((SatMask) 1) << 5)) && abCondKnown != NULL((void*)0)) {
1947 TForm tfdomNew = ablogImpliedType(abCondKnown, dom, tfdom);
1948 if (tfdomNew != NULL((void*)0)) {
1949 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "Domain switch: %pTForm --> %pTForm\n", tfdom, tfdomNew);
1950 tfdom = tfdomNew;
1951 }
1952 }
1953 cat = cond->abHas.property;
1954 tfcat = abTForm(cat)((cat)->abHdr.seman ? (cat)->abHdr.seman->tform : 0) ? abTForm(cat)((cat)->abHdr.seman ? (cat)->abHdr.seman->tform : 0) : tiTopFns()->tiGetTopLevelTForm(ablogTrue(), cat);
1955 tfTestPush(tfdom, cond->abHas.property);
1956 result = tfSat1(mask, dom, tfdom, tfcat);
1957 tfTestPop(tfdom, cond->abHas.property);
1958
1959 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, " %d Check condition %pSyme %oBool)\n", serial, s, tfSatSucceed(result));
1960 if (tfSatSucceed(result))
1961 continue;
1962 else if (tfSatPending(result)) {
1963 result = tfSatResult(mask, TFS_Pending)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 6
)));
1964 continue;
1965 }
1966 }
1967 return tfSatFalse(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 18
)));
1968 }
1969 return result;
1970}
1971
1972SatMask
1973tfSatConditionOnSelf(SatMask mask, SymeList mods, Syme s, Sefo property)
1974{
1975 tfsExportDEBUGif (!tfsExportDebug) { } else afprintf(dbOut, "tfsExport: Check self condition %pSyme %pTForm %pAbSyn\n", s, symeType(s), property);
1976 // Might as well say true as this is an export list.. need to retain
1977 // in case it becomes true on import
1978 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
1979}
1980
1981
1982localstatic Bool
1983sefoListMemberMod(SymeList mods, Sefo sefo, SefoList sefos)
1984{
1985 for (; sefos; sefos = cdr(sefos)((sefos)->rest))
1986 if (sefoEqualMod(mods, sefo, car(sefos)((sefos)->first)))
1987 return true1;
1988 return false((int) 0);
1989}
1990
1991static TFormList TfSatCondTypes = listNil(TForm)((TFormList) 0);
1992static SefoList TfSatCondExprs = listNil(Sefo)((SefoList) 0);
1993
1994localstatic void
1995tfSatPushMapConds(TForm tfm)
1996{
1997 Length i, argc = tfMapArgc(tfm);
1998
1999 for (i = 0; i < argc; i += 1) {
2000 TForm tfi = tfMapArgN(tfm, i);
2001 if (!tfIsDeclare(tfi)(((tfi)->tag) == TF_Declare)) continue;
2002
2003 listPush(TForm, tfi, TfSatCondTypes)(TfSatCondTypes = (TForm_listPointer->Cons)(tfi, TfSatCondTypes
));
2004 if (TfSatCondExprs)
2005 listPush(Sefo, tfSatCond(tfi), TfSatCondExprs)(TfSatCondExprs = (Sefo_listPointer->Cons)(tfSatCond(tfi),
TfSatCondExprs));
2006 }
2007}
2008
2009localstatic void
2010tfSatPopMapConds(TForm tfm)
2011{
2012 Length i, argc = tfMapArgc(tfm);
2013
2014 for (i = 0; i < argc; i += 1) {
2015 TForm tfi = tfMapArgN(tfm, i);
2016 if (!tfIsDeclare(tfi)(((tfi)->tag) == TF_Declare)) continue;
2017
2018 TfSatCondTypes = listFreeCons(TForm)(TForm_listPointer->FreeCons)(TfSatCondTypes);
2019 if (TfSatCondExprs)
2020 TfSatCondExprs = listFreeCons(Sefo)(Sefo_listPointer->FreeCons)(TfSatCondExprs);
2021 }
2022}
2023
2024localstatic SefoList
2025tfSatConds(void)
2026{
2027 TFormList types;
2028 SefoList exprs = listNil(Sefo)((SefoList) 0);
2029
2030 if (!TfSatCondExprs) {
2031 for (types = TfSatCondTypes; types; types = cdr(types)((types)->rest))
2032 exprs = listCons(Sefo)(Sefo_listPointer->Cons)(tfSatCond(car(types)((types)->first)), exprs);
2033 TfSatCondExprs = listNReverse(Sefo)(Sefo_listPointer->NReverse)(exprs);
2034 }
2035
2036 return TfSatCondExprs;
2037}
2038
2039localstatic Sefo
2040tfSatCond(TForm tf)
2041{
2042 assert(tfIsDeclare(tf))do { if (!((((tf)->tag) == TF_Declare))) _do_assert(("tfIsDeclare(tf)"
),"tfsat.c",2042); } while (0);
2043 return abHas(tfDefineeSyme(tf), tfDefineeType(tf));
2044}
2045
2046/*
2047 * Succeed if each of the symes in T can be found in the parent tree
2048 * for the symes in S.
2049 */
2050localstatic SatMask
2051tfSatParents(SatMask mask, SymeList mods, AbSyn Sab, SymeList S, SymeList T)
2052{
2053 SymeList newS = S, oldS = listNil(Syme)((SymeList) 0);
2054 SymeList queue = listNil(Syme)((SymeList) 0);
2055 SymeTSet oldTbl = tsetCreateCustom(Syme)(Syme_tsetPointer->CreateCustom)(symeHashFn, symeEqual);
2056 int serialThis;
2057 int iterThis = 0;
2058
2059 tfsSerialNo += 1;
2060 serialThis = tfsSerialNo;
2061
2062 /* Collect all of the missing exports. */
2063 mask |= TFS_Missing(((SatMask) 1) << 2);
2064
2065 tfsParentDEBUGif (!tfsParentDebug) { } else afprintf(dbOut, "(->tfpSyme: %*s%d = source list: %pSymeList\n",
2066 tfsDepthNo, "", serialThis, S);
2067
2068 while (newS || queue) {
2069 iterThis++;
2070 SymeList currentS = newS;
2071 T = tfSatExportsMissing(mask, mods, Sab, currentS, T);
2072 if (T == listNil(Syme)((SymeList) 0)) {
2073 tfsParentDEBUGif (!tfsParentDebug) { } else afprintf(dbOut, " ->tfpSyme: %*s%d = No parents)\n", tfsDepthNo, "", serialThis);
2074 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
2075 }
2076 newS = tfSatParentsFilterTable(oldTbl, currentS);
2077 queue = listNConcat(Syme)(Syme_listPointer->NConcat)(queue, listCopy(Syme)(Syme_listPointer->Copy)(newS));
2078 tsetAddAll(Syme)(Syme_tsetPointer->AddAll)(oldTbl, newS);
2079
2080 if (queue) {
2081 Syme oldSyme = car(queue)((queue)->first);
2082
2083 tfsParentDEBUGif (!tfsParentDebug) { } else afprintf(dbOut, " ->tfpSyme: %*s%d.%d= expanding: %pSyme %pTForm %pAbSynList\n",
2084 tfsDepthNo, "", serialThis, iterThis, oldSyme,
2085 symeType(oldSyme), symeCondition(oldSyme));
2086
2087 newS = tfGetCatParents(symeType(oldSyme), true1);
2088 /*
2089 if (symeCondition(oldSyme) != listNil(Sefo)) {
2090 newS = symeListAddCondition(newS, abNewOfList(AB_And, sposNone,
2091 (AbSynList) symeCondition(oldSyme)), true);
2092 }
2093 */
2094 queue = cdr(queue)((queue)->rest);
2095
2096 tfsParentDEBUGif (!tfsParentDebug) { } else afprintf(dbOut, " ->tfpSyme: %*s%d.%d= into: %pSymeList\n",
2097 tfsDepthNo, "", serialThis, iterThis, newS);
2098 }
2099 else
2100 newS = listNil(Syme)((SymeList) 0);
2101 }
2102 tfsParentDEBUGif (!tfsParentDebug) { } else afprintf(dbOut, " ->tfpSyme: %*s%d= Left: %pSymeList)\n",
2103 tfsDepthNo, "", serialThis, T);
2104 if (T == listNil(Syme)((SymeList) 0))
2105 return tfSatTrue(mask)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | (((SatMask) 0)));
2106 tsetFree(Syme)(Syme_tsetPointer->Free)(oldTbl);
2107 while (T && tfsParentDebug) {
2108 tfsParentDEBUGif (!tfsParentDebug) { } else afprintf(dbOut, "%d Missing %pAbSyn %pSyme: %pTForm %pAbSynList\n", serialThis, Sab, car(T)((T)->first),
2109 symeType(car(T)((T)->first)),
2110 symeCondition(car(T)((T)->first)));
2111 T = cdr(T)((T)->rest);
2112 }
2113
2114 return tfSatResult(mask, TFS_ExportsMissing)(((mask) & ( (((SatMask) 1) << 0) | (((SatMask) 1) <<
1) | (((SatMask) 1) << 2) | (((SatMask) 1) << 3)
| (((SatMask) 1) << 4) )) | ((((SatMask) 1) << 19
)));
2115}
2116
2117localstatic SymeList
2118tfSatParentsFilterTable(SymeTSet tbl, SymeList nsymes)
2119{
2120 SymeList symes, rsymes = listNil(Syme)((SymeList) 0);
2121 /* Collect symes for %% which have not been seen before. */
2122 for (symes = nsymes; symes; symes = cdr(symes)((symes)->rest))
2123 if (symeIsSelfSelf(car(symes))(((((symes)->first))->id) == ssymSelfSelf) &&
2124 !tsetMember(Syme)(Syme_tsetPointer->Member)(tbl, car(symes)((symes)->first)))
2125 rsymes = listCons(Syme)(Syme_listPointer->Cons)(car(symes)((symes)->first), rsymes);
2126
2127 listFree(Syme)(Syme_listPointer->Free)(nsymes);
2128 return listNReverse(Syme)(Syme_listPointer->NReverse)(rsymes);
2129
2130}
2131
2132
2133
2134localstatic String
2135tfSatMaskToString(SatMask mask)
2136{
2137 String sep="";
2138 if (mask == TFS_Succeed((SatMask) 0)) {
2139 return "Success";
2140 }
2141 else {
2142 Buffer b = bufNew();
2143 OStream os = ostreamNewFrBuffer(b);
2144 int i = 0;
2145
2146 while (tfSatMaskInfo[i].name != 0) {
2147 if (mask & (1<<i)) {
2148 ostreamWrite(os, sep, -1);
2149 ostreamWrite(os, tfSatMaskInfo[i].name, -1);
2150 sep = "|";
2151 }
2152 i++;
2153 }
2154 ostreamFree(os);
2155 return bufLiberate(b);
2156 }
2157}
2158
2159/******************************************************************************
2160 *
2161 * :: Type form satisfaction flags.
2162 *
2163 *****************************************************************************/
2164
2165static TForm tfSatPendingFailValue;
2166
2167localstatic void
2168tfSatSetPendingFail(TForm S)
2169{
2170 tfSatPendingFailValue = S;
2171}
2172
2173TForm
2174tfSatGetPendingFail()
2175{
2176 return tfSatPendingFailValue;
2177}