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