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