1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(z_typechecker, [ | |
6 | %z_type/4, | |
7 | global_environment/3, | |
8 | extract_btypes/3, | |
9 | internal2b/2, | |
10 | %remove_typeinfos/2, | |
11 | ti_expr/2, | |
12 | ti_type/2, | |
13 | zfields2b/3, | |
14 | remove_fields_by_name/3 | |
15 | %unify_generic/4 | |
16 | ]). | |
17 | ||
18 | :- use_module(library(lists)). | |
19 | ||
20 | :- use_module(probsrc(error_manager),[add_error/3,add_warning/3]). | |
21 | :- use_module(probsrc(tools)). | |
22 | ||
23 | :- use_module(probsrc(module_information)). | |
24 | :- module_info(group,proz). | |
25 | :- module_info(description,'This module contains a type checker for Z specifications, mainly because the types are needed for the translation to B.'). | |
26 | ||
27 | :- use_module(fuzzfile). | |
28 | :- use_module(proz). | |
29 | :- use_module(schemavars). | |
30 | :- use_module(z_tools). | |
31 | :- use_module(subexpressions). | |
32 | :- use_module(zparameters). | |
33 | :- use_module(zenvironment). | |
34 | ||
35 | %******************************************************************************** | |
36 | % Type checking expressions | |
37 | z_type([],_,[],[]) :- !. | |
38 | z_type([Expr|Rest],Env,[Type|TRest],[AExpr|ARest]) :- | |
39 | !,z_type(Expr,Env,Type,AExpr), | |
40 | z_type(Rest,Env,TRest,ARest). | |
41 | z_type(Expr,Env,Type,ti(AnnotatedExpr,Type)) :- | |
42 | if(z_type2(Expr,Env,AnnotatedExpr,Type),true, | |
43 | (add_warning(z_typechecker,'Typing expression failed: ',Expr), | |
44 | fail)). | |
45 | ||
46 | ti_expr(ti(Expr,_),Expr). | |
47 | ti_type(ti(_,Type),Type). | |
48 | ||
49 | update_params(name('\\emptyset',_),[_],Params) :- !, Params=[]. % remove now useless parameter of \emptyset; otherwise Z consistency check will complain as currently the Param of \emptyset is not typed itself (I don't know why; probably because \emptyset is registered as a 0-ary construct) | |
50 | update_params(_,P,P). | |
51 | ||
52 | z_type2(ref(Name,Params),Env,ref(Name,NewParams),Type) :- | |
53 | ( lookup_type(Env,Name,T) -> | |
54 | ( nonvar(T),T=generic(GenParams,GenType) -> | |
55 | prepare_generic(Params,Env,GenType,GenParams,Type) | |
56 | ; Type=T -> true | |
57 | ; add_warning(proz,'Type mismatch: ',Name:Type:T),fail | |
58 | ), | |
59 | update_params(Name,Params,NewParams) | |
60 | ; | |
61 | add_error(proz,'Internal error: Unknown type of ', Name), fail). | |
62 | ||
63 | z_type2(number(N),_,number(N),num). | |
64 | ||
65 | z_type2(apply(Ref,Arg),Env,apply(RefTI,ArgTI),ResultType) :- | |
66 | z_type(Ref,Env,FunType,RefTI), | |
67 | zrel(ArgType,ResultType,FunType), | |
68 | z_type(Arg,Env,ArgType,ArgTI). | |
69 | ||
70 | z_type2(inop(Name,A,B),Env,inop(Name,Ati,Bti),Type) :- | |
71 | ti_expr(ApplyTI,apply(_,ArgTI)), | |
72 | ti_expr(ArgTI,tuple([Ati,Bti])), | |
73 | z_type(apply(ref(Name,[]),tuple([A,B])),Env,Type,ApplyTI). | |
74 | z_type2(ingen(Name,A,B),Env,ingen(Name,Ati,Bti),Type) :- | |
75 | ti_expr(InopTI,inop(_,Ati,Bti)), | |
76 | z_type(inop(Name,A,B),Env,Type,InopTI). | |
77 | ||
78 | z_type2(postop(Name,Arg),Env,postop(Name,ArgTI),Type) :- | |
79 | ti_expr(ApplyTI,apply(_,ArgTI)), | |
80 | z_type(apply(ref(Name,[]),Arg),Env,Type,ApplyTI). | |
81 | z_type2(pregen(Name,Arg),Env,pregen(Name,ArgTI),Type) :- | |
82 | z_type2(postop(Name,Arg),Env,postop(_,ArgTI),Type). | |
83 | ||
84 | z_type2(inrel(Name,A,B),Env,inrel(Name,Ati,Bti),Type) :- | |
85 | ti_expr(MemTI,member(TupleTI,_)), | |
86 | ti_expr(TupleTI,tuple([Ati,Bti])), | |
87 | z_type(member(tuple([A,B]),ref(Name,[])),Env,Type,MemTI). | |
88 | z_type2(prerel(Name,Arg),Env,prerel(Name,ArgTI),Type) :- | |
89 | ti_expr(MemTI,member(ArgTI,_)), | |
90 | z_type(member(Arg,ref(Name,[])),Env,Type,MemTI). | |
91 | ||
92 | z_type2(equal(A,B), Env, equal(Ati,Bti), bool) :- | |
93 | z_types_common([A,B],Env,_,[Ati,Bti]). | |
94 | z_type2(member(A,B), Env, member(Ati,Bti), bool) :- | |
95 | z_type(A,Env,Type,Ati), | |
96 | z_type(B,Env,set(Type),Bti). | |
97 | z_type2(power(A), Env, power(Ati),set(Type)) :- | |
98 | z_type(A,Env,Type,Ati). | |
99 | ||
100 | z_type2(cross(Args), Env, cross(TypeInfos), set(tuple(Types))) :- | |
101 | z_type_sets(Args, Env, Types, TypeInfos). | |
102 | z_type2(tuple(Args), Env, tuple(TypeInfos), tuple(Types)) :- | |
103 | z_type_l(Args, Env, Types,TypeInfos). | |
104 | z_type2(if(If,Then,Else), Env, if(Ifti,Thenti,Elseti), Type) :- | |
105 | z_type(If,Env,bool,Ifti), | |
106 | z_type(Then,Env,Type,Thenti), | |
107 | z_type(Else,Env,Type,Elseti). | |
108 | ||
109 | z_type2(ext(Expressions), Env, ext(TypeInfos), set(Type)) :- | |
110 | z_types_common(Expressions,Env,Type,TypeInfos). | |
111 | z_type2(seq(Expressions), Env, seq(TypeInfos), Type) :- | |
112 | zseq(IType,Type), | |
113 | z_types_common(Expressions,Env,IType,TypeInfos). | |
114 | z_type2(bag(Expressions), Env, bag(TypeInfos), set(tuple([Type,num]))) :- | |
115 | z_types_common(Expressions,Env,Type,TypeInfos). | |
116 | ||
117 | z_type2(theta(Name,Deco,Renamings), Env, theta(Name,Deco,Renamings), Type) :- | |
118 | z_type(sref(Name,'',[],[]),Env,set(Type),_). | |
119 | ||
120 | z_type2(sexpr(Sexpr), Env, sexpr(SexprTi), Type) :- | |
121 | z_type(Sexpr,Env,Type,SexprTi). | |
122 | z_type2(select(Record,Field), Env, select(RecordTi,Field), Type) :- | |
123 | z_type(Record,Env,schema(Fields),RecordTi), | |
124 | type_of_field(Fields,Field,Type). | |
125 | ||
126 | z_type2(lambda(Body,Expr), Env, lambda(BodyTi,ExprTi), Type) :- | |
127 | Body = body(Decls,_), | |
128 | declaration_tuple(Decls,Env,Tuple), | |
129 | ti_expr(TypeInfo,comp(BodyTi,JustTi)), | |
130 | ti_expr(InopTi,inop(_,_,ExprTi)), | |
131 | ti_expr(JustTi,just(InopTi)), | |
132 | z_type(comp(Body,just(inop(name('\\mapsto',''),Tuple,Expr))), | |
133 | Env,Type,TypeInfo). | |
134 | z_type2(comp(Body,Expr), Env, comp(BodyTi,ExprTi), set(Type)) :- | |
135 | ti_expr(TypeInfo,mu(BodyTi,ExprTi)), | |
136 | z_type(mu(Body,Expr),Env,Type,TypeInfo). | |
137 | z_type2(mu(Body,MuExpr), Env, mu(BodyTi,ExprTypeInfo), Type) :- | |
138 | ( MuExpr = nothing -> | |
139 | ExprTypeInfo = ti(nothing,none), | |
140 | Body = body(Decls,_),declaration_tuple(Decls,Env,Tuple), | |
141 | ti_expr(TypeInfo,mu(BodyTi,_)), | |
142 | z_type(mu(Body,just(Tuple)), Env, Type, TypeInfo) | |
143 | ; MuExpr = just(Expr) -> | |
144 | z_type_body(Body,Env,_,BodyTi,Subenv), | |
145 | z_type(just(Expr),Subenv,_,ExprTypeInfo), | |
146 | ti_expr(ExprTypeInfo,just(ExprTi)), | |
147 | ti_type(ExprTi,Type) ). | |
148 | z_type2(letexpr(Letdefs,Expr), Env, letexpr(Lettis,ExprTi), Type) :- | |
149 | types_in_let(Letdefs,Env,LetTypes,Lettis), | |
150 | create_subenv(Env,LetTypes,LetEnv), | |
151 | z_type(Expr,LetEnv,Type,ExprTi). | |
152 | ||
153 | z_type2(nothing,_,nothing,none). | |
154 | z_type2(just(Expr),Env,just(ExprTi),none) :- | |
155 | z_type(Expr,Env,_,ExprTi). | |
156 | ||
157 | ||
158 | %******************************************************************************** | |
159 | % Type checking Predicates | |
160 | ||
161 | z_type2(falsity, _, falsity, bool). | |
162 | z_type2(truth, _, truth, bool). | |
163 | z_type2(forall(Body,Expr), Env, forall(BodyTi,ExprTi), bool) :- | |
164 | z_type_body(Body,Env,_,BodyTi,Subenv), | |
165 | z_type(Expr,Subenv,bool,ExprTi). | |
166 | z_type2(exists(Body,Expr), Env, exists(BodyTi,ExprTi), Type) :- | |
167 | z_type2(forall(Body,Expr),Env,forall(BodyTi,ExprTi),Type). | |
168 | z_type2(exists1(Body,Expr), Env, exists1(BodyTi,ExprTi), Type) :- | |
169 | z_type2(forall(Body,Expr),Env,forall(BodyTi,ExprTi),Type). | |
170 | z_type2(and(A,B), Env, and(Ati,Bti), bool) :- | |
171 | z_type(A,Env,bool,Ati),z_type(B,Env,bool,Bti). | |
172 | z_type2(or(A,B), Env, or(Ati,Bti), Type) :- | |
173 | z_type2(and(A,B),Env,and(Ati,Bti),Type). | |
174 | z_type2(implies(A,B), Env, implies(Ati,Bti), Type) :- | |
175 | z_type2(and(A,B),Env,and(Ati,Bti),Type). | |
176 | z_type2(equiv(A,B), Env, equiv(Ati,Bti), Type) :- | |
177 | z_type2(and(A,B),Env,and(Ati,Bti),Type). | |
178 | z_type2(not(E), Env, not(Eti), bool) :- z_type(E,Env,bool,Eti). | |
179 | z_type2(letpred(Letdefs,Expr), Env, letpred(Letties,ExprTi), bool) :- | |
180 | z_type2(letexpr(Letdefs,Expr), Env, letexpr(Letties,ExprTi), bool). | |
181 | z_type2(spred(SExpr), Env, spred(SExprTi), bool) :- | |
182 | z_type(SExpr,Env,set(schema(_)),SExprTi). | |
183 | ||
184 | %******************************************************************************** | |
185 | % Type checking schema expressions | |
186 | ||
187 | z_type2(sref(Name,Deco,ParamValues,Renamings), Env, sref(Name,Deco,ParamValues,Renamings), Type) :- | |
188 | zlookup_schema(Env,Name,ParamNames,Expr), | |
189 | z_type_schemabody(Expr,Deco,ParamNames,ParamValues,Renamings,Env,Type,_). | |
190 | ||
191 | z_type2(sand(A,B), Env, sand(Ati,Bti), Type) :- | |
192 | logical_bin_schema(A,B,Env,Ati,Bti,Type). | |
193 | z_type2(sor(A,B), Env, sor(Ati,Bti), Type) :- | |
194 | logical_bin_schema(A,B,Env,Ati,Bti,Type). | |
195 | z_type2(simplies(A,B), Env, simplies(Ati,Bti), Type) :- | |
196 | logical_bin_schema(A,B,Env,Ati,Bti,Type). | |
197 | z_type2(sequiv(A,B), Env, sequiv(Ati,Bti), Type) :- | |
198 | logical_bin_schema(A,B,Env,Ati,Bti,Type). | |
199 | z_type2(snot(A), Env, snot(Ati), Type) :- | |
200 | z_type(A,Env,Type,Ati). | |
201 | ||
202 | z_type2(sforall(Body,Schema), Env, sforall(BodyTi,SchemaTi), Type) :- | |
203 | type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,Type). | |
204 | z_type2(sexists(Body,Schema), Env, sexists(BodyTi,SchemaTi), Type) :- | |
205 | type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,Type). | |
206 | z_type2(sexists1(Body,Schema), Env, sexists1(BodyTi,SchemaTi), Type) :- | |
207 | type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,Type). | |
208 | z_type2(hide(Schema,Vars), Env, hide(SchemaTi,Vars), set(schema(Fields))) :- | |
209 | z_type(Schema,Env,set(schema(InnerFields)),SchemaTi), | |
210 | remove_fields_by_name(InnerFields,Vars,UFields), | |
211 | normalize_fields(UFields,Fields). | |
212 | ||
213 | z_type2(fatsemi(A,B), Env, fatsemi(Ati,Bti), set(schema(Fields))) :- | |
214 | get_fields(A,B,Env,Ati,Bti,FieldsA,FieldsB), | |
215 | composite_fields(FieldsA,FieldsB,Out,In), | |
216 | remove_fields_by_name(FieldsA,Out,Aall), | |
217 | remove_fields_by_name(FieldsB,In,Ball), | |
218 | append_not_duplicate(Aall,Ball,UFields), | |
219 | normalize_fields(UFields,Fields). | |
220 | z_type2(project(A,B), Env, project(Ati,Bti), set(schema(Fields))) :- | |
221 | z_type(A,Env,set(schema(_)),Ati), | |
222 | z_type(B,Env,set(schema(Fields)),Bti). | |
223 | z_type2(pre(Schema), Env, pre(SchemaTi), set(schema(Fields))) :- | |
224 | z_type(Schema,Env,set(schema(AllFields)),SchemaTi), | |
225 | findall(name(Name,Deco), | |
226 | (member(field(name(Name,Deco),_),AllFields), | |
227 | member(Deco,['\'','!'])), | |
228 | ToRemove), | |
229 | remove_fields_by_name(AllFields,ToRemove,UFields), | |
230 | normalize_fields(UFields,Fields). | |
231 | z_type2(pipe(A,B), Env, pipe(Ati,Bti), set(schema(Fields))) :- | |
232 | z_type(A,Env,set(schema(FieldsA)),Ati), | |
233 | z_type(B,Env,set(schema(FieldsB)),Bti), | |
234 | pipe_fields(FieldsA,FieldsB,Out,In), | |
235 | remove_fields_by_name(FieldsA,Out,AwoO), | |
236 | remove_fields_by_name(FieldsB,In,BwoI), | |
237 | append_not_duplicate(AwoO,BwoI,UFields), | |
238 | ||
239 | normalize_fields(UFields,Fields). | |
240 | ||
241 | z_type2(body(Decl,Where), Env, TypedBody, Type) :- | |
242 | z_type_body(body(Decl,Where),Env,Type,BodyTi,_), | |
243 | ti_expr(BodyTi,TypedBody). | |
244 | z_type2(text(Text), Env, text(TextTi), Type) :- | |
245 | z_type(Text,Env,Type,TextTi). | |
246 | ||
247 | z_type2(given(Vars), _, given(Vars), none). | |
248 | z_type2(namedset(SetName,Vars), _, namedset(SetName,Vars), none). | |
249 | z_type2(data(Name,Arms), Env, data(Name,ArmsTi), none) :- | |
250 | z_type_arms(Arms,Env,Name,ArmsTi). | |
251 | z_type2(sdef(Head,Body), Env, sdef(Head,BodyTi), none) :- | |
252 | z_type_schema(Head,Body,Env,BodyTi). | |
253 | z_type2(defeq(Head,Body), Env, defeq(Head,BodyTi), none) :- | |
254 | z_type_schema(Head,Body,Env,BodyTi). | |
255 | z_type2(eqeq(lhs(Name,ParamNames),Expr), Env, eqeq(lhs(Name,ParamNames),ExprTi), none) :- | |
256 | create_param_env(ParamNames,Env,ParamEnv), | |
257 | z_type(Expr,ParamEnv,PType,ExprTi), | |
258 | generic_type(ParamNames,PType,Type), | |
259 | lookup_type(Env,Name,Type). | |
260 | z_type2(axdef(Body), Env, axdef(BodyTi), none) :- | |
261 | z_type_globaldef(Body,[],Env,BodyTi). | |
262 | z_type2(define(ParamNames,Body), Env, define(ParamNames,BodyTi), none) :- | |
263 | z_type_globaldef(Body,ParamNames,Env,BodyTi). | |
264 | z_type2(pred(Pred), Env, pred(PredTi), none) :- | |
265 | z_type(Pred,Env,bool,PredTi). | |
266 | ||
267 | ||
268 | % internal expressions | |
269 | z_type2(basetype(Type), _, basetype(Type), Type). | |
270 | ||
271 | z_type2(binding(Bindings), Env, binding(BindingTis), schema(Fields)) :- | |
272 | z_type_binding(Bindings,Env,UFields,BindingTis), | |
273 | normalize_fields(UFields,Fields). | |
274 | ||
275 | z_type2(ftconstant(Freetype,Name), _, ftconstant(Freetype,Name),freetype(Freetype)). | |
276 | z_type2(ftconstructor(Freetype,Name,Expr), Env, | |
277 | ftconstructor(Freetype,Name,ExprTi), freetype(Freetype)) :- | |
278 | z_type(Expr,Env,_,ExprTi). | |
279 | z_type2(ftdestructor(Freetype,Name,Expr), Env, ftdestructor(Freetype,Name,ExprTi), Type) :- | |
280 | z_type(Expr,Env,freetype(Freetype),ExprTi), | |
281 | lookup_type(Env,Name,ConstructorType), | |
282 | zrel(Type,freetype(Freetype),ConstructorType). | |
283 | z_type2(ftcase(Freetype,Name,Expr), Env, ftcase(Freetype,Name,ExprTi), bool) :- | |
284 | z_type(Expr,Env,freetype(Freetype),ExprTi). | |
285 | ||
286 | ||
287 | ||
288 | %******************************************************************************** | |
289 | % Type checking for lists of expressions | |
290 | ||
291 | % z_type_l(Expressions, Environment, Types, TypeInfos). | |
292 | % Computes the type of each expression in the list and returns the | |
293 | % type informations and types as lists. | |
294 | z_type_l([],_,[],[]). | |
295 | z_type_l([Expr|Rest],Env,[Type|RestTypes],[TypeInfo|RestInfos]) :- | |
296 | z_type(Expr, Env, Type, TypeInfo), | |
297 | z_type_l(Rest, Env, RestTypes, RestInfos). | |
298 | ||
299 | % z_type_sets(Expressions, Environment, Types, TypeInfos). | |
300 | % Computes the type of each (set) expression in the list and returns the | |
301 | % the type informations and the types with the "set" removed. | |
302 | z_type_sets([],_,[],[]). | |
303 | z_type_sets([Expr|Rest],Env,[Type|RestTypes],[TypeInfo|RestInfos]) :- | |
304 | z_type(Expr,Env,set(Type),TypeInfo), | |
305 | z_type_sets(Rest,Env,RestTypes,RestInfos). | |
306 | ||
307 | z_type_binding([],_,[],[]). | |
308 | z_type_binding([bindfield(Name,Expr)|BRest],Env,[field(Name,Type)|FRest], | |
309 | [ti(bindfield(Name,TypeInfo),none)|RestInfos]) :- | |
310 | z_type(Expr,Env,Type,TypeInfo), | |
311 | z_type_binding(BRest,Env,FRest,RestInfos). | |
312 | ||
313 | % z_types_common(Expressions, Environemnt, Type, TypeInfos). | |
314 | % Assumes that each expression in the list has the same Type and | |
315 | % returns the list of all type informations. | |
316 | z_types_common([],_,_,[]). | |
317 | z_types_common([Expr|Rest],Env,Type,[TypeInfo|RestInfos]) :- | |
318 | z_type(Expr,Env,Type,TypeInfo), | |
319 | z_types_common(Rest,Env,Type,RestInfos). | |
320 | ||
321 | % types_in_let(Letdefs,Environment,Variables,TypeInfos). | |
322 | % Computes the type of each expression in the list of let definitions and | |
323 | % returns a list of variables with their corresponding type and a list | |
324 | % of type informations for the let definitions. | |
325 | types_in_let([],_,[],[]). | |
326 | types_in_let([letdef(Name,Expr)|Rest],Env,[variable(Name,Type)|RTypes],[LetTi|RestInfos]) :- | |
327 | LetTi = ti(letdef(Name,TypeInfo),none), | |
328 | z_type(Expr,Env,Type,TypeInfo), | |
329 | types_in_let(Rest,Env,RTypes,RestInfos). | |
330 | ||
331 | z_type_arms([],_,_,[]). | |
332 | z_type_arms([Arm|ArmRest],Env,Freetype,[ti(AnnotatedArm,none)|TiRest]) :- | |
333 | z_type_arm(Arm,Env,Freetype,AnnotatedArm), | |
334 | z_type_arms(ArmRest,Env,Freetype,TiRest). | |
335 | z_type_arm(arm(Name,nothing), Env, _, arm(Name,TypeInfo)) :- | |
336 | z_type(nothing,Env,_,TypeInfo). | |
337 | z_type_arm(arm(Name,just(Expr)), Env, Freetype, arm(Name,ti(just(TypeInfo),none))) :- | |
338 | zrel(DomType,RanType,Type), | |
339 | z_type(Expr,Env,set(DomType),TypeInfo), | |
340 | lookup_type(Env,Freetype,set(RanType)), | |
341 | lookup_type(Env,Name,Type). | |
342 | ||
343 | % z_type_body(Body,BodyTypeInfo,Subenvironment). | |
344 | % Type checks the given body and returns the type information and the | |
345 | % subenvironment specified by the body | |
346 | z_type_body(body(Decl,Where),Env,Type,BodyTi,Subenv) :- | |
347 | BodyTi = ti(body(DeclTi,WhereTi),Type), | |
348 | Type = set(schema(Fields)), | |
349 | type_decls(Decl,Env,DeclTi,Fields), | |
350 | fields2var(Fields,Vars), | |
351 | create_subenv(Env,Vars,Subenv), | |
352 | z_types_common(Where,Subenv,bool,WhereTi). | |
353 | ||
354 | fields2var([],[]). | |
355 | fields2var([field(N,T)|FRest],[variable(N,T)|VRest]) :- fields2var(FRest,VRest). | |
356 | ||
357 | %******************************************************************************** | |
358 | % predicates for type checking schemas | |
359 | z_type_schema(shead(Name,ParamNames),Body,Env,BodyTi) :- | |
360 | findall(ref(P,[]),member(P,ParamNames),ParamValues), | |
361 | z_type_schemabody(Body,'',ParamNames,ParamValues,[],Env,PType,BodyTi), | |
362 | generic_type(ParamNames,PType,Type), | |
363 | lookup_type(Env,name(Name,''),Type). | |
364 | ||
365 | z_type_schemabody(Body,Deco,PNames,PValues,Renamings,Env,set(schema(Fields)),TypeInfo) :- | |
366 | create_param_env(PNames,Env,ParamEnv), | |
367 | insert_parameter(Body,PNames,PValues,Expr), | |
368 | z_type(Expr,ParamEnv,set(schema(Fields1)),TypeInfo), | |
369 | decorate_fields(Fields1,Deco,Fields2), | |
370 | rename_fields(Fields2,Renamings,UFields), | |
371 | normalize_fields(UFields,Fields). | |
372 | ||
373 | z_type_globaldef(Body,ParamNames,Env,BodyTi) :- | |
374 | create_param_env(ParamNames,Env,ParamEnv), | |
375 | z_type(Body,ParamEnv,set(schema(Fields)),BodyTi), | |
376 | z_type_globaldef2(Fields,ParamNames,Env). | |
377 | z_type_globaldef2([],_,_). | |
378 | z_type_globaldef2([field(Name,PType)|Rest],ParamNames,Env) :- | |
379 | generic_type(ParamNames,PType,Type), | |
380 | lookup_type(Env,Name,Type), | |
381 | z_type_globaldef2(Rest,ParamNames,Env). | |
382 | ||
383 | ||
384 | pipe_fields(AFields,BFields,Out,In) :- | |
385 | intersect_fields(AFields,BFields,'!','?',Out,In). | |
386 | composite_fields(AFields,BFields,Out,In) :- | |
387 | intersect_fields(AFields,BFields,'\'','',Out,In). | |
388 | intersect_fields([],_,_,_,[],[]). | |
389 | intersect_fields([field(name(Name,DecoA),Type)|ARest],BFields,DecoA,DecoB, | |
390 | [name(Name,DecoA)|ORest],[name(Name,DecoB)|IRest]) :- | |
391 | member(field(name(Name,DecoB),TypeB),BFields), | |
392 | !,Type = TypeB, | |
393 | intersect_fields(ARest,BFields,DecoA,DecoB,ORest,IRest). | |
394 | intersect_fields([_|ARest],BFields,DecoA,DecoB,ORest,IRest) :- | |
395 | intersect_fields(ARest,BFields,DecoA,DecoB,ORest,IRest). | |
396 | ||
397 | ||
398 | ||
399 | generic_type(ParamNames,Type,GenericType) :- | |
400 | (ParamNames = [] -> | |
401 | GenericType = Type; | |
402 | GenericType = generic(ParamNames,Type)). | |
403 | ||
404 | ||
405 | :- use_module(probsrc(error_manager),[add_internal_error/2]). | |
406 | global_environment(Defs,Env,DefsTi) :- | |
407 | create_initial_zenvironment(Defs,GlobalEnv), | |
408 | ||
409 | predefined_variables(Predefs), | |
410 | create_subenv(GlobalEnv,Predefs,PreEnv), | |
411 | global_variables(PreEnv,Usertypes), | |
412 | create_subenv(PreEnv,Usertypes,Env), | |
413 | ||
414 | (z_type(Defs,Env,_,DefsTi) -> true ; add_internal_error('Typing Definitions failed: ',global_environment),fail). | |
415 | ||
416 | % only for debugging: | |
417 | :- public remove_zdef/2. | |
418 | remove_zdef(zdef(_),zdef([])). | |
419 | remove_zdef(env(E,D),env(R,D)) :- remove_zdef(E,R). | |
420 | ||
421 | predefined_variables(Predefs) :- | |
422 | findall(variable(Name,Type),predefinedvar(Name,Type),Predefs). | |
423 | ||
424 | global_variables(Env,Types) :- | |
425 | % given types | |
426 | findall(variable(Name,set(given(Name))),(zlookup(Env,given(L)),member(Name,L)),Given), | |
427 | % named sets | |
428 | findall(variable(Name,set(given(Name))),zlookup(Env,namedset(Name,_)),NamedSets), | |
429 | findall(variable(Name,given(SetName)), | |
430 | (zlookup(Env,namedset(SetName,L)),member(Name,L)),NamedSetMembers), | |
431 | % free types | |
432 | findall(variable(Name,set(freetype(Name))),zlookup(Env,data(Name,_)),FreeTypes), | |
433 | % free type constants | |
434 | findall(variable(Name,freetype(Freetype)), | |
435 | (zlookup(Env,data(Freetype,Arms)),member(arm(Name,nothing),Arms)), | |
436 | FTConstants), | |
437 | % free type constructors: not defined yet | |
438 | findall(variable(Name,set(tuple([_,freetype(Freetype)]))), | |
439 | (zlookup(Env,data(Freetype,Arms)),member(arm(Name,just(_)),Arms)), | |
440 | FTConstructors), | |
441 | % schema types: not defined yet | |
442 | env_z_defs(Env,Defs), | |
443 | findall(variable(name(Name,''),set(schema(_))), | |
444 | (member(Def,Defs), | |
445 | (Def = sdef(shead(Name,[]),_); | |
446 | Def = defeq(shead(Name,[]),_))), | |
447 | Schemas), | |
448 | findall(variable(name(Name,''),generic(Params,set(schema(_)))), | |
449 | (member(Def,Defs), | |
450 | Params = [_|_], | |
451 | (Def = sdef(shead(Name,Params),_); | |
452 | Def = defeq(shead(Name,Params),_))), | |
453 | ParamSchemas), | |
454 | % constants | |
455 | findall(variable(Name,_), | |
456 | (zlookup(Env,axdef(body(Decls,_))),decl_member(Decls,Name,_)), | |
457 | Constants), | |
458 | % abbreviations | |
459 | findall(variable(Name,_),zlookup(Env,eqeq(lhs(Name,[]),_)),Abbrevs), | |
460 | findall(variable(Name,generic(Params,_)), | |
461 | (zlookup(Env,eqeq(lhs(Name,Params),_)),Params=[_|_]), | |
462 | GenAbbrevs), | |
463 | % generic definitions | |
464 | findall(variable(Name,generic(Params,_)), | |
465 | (zlookup(Env,define(Params,body(Decls,_))),decl_member(Decls,Name,_)), | |
466 | Generics), | |
467 | ||
468 | append([Given,NamedSets,NamedSetMembers,FreeTypes,FTConstants,FTConstructors, | |
469 | Schemas,ParamSchemas,Constants,Abbrevs,GenAbbrevs,Generics], | |
470 | Types). | |
471 | ||
472 | ||
473 | type_of_field(Fields,Fieldname,Type) :- | |
474 | when(nonvar(Fields),type_of_field2(Fields,Fieldname,Type)). | |
475 | type_of_field2([F|R],Fieldname,Type) :- | |
476 | when(nonvar(F),type_of_field3([F|R],Fieldname,Type)). | |
477 | type_of_field3([field(Fieldname,Type)|_],Fieldname,Type) :- !. | |
478 | type_of_field3([_|Rest],Fieldname,Type) :- type_of_field2(Rest,Fieldname,Type). | |
479 | ||
480 | ||
481 | create_param_env([],Env,Env) :- !. | |
482 | create_param_env(Params,Env,NewEnv) :- | |
483 | Params = [_|_], | |
484 | findall(variable(Name,set(param(Name))),member(Name,Params),PVars), | |
485 | create_subenv(Env,PVars,NewEnv). | |
486 | ||
487 | decl_member([decl(Vars,Type)|_],Var,Type) :- member(Var,Vars). | |
488 | decl_member([_|Rest],Var,Type) :- decl_member(Rest,Var,Type). | |
489 | ||
490 | ||
491 | prepare_generic(Params,Env,Gentype,Ids,Types) :- | |
492 | get_params(Params,Env,PTypes), | |
493 | unify_generic(Gentype,Ids,PTypes,Types). | |
494 | ||
495 | unify_generic(Gentype,Ids,PTypes,Types) :- | |
496 | same_length(Ids,PTypes), | |
497 | when(ground(Gentype),prepare_generic2(Gentype,Ids,PTypes,Types)). | |
498 | ||
499 | prepare_generic2(param(P),Ids,Vars,Type) :- | |
500 | nth0(N,Ids,P) -> nth0(N,Vars,Type) ; Type = param(P). | |
501 | prepare_generic2(set(T),Ids,Vars,set(Type)) :- prepare_generic2(T,Ids,Vars,Type). | |
502 | prepare_generic2(tuple(T),Ids,Vars,tuple(Types)) :- prepare_generic_l(T,Ids,Vars,Types). | |
503 | prepare_generic2(schema(T),Id,Vars,schema(Types)) :- prepare_generic_fields(T,Id,Vars,Types). | |
504 | prepare_generic2(num,_,_,num). | |
505 | prepare_generic2(given(G),_,_,given(G)). | |
506 | prepare_generic2(freetype(F),_,_,freetype(F)). | |
507 | ||
508 | prepare_generic_l([],_,_,[]). | |
509 | prepare_generic_l([T|Rest],Ids,Vars,[Type|TRest]) :- | |
510 | prepare_generic2(T,Ids,Vars,Type), | |
511 | prepare_generic_l(Rest,Ids,Vars,TRest). | |
512 | ||
513 | prepare_generic_fields([],_,_,[]). | |
514 | prepare_generic_fields([field(Name,T)|Rest],Ids,Vars,[field(Name,Type)|TRest]) :- | |
515 | prepare_generic2(T,Ids,Vars,Type), | |
516 | prepare_generic_fields(Rest,Ids,Vars,TRest). | |
517 | ||
518 | get_params([],_,_). | |
519 | get_params([EH|ER],Env,Types) :- z_type_sets([EH|ER],Env,Types,_). | |
520 | ||
521 | ||
522 | ||
523 | % basic | |
524 | predefinedvar(name('\\neq',''),generic([x],T)) :- zprel(x,x,T). | |
525 | ||
526 | % sets | |
527 | predefinedvar(name('\\emptyset',''),generic([x],set(param(x)))). | |
528 | %predefinedvar(name('\\emptyset',''),generic([x],T)) :- % emptyset with parameter e.g., \emptyset[\nat] | |
529 | % Set=set(param(x)), zrel(Set,Set,T). | |
530 | predefinedvar(name('\\power_1',''),generic([x],T)) :- zrel(set(param(x)),set(set(param(x))),T). | |
531 | predefinedvar(name('\\finset',''),T) :- predefinedvar(name('\\power_1',''),T). | |
532 | predefinedvar(name('\\finset','_1'),T) :- predefinedvar(name('\\power_1',''),T). | |
533 | % sets: operations | |
534 | predefinedvar(name('\\cup',''),generic([x],T)) :- | |
535 | Set=set(param(x)), zrel(tuple([Set,Set]),Set,T). | |
536 | predefinedvar(name('\\cap',''),T) :- predefinedvar(name('\\cup',''),T). | |
537 | predefinedvar(name('\\setminus',''),T) :- predefinedvar(name('\\cup',''),T). | |
538 | predefinedvar(name('\\bigcup',''),generic([x],T)) :- zrel(set(set(param(x))),set(param(x)),T). | |
539 | predefinedvar(name('\\bigcap',''),T) :- predefinedvar(name('\\bigcup',''),T). | |
540 | predefinedvar(name('\\#',''),generic([x],T)) :- zrel(set(param(x)),num,T). | |
541 | % sets: relations | |
542 | predefinedvar(name('\\subseteq',''),generic([x],T)) :- zrel(set(param(x)),set(param(x)),T). | |
543 | predefinedvar(name('\\subset',''),T) :- predefinedvar(name('\\subseteq',''),T). | |
544 | predefinedvar(name('\\notin',''),generic([x],T)) :- zrel(param(x),set(param(x)),T). | |
545 | ||
546 | % relations: sets | |
547 | predefinedvar(name('\\rel',''),generic([x,y],T)) :- | |
548 | zrel(tuple([set(param(x)),set(param(y))]),set(R),T), zprel(x,y,R). | |
549 | predefinedvar(name('\\pfun',''),T) :- predefinedvar(name('\\rel',''),T). | |
550 | predefinedvar(name('\\fun',''),T) :- predefinedvar(name('\\rel',''),T). | |
551 | predefinedvar(name('\\pinj',''),T) :- predefinedvar(name('\\rel',''),T). | |
552 | predefinedvar(name('\\inj',''),T) :- predefinedvar(name('\\rel',''),T). | |
553 | predefinedvar(name('\\psurj',''),T) :- predefinedvar(name('\\rel',''),T). | |
554 | predefinedvar(name('\\surj',''),T) :- predefinedvar(name('\\rel',''),T). | |
555 | predefinedvar(name('\\bij',''),T) :- predefinedvar(name('\\rel',''),T). | |
556 | predefinedvar(name('\\ffun',''),T) :- predefinedvar(name('\\rel',''),T). | |
557 | predefinedvar(name('\\finj',''),T) :- predefinedvar(name('\\rel',''),T). | |
558 | % relations: functions | |
559 | predefinedvar(name('\\dom',''),generic([x,y],T)) :- zprel(x,y,R),zrel(R,set(param(x)),T). | |
560 | predefinedvar(name('\\ran',''),generic([x,y],T)) :- zprel(x,y,R),zrel(R,set(param(y)),T). | |
561 | % relations: operations | |
562 | predefinedvar(name('\\id',''),generic([x],T)) :- zrel(set(param(x)),R,T),zprel(x,x,R). | |
563 | predefinedvar(name('\\inv',''),generic([x,y],T)) :- zprelfunc(x,y,y,x,T). | |
564 | predefinedvar(name('\\plus',''),generic([x],T)) :- zprelfunc(x,x,x,x,T). | |
565 | predefinedvar(name('\\star',''),T) :- predefinedvar(name('\\plus',''),T). | |
566 | predefinedvar(name('\\comp',''),generic([x,y,z],T)) :- | |
567 | zprel(x,y,A),zprel(y,z,B),zprel(x,z,C),zrel(tuple([A,B]),C,T). | |
568 | predefinedvar(name('\\circ',''),generic([x,y,z],T)) :- | |
569 | zprel(x,y,A),zprel(y,z,B),zprel(x,z,C),zrel(tuple([B,A]),C,T). | |
570 | predefinedvar(name('\\dres',''),generic([x,y],T)) :- | |
571 | zprel(x,y,R),zrel(tuple([set(param(x)),R]),R,T). | |
572 | predefinedvar(name('\\rres',''),generic([x,y],T)) :- | |
573 | zprel(x,y,R),zrel(tuple([R,set(param(y))]),R,T). | |
574 | predefinedvar(name('\\ndres',''),T) :- predefinedvar(name('\\dres',''),T). | |
575 | predefinedvar(name('\\nrres',''),T) :- predefinedvar(name('\\rres',''),T). | |
576 | predefinedvar(name('_(|_|)',''),generic([x,y],T)) :- | |
577 | zprel(x,y,R),zrel(tuple([R,set(param(x))]),set(param(y)),T). | |
578 | predefinedvar(name('\\oplus',''),generic([x,y],T)) :- | |
579 | zprel(x,y,R),zrel(tuple([R,R]),R,T). | |
580 | predefinedvar(name(iter,''),generic([x],T)) :- | |
581 | zprelfunc(x,x,x,x,F),zrel(num,F,T). | |
582 | ||
583 | % numbers: sets | |
584 | predefinedvar(name('\\num',''),set(num)). | |
585 | predefinedvar(name('\\nat',''),set(num)). | |
586 | predefinedvar(name('\\nat','_1'),set(num)). | |
587 | predefinedvar(name('\\upto',''),T) :- zrel(tuple([num,num]),set(num),T). | |
588 | % numbers: operations | |
589 | predefinedvar(name('(-)',''),T) :- zrel(num,num,T). | |
590 | predefinedvar(name('+',''),T) :- zrel(tuple([num,num]),num,T). | |
591 | predefinedvar(name('-',''),T) :- predefinedvar(name('+',''),T). | |
592 | predefinedvar(name('*',''),T) :- predefinedvar(name('+',''),T). | |
593 | predefinedvar(name('\\div',''),T) :- predefinedvar(name('+',''),T). | |
594 | predefinedvar(name('\\mod',''),T) :- predefinedvar(name('+',''),T). | |
595 | % numbers: functions | |
596 | predefinedvar(name('succ',''),T) :- zrel(num,num,T). | |
597 | predefinedvar(name('min',''),T) :- zrel(set(num),num,T). | |
598 | predefinedvar(name('max',''),T) :- predefinedvar(name('min',''),T). | |
599 | % numbers: relations | |
600 | predefinedvar(name('<',''),T) :- zrel(num,num,T). | |
601 | predefinedvar(name('\\leq',''),T) :- predefinedvar(name('<',''),T). | |
602 | predefinedvar(name('\\geq',''),T) :- predefinedvar(name('<',''),T). | |
603 | predefinedvar(name('>',''),T) :- predefinedvar(name('<',''),T). | |
604 | ||
605 | % sequences: sequences | |
606 | predefinedvar(name('\\seq',''),generic([x],T)) :- zseq(param(x),Seq),zrel(set(param(x)),set(Seq),T). | |
607 | predefinedvar(name('\\seq','_1'),T) :- predefinedvar(name('\\seq',''),T). | |
608 | predefinedvar(name('\\iseq',''),T) :- predefinedvar(name('\\seq',''),T). | |
609 | % sequences: operations | |
610 | predefinedvar(name('\\cat',''),generic([x],T)) :- | |
611 | zseq(param(x),S),zrel(tuple([S,S]),S,T). | |
612 | % sequences: functions | |
613 | predefinedvar(name('rev',''),generic([x],T)) :- zseq(param(x),S),zrel(S,S,T). | |
614 | predefinedvar(name('head',''),generic([x],T)) :- zseq(param(x),S),zrel(S,param(x),T). | |
615 | predefinedvar(name('last',''),T) :- predefinedvar(name('head',''),T). | |
616 | predefinedvar(name('tail',''),T) :- predefinedvar(name('rev',''),T). | |
617 | predefinedvar(name('front',''),T) :- predefinedvar(name('tail',''),T). | |
618 | predefinedvar(name('\\extract',''),generic([x],T)) :- | |
619 | zseq(param(x),S),zrel(tuple([set(num),S]),S,T). | |
620 | predefinedvar(name('\\filter',''),generic([x],T)) :- | |
621 | zseq(param(x),S),zrel(tuple([S,set(param(x))]),S,T). | |
622 | predefinedvar(name('squash',''),generic([x],T)) :- zseq(param(x),S),zrel(S,S,T). | |
623 | predefinedvar(name('\\dcat',''),generic([x],T)) :- | |
624 | zseq(param(x),S),zseq(S,SS),zrel(SS,S,T). | |
625 | predefinedvar(name('\\disjoint',''),generic([i,x],set(P))) :- | |
626 | zrel(param(i),set(param(x)),P). | |
627 | predefinedvar(name('\\partition',''),generic([i,x],T)) :- | |
628 | zrel(P,set(param(x)),T),zrel(param(i),set(param(x)),P). | |
629 | % sequences: relations | |
630 | predefinedvar(name('\\prefix',''),generic([x],set(tuple([S,S])))) :- zseq(param(x),S). | |
631 | predefinedvar(name('\\suffix',''),T) :- predefinedvar(name('\\prefix',''),T). | |
632 | predefinedvar(name('\\inseq',''),T) :- predefinedvar(name('\\prefix',''),T). | |
633 | ||
634 | % bag: set | |
635 | predefinedvar(name('\\bag',''),generic([x],T)) :- zbag(param(x),Bag),zrel(set(param(x)),set(Bag),T). | |
636 | % bag: functions | |
637 | predefinedvar(name('items',''),generic([x],T)) :- | |
638 | zseq(param(x),Seq), zbag(param(x),Bag), zrel(Seq,Bag,T). | |
639 | predefinedvar(name('count',''),generic([x],T)) :- | |
640 | zrel(param(x),num,ConcreteCount),zbag(param(x),Bag),zrel(Bag,ConcreteCount,T). | |
641 | predefinedvar(name('\\bcount',''),generic([x],T)) :- | |
642 | zbag(param(x),Bag),zrel(tuple([Bag,param(x)]),num,T). | |
643 | predefinedvar(name('\\otimes',''),generic([x],T)) :- | |
644 | zbag(param(x),Bag),zrel(tuple([num,Bag]),Bag,T). | |
645 | predefinedvar(name('\\uplus',''),generic([x],T)) :- | |
646 | zbag(param(x),Bag),zrel(tuple([Bag,Bag]),Bag,T). | |
647 | predefinedvar(name('\\uminus',''),T) :- predefinedvar(name('\\uplus',''),T). | |
648 | predefinedvar(name('\\inbag',''),generic([x],Rel)) :- | |
649 | zbag(param(x),Bag),zrel(param(x),Bag,Rel). | |
650 | predefinedvar(name('\\subbageq',''),generic([x],Rel)) :- | |
651 | zbag(param(x),Bag),zrel(Bag,Bag,Rel). | |
652 | ||
653 | % tuples: operations | |
654 | predefinedvar(name('\\mapsto',''),generic([x,y],T)) :- | |
655 | zrel(tuple([param(x),param(y)]),tuple([param(x),param(y)]),T). | |
656 | % tuples: functions | |
657 | predefinedvar(name('first',''),generic([x,y],T)) :- zrel(tuple([param(x),param(y)]),param(x),T). | |
658 | predefinedvar(name('second',''),generic([x,y],T)) :- zrel(tuple([param(x),param(y)]),param(y),T). | |
659 | ||
660 | ||
661 | % internal constructs | |
662 | predefinedvar(name('\\prozignore',''),generic([x],T)) :- zrel(set(param(x)),set(param(x)),T). | |
663 | ||
664 | ||
665 | zrel(A,B,set(tuple([A,B]))). | |
666 | zprel(A,B,R) :- zrel(param(A),param(B),R). | |
667 | zseq(A,T) :- zrel(num,A,T). | |
668 | zrelfunc(A,B,C,D,F) :- zrel(A,B,X),zrel(C,D,Y),zrel(X,Y,F). | |
669 | zprelfunc(A,B,C,D,F) :- zrelfunc(param(A),param(B),param(C),param(D),F). | |
670 | ||
671 | zbag(A,T) :- zrel(A,num,T). | |
672 | ||
673 | ||
674 | /******************************************************************************/ | |
675 | ||
676 | type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,set(schema(Fields))) :- | |
677 | z_type(Body,Env,set(schema(Fieldlist)),BodyTi), | |
678 | z_type(Schema,Env,set(schema(InnerFields)),SchemaTi), | |
679 | eliminate_fields(Fieldlist,InnerFields,UFields), | |
680 | normalize_fields(UFields,Fields). | |
681 | ||
682 | logical_bin_schema(A,B,Env,Ati,Bti,set(schema(Fields))) :- | |
683 | get_fields(A,B,Env,Ati,Bti,FieldsA,FieldsB), | |
684 | merge_fields(FieldsA,FieldsB,Fields). | |
685 | ||
686 | get_fields(A,B,Env,Ati,Bti,FieldsA,FieldsB) :- | |
687 | z_type(A,Env,set(schema(FieldsA)),Ati), | |
688 | z_type(B,Env,set(schema(FieldsB)),Bti). | |
689 | ||
690 | ||
691 | type_decls(Decls,Env,DeclTi,Fields) :- | |
692 | type_decls2(Decls,Env,DeclTi,UFields), | |
693 | normalize_fields(UFields,Fields). | |
694 | type_decls2([],_,[],[]). | |
695 | type_decls2([decl(Vars,TypeExpr)|Rest],Env,[DeclTi|RestTi],Fields) :- | |
696 | !,DeclTi = ti(decl(Vars,TypeInfo),none), | |
697 | z_type(TypeExpr,Env,set(Type),TypeInfo), | |
698 | create_field_types(Vars,Type,LocalFields), | |
699 | append(LocalFields,RestFields,Fields), | |
700 | type_decls2(Rest,Env,RestTi,RestFields). | |
701 | type_decls2([sdecl(Sref)|Rest],Env,[SDeclTi|RestTi],Fields) :- | |
702 | SDeclTi = ti(sdecl(SrefTi),none), | |
703 | z_type(Sref,Env,set(schema(LocalFields)),SrefTi), | |
704 | append(LocalFields,RestFields,Fields), | |
705 | type_decls2(Rest,Env,RestTi,RestFields). | |
706 | create_field_types([],_,[]). | |
707 | create_field_types([Name|NRest],Type,[field(Name,Type)|FRest]) :- | |
708 | create_field_types(NRest,Type,FRest). | |
709 | ||
710 | ||
711 | merge_fields(FieldsA,FieldsB,Fields) :- | |
712 | eliminate_fields(FieldsA,FieldsB,NewFieldsB), | |
713 | append(FieldsA,NewFieldsB,UnsortedFields), | |
714 | normalize_fields(UnsortedFields,Fields). | |
715 | ||
716 | eliminate_fields([],_,[]). | |
717 | eliminate_fields([field(Name,TypeA)|Rest],Eliminate,Fields) :- | |
718 | (member(field(Name,TypeB),Eliminate) -> | |
719 | (TypeA = TypeB, Fields = Rest); | |
720 | Fields = [field(Name,TypeA)|ERest]), | |
721 | eliminate_fields(Rest,Eliminate,ERest). | |
722 | ||
723 | normalize_fields(Fields,Normalized) :- | |
724 | findall(Name,member(field(Name,_),Fields),Fieldnames), | |
725 | sort(Fieldnames,SFieldnames), | |
726 | normalize_fields2(SFieldnames,Fields,Normalized). | |
727 | normalize_fields2([],_,[]). | |
728 | normalize_fields2([Name|Rest],Fields,[field(Name,Type)|NRest]) :- | |
729 | member(field(Name,Type),Fields),!, | |
730 | normalize_fields2(Rest,Fields,NRest). | |
731 | ||
732 | decorate_fields(A,Deco,B) :- (Deco = '' -> A=B; decorate_fields2(A,Deco,B)). | |
733 | decorate_fields2([],_,[]). | |
734 | decorate_fields2([field(name(Name,DecoA),Type)|Rest],Deco,[field(name(Name,DecoB),Type)|DRest]) :- | |
735 | atom_concat(DecoA,Deco,DecoB), | |
736 | decorate_fields2(Rest,Deco,DRest). | |
737 | ||
738 | rename_fields([],_,[]). | |
739 | rename_fields([field(NameA,Type)|Rest],Renamings,[field(NameB,Type)|RenamedRest]) :- | |
740 | (member(rename(NameB,NameA),Renamings) -> | |
741 | true; | |
742 | NameA = NameB), | |
743 | rename_fields(Rest,Renamings,RenamedRest). | |
744 | ||
745 | ||
746 | % declaration_tuple(Declarations,Environment,Tuple) | |
747 | % returns the expression for the tuple representing the declaration, | |
748 | % if only one variable is declared, a reference to the variable is returned. | |
749 | declaration_tuple(Decl,Env,Tuple) :- | |
750 | schema_vars_decl(Decl,Env,Vars), | |
751 | declaration_tuple2(Vars,Tuple). | |
752 | declaration_tuple2([Name],ref(Name,[])) :- !. | |
753 | declaration_tuple2([A,B|R],tuple(Refs)) :- | |
754 | findall(ref(Name,[]),member(Name,[A,B|R]),Refs). | |
755 | ||
756 | ||
757 | %******************************************************************************** | |
758 | ||
759 | remove_fields_by_name([],_,[]). | |
760 | remove_fields_by_name([field(Name,Type)|FRest],ToRemove,Result) :- | |
761 | (member(Name,ToRemove) -> | |
762 | !,Result = Rest; | |
763 | Result = [field(Name,Type)|Rest]), | |
764 | remove_fields_by_name(FRest,ToRemove,Rest). | |
765 | ||
766 | %******************************************************************************** | |
767 | % extract_btypes/3 returns the list of all variables declared in the given | |
768 | % schema definition. It returns also a list of the types in the internal ProB | |
769 | % syntax. | |
770 | extract_btypes(SchemaDef,Vars,Types) :- | |
771 | ( ti_expr(SchemaDef,sdef(_,BodyTi)) | |
772 | ; ti_expr(SchemaDef,defeq(_,BodyTi)) | |
773 | ; ti_expr(SchemaDef,axdef(BodyTi))), | |
774 | !, | |
775 | ti_type(BodyTi,set(schema(Fields))), | |
776 | zfields2b(Fields,Vars,Types). | |
777 | ||
778 | zfields2b([],[],[]). | |
779 | zfields2b([field(Name,IType)|FRest],[Name|IRest],[BType|BRest]) :- | |
780 | internal2b(IType,BType), | |
781 | zfields2b(FRest,IRest,BRest). | |
782 | ||
783 | internal2b(num,integer). | |
784 | internal2b(given(Name),global(Id)) :- z_translate_identifier(Name,Id). | |
785 | internal2b(freetype(Name),freetype(Id)) :- z_translate_identifier(Name,Id). | |
786 | internal2b(set(X),set(T)) :- internal2b(X,T). | |
787 | internal2b(tuple([A,B]),couple(Ab,Bb)) :- internal2b(A,Ab),internal2b(B,Bb). | |
788 | internal2b(tuple([A,B,C|Rest]),couple(Ab,Rb)) :- | |
789 | internal2b(A,Ab),internal2b(tuple([B,C|Rest]),Rb). | |
790 | internal2b(schema(Fi),record(Fb)) :- internal2b_fields(Fi,Fb). | |
791 | ||
792 | internal2b(bool,pred). | |
793 | ||
794 | internal2b_fields([],[]). | |
795 | internal2b_fields([field(Name,Ti)|IRest],[field(Id,Tb)|BRest]) :- | |
796 | z_translate_identifier(Name,Id), | |
797 | internal2b(Ti,Tb), | |
798 | internal2b_fields(IRest,BRest). |