1module form4;   % Type analysis for REDUCE 4.
2
3% Authors:  Anthony C. Hearn, Eberhard Schruefer.
4
5% Redistribution and use in source and binary forms, with or without
6% modification, are permitted provided that the following conditions are met:
7%
8%    * Redistributions of source code must retain the relevant copyright
9%      notice, this list of conditions and the following disclaimer.
10%    * Redistributions in binary form must reproduce the above copyright
11%      notice, this list of conditions and the following disclaimer in the
12%      documentation and/or other materials provided with the distribution.
13%
14% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
15% AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
16% THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
17% PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR
18% CONTRIBUTORS
19% BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20% CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21% SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22% INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23% CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24% ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25% POSSIBILITY OF SUCH DAMAGE.
26%
27
28
29fluid '(!*specification !*specification_reduce !*generate_retracts
30        !*instantiate);
31
32switch instantiate,specification;
33
34% If the switch specification is on, all expression are checked for type
35% consistency at form-time. For this to work it is necessary that all
36% ranks and type relations are set up prior to function definitions.
37% In the code below any n_form function is required to return a list
38% whose first element is the ceiling type of the formed expression and
39% the second element is the formed expression. The toplevel function
40% n_form returns only the formed expression.
41
42%!*specification := t;
43
44symbolic procedure n_form u;
45   % Car of n_form1 is the ceiling type.  Cadr is a typed expression.
46   cadr n_form1(u,!*vars!*);
47
48symbolic procedure n_form1(u,vars);
49   begin scalar x,z,ctype,arity_pairs,args,fnc;
50      return if atom u
51     then if numberp u
52            then if fixp u
53                    then if u=0
54                            then <<z := pckg_type 'zero;
55                                   {z, mkquote {z,0}}>>
56                          else <<z := pckg_type 'int;
57                                 {z,mkquote type_reduce(u,z)}>>
58             else {'float,mkquote list('float,u)}
59           else if stringp u then {'string,mkquote {'string,u}}
60           else if arrayp u then {'array,mkquote {'array,u}}
61           else if x := atsoc(u,vars) then {cdr x, u}
62%          else if (x := get(u,'type)) then mkquote {x,mkquote u}
63%               % type_reduce
64           else if x := get(u,'avalue)
65                then {type x,{'ideval,mkquote u}}
66           else {x := pckg_type 'variable,{'ideval,mkquote u}}
67    else if not idp car u then typerr(car u,"operator")
68    else if (null cdr u and car u neq 'list) or flagp(car u,'non_form)
69     then {'non_form,u}
70    else if flagp(car u,'non_form) then {'non_form,u}
71    else if (x := get(car u,'n_formfn)) then apply2(x,u,vars)
72    % See if a direct result can be formed.
73    else if x := get(car u,'xform)
74     then x . for each j in cdr u collect n_form1(j,vars)
75    else <<x := for each j in cdr u collect n_form1(j,vars);
76           arity_pairs := for each j in x collect {type j};
77           args := for each j in x collect value j;
78    % If there is a type constraint, it cannot be resolved in general.
79    % The highest type must then be returned as the coarity.
80           fnc := type_function2(car u,arity_pairs,args);
81           ctype := if null fnc then if !*specification
82                       then rederr{"no meaning for",car u,x}
83                     else 'generic
84                 else cadr fnc;
85           if !*generate_retracts then
86              args := for each arg in args collect
87                        <<x := arity_pairs;
88                          arity_pairs := cdr arity_pairs;
89 %                         if cdar x and (xxxxx := atsoc(arg,vars))
90 %                            then rplacd(xxxxx,cadar x);
91                          if cdar x then mkretract(caar x,cadar x,arg)
92                           else arg>>;
93           if !*instantiate and fnc
94%            then {ctype,mk_type_reduce(car fnc . args,ctype)}
95             then {ctype,{'type_reduce1,car fnc . args}}
96 %           else if !*specification_reduce
97 %             then {ctype,{'type_reduce1,
98 %                          {'rapply,mkquote car u,'list . args},ctype}}
99            else
100           {ctype,{'rapply,mkquote car u,'list . args}}>>
101   end;
102
103
104
105symbolic procedure mk_type_reduce(u,v);
106   % We must not call type_reduce when defining a sort constraint for
107   % type v, as we would loop otherwise.
108   if flagp(v,'defining) then mkquote {v,u}
109    else {'type_reduce,u,mkquote v};
110
111symbolic procedure type_function2(fn,typelist,args);
112   % Returns disambiguated function symbol for fn.
113   % If retracts are necessary, typelist is destructively changed.
114   % Type constraints are ignored as we are here only interested
115   % in ceiling types and more information can only be derived
116   % by formal proofs.
117   begin scalar x;
118      return if (x := get(fn,'ranks))
119                and (x := assoc(length typelist,x))
120                and (x := type_assocf(typelist,cdr x,args))
121               then x
122              else nil
123   end;
124
125symbolic procedure type_assocf(typelist,type_assoc_list,args);
126   % Determine if there's a match for typelist in type_assoc_list.
127   begin scalar x;
128     if x :=
129        type_assoc1f(car typelist,cdr typelist,type_assoc_list,args)
130        then return x
131      else if x := atsoc('generic,type_assoc_list)
132        then return cdr x
133      else return nil
134   end;
135
136
137symbolic procedure type_assoc1f(type,typelist,type_assoc_list,args);
138   begin scalar x,y,z;
139      if (type_in_pckgp type and
140          (x := type_assoc0f(type,type_assoc_list)))
141%         or (x := atsoc('generic,type_assoc_list))
142        then if null typelist
143        then return ceiling_of_constraints cdaddr cdr x
144         % We assume termination with the actual name of function here.
145       else if y := type_assoc1f(car typelist,cdr typelist,cdr x,args)
146               then return y;
147      if z := get(car type,'uptree)
148        then <<while z and
149                 not (x := type_assoc1f(rplaca(type,car z),
150                                        typelist,type_assoc_list,args))
151                 do z := cdr z; return x>>
152       else return nil
153   end;
154
155symbolic procedure ceiling_of_constraints u;
156   if null u then nil
157    else if caar u eq t then cadadr car u
158    else ceiling_of_constraints cdr u;
159
160symbolic procedure type_assoc0f(type,type_assoc_list);
161   if null type_assoc_list then nil
162    else if car type eq caar type_assoc_list  then car type_assoc_list
163    else if xtype1(caar type_assoc_list,car type) and !*specification
164            then <<lprim {type," -> ",caar type_assoc_list};
165                   car type_assoc_list; rplacd(type,{caar type_assoc_list});
166                   car type_assoc_list>>
167% The above finds a resolution but it might be lower than intended.
168% Is the solution to find the closest node or need we to generate all????
169    else type_assoc0f(type,cdr type_assoc_list);
170
171
172flag('(load),'non_form);
173
174put('type,'xform,'type_1);
175
176symbolic procedure type_1 u; list('variable,type u);
177
178symbolic procedure n_formbool(u,vars);
179 %%% Should we check if type of u is liftable to bool ???
180 %%% Would like to get rid of n_boolvalue*.
181   begin scalar x;
182     if atom u then if u eq 't then return {'bool,u}
183      else if x := atsoc(u,vars)
184              then if (cdr x eq 'bool) or (cdr x eq 'generic)
185                      then return {'bool,list('n_boolvalue!*,u)}
186                    else rederr {"a boolean was expected, but got",cdr x};
187     x := n_form1(u,vars);
188     if null((type x eq 'bool) or (type x eq 'generic))
189        then rederr {"a boolean was expected, but got",type x};
190     return {'bool,list('n_boolvalue!*,value x)}
191   end;
192
193symbolic procedure n_boolvalue!* u; (v and null(v = 0)) where v=value u;
194
195%  --- COND ---
196
197symbolic procedure n_formcond(u,vars);
198   {type x,'cond . value x} where x = n_formcond1(cdr u,vars);
199
200symbolic procedure n_formcond1(u,vars);
201   % We need to consider generic a bit more carefully here.
202   begin scalar v,eptr,x,restype;
203     v := eptr := {nil};
204     a: if null u then return {restype,cdr v};
205        x := n_form1(cadar u,vars);
206        if null restype
207           then restype := type x
208         else if xtype1(type x,restype) then nil
209         else if xtype1(restype,type x) then restype := type x
210         else rederr {"types in conditional",type x,"and",restype,
211                      "are unrelated"};
212        eptr := cdr rplacd(eptr,{{value n_formbool(caar u,vars),
213                                  value x}});
214        u := cdr u;
215        go to a
216    end;
217
218put('cond,'n_formfn,'n_formcond);
219
220%  --- LIST ----
221
222symbolic procedure n_formlist(u,vars); % parametrization ??? very crude version
223   begin scalar x,y,eltype;
224     if null cdr u then return {'empty_list,''(empty_list nil)};
225     x := n_form1(cadr u,vars);
226     eltype := type x;
227     y := value x;
228     y := y . for each j in cddr u
229                  collect <<x := n_form1(j,vars);
230%                           if xtype1(type x,eltype) then nil
231%                            else if xtype1(eltype,type x)
232%                                    then eltype := type x
233%                            else rederr {"types in list",type x,
234%                                         "and",eltype,"are unrelated"};
235                            value x>>;
236     return {'non_empty_list,{'mklistt,'list . y}}
237   end;
238
239symbolic procedure mklistt u;   %%% this is not consistent with others
240   type_reduce(u,'list);
241
242put('list,'n_formfn,'n_formlist);
243
244
245%  --- PROGN ---
246
247symbolic procedure n_formprogn(u,vars);
248   begin scalar restype,x;
249     x := for each j in cdr u
250             collect <<restype := n_form1(j,vars);
251                       value restype>>;
252     return {type restype,'progn . x}
253   end;
254
255put('progn,'n_formfn,'n_formprogn);
256
257%  --- SETQ ---
258
259symbolic procedure n_formsetq(u,vars);
260   begin scalar x,y,z;
261   % Note that target type (car z) is target type of assignment.
262   z := n_form1(caddr u,vars);
263   if idp cadr u and (x := atsoc(cadr u,vars)) then
264     <<if not(cdr x eq 'generic)
265          then if xtype1(type z,cdr x) then nil
266                else if xtype1(cdr x,type z)
267                        then lprim {"assignment is only valid if type of rhs",
268                                    type z,"is retractable to",cdr x}
269                else rederr {"type of lhs",cdr x,
270                             "in assignment is unrelated to ceiling type",
271                              type z,"of rhs"};
272       return {car z,list('setq,cadr u,cadr z)}>> else
273    if not atom cadr u and (x := getobject caadr u)
274       and (y := get(type x,'putfn)) then
275     return {car z,{y,mkquote x,'list . for each j in cdadr u collect
276                        cadr n_form1(j,vars),cadr z}} else
277     return {car z,{'rapply,mkquote 'setq,{'list,
278                      {'mkobject,mkquote cadr u,mkquote 'variable},
279                      cadr z}}}
280   end;
281
282put('setq,'n_formfn,'n_formsetq);
283
284endmodule;
285
286end;
287