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). |