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